Re: [isabelle-dev] logging and debugging output
On Wed, 2 Apr 2014, stvienna wiener wrote: Now I started to use the development version of Isabelle instead of Isabelle 2013-2. My work is much more productive now, e.g., fewer crashes and the GUI is much more responsive. The development version is a running gag on this maling list, because that expression is not well-defined. There are presently more than 5 development versions. You need to say which version you are using, by the unique changeset id that is given in the welcome message, isabelle version -i, or hg id. (It does not make much sense to test snapshots that are older than approx. 1 week.) I am surprised to hear about crashes of Isabelle2013-2, but maybe these are just more secret problems that users don't want to tell and prefer to keep for themselves. What is your OS and hardware platform (memory, number of cores)? But still, Isabelle/JEdit gets unresponsive and unstable, then finally crashes completely. In most cases this happens after a try0 or try call. I suspect it could be a problem related to a fastforce call. Is there a way to look behind the scenes, e.g., to look at the communication between JEdit and Isabelle? Is there a system console or a logging console or any other way to get more debugging info? (I can only she the NullPointerExceptions in the lower right corner of the JEdit interface, i.e., the pink written message, and by clicking on it a pop up with the error message opens.) In principle the Protocol panel tells the whole story between the editor and the prover, but I don't think you will see anything useful there. If you have an exception trace, the obvious thing is to show that here. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Annotations in Theories panel not visible
On Tue, 1 Apr 2014, Lars Noschinski wrote: I made a short video: http://www21.in.tum.de/~noschinl/jedit-annotations.webm. I tested the Metal and Nimbus LF; the font is IsabelleText. This is on a system running Debian stable with Gnome 3.4.2. I couldn't reproduce the behaviour on another machine with Debian testing and Gnome 3.8.4. Looking closer yet again, the annotations don't vanish, but the bars get too wide. If you look at the video above, the Theories panel is redrawn two times before the actual process of proving starts. Each time, the width of the bars increases. After the third iteration, it is wider than the panel. But there is no optical indication for this (e.g., a scrollbar), so it looks like part of the annotations vanish when processing procedes into the hidden part of the panel. The video is very helpful, it shows the dynamics of what is really going on. My initial reaction (without much thinking) was to resize the Theories dockable, since I am used to Swing components not being very precise concerning scrollbars etc. (this also depends on LF). I don't know an easy way to combine scrollbars with flexible (two-dimensional) layouts, as seen in this list view. A more basic approach is now in Isabelle/8a58a8c5a1c0, just painting more borders. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Issues with interpretations
Hi all, My work on (co)datatypes and my desire to move Quickcheck_Narrowing out of HOL and into Library have lead me to discover several issues with the interpretation mechanism (Pure/interpretation.ML) that is used to hook into various modules (e.g., the size-generating extension to datatypes). I will summarize my findings below. It might well be that this is already (at least partially) known to some of you. In the following, I will talk concretely about datatype and their various hooks (size, Quickcheck random, Quickcheck narrowing, etc.), but the same issues can arise in principle with all the other hooking-mechanism based on Pure/interpretation.ML. Generally, the issues arise when a datatype is introduced in theory A and a hook is registered in theory B, and A does not import B. Scenario 1: Two Types, One Name In this scenario, we introduce two datatypes with the same base name (t) in two different theories: theory A imports ~~/src/HOL/Datatype begin datatype t = T end theory B imports ~~/src/HOL/Datatype begin datatype t = U | V end Then we get a name clash at merge time when pulling in a new hook (such as the one defined by Typerep below): theory C imports A B ~~/src/HOL/Typerep begin end *** Duplicate constant declaration C.typerep_t_inst.typerep_t vs. C.typerep_t_inst.typerep_t (line 1 of /Users/blanchet/bugs/scenarios/C.thy) *** At command theory (line 1 of /Users/blanchet/bugs/scenarios/C.thy) The examples above are self-contained and can be tested directly against a HOL or a Pure image. What's happening here is that the Typerep is generating theorems that contain the name t but not the unambiguous names A.t vs. B.t, and since the merge takes place in C, the prefix is C. for both. Interestingly, the size hook bypasses the problem by overriding the path using Sign.root_path and Sign.add_path. For example, this works: theory C2 imports A B ~~/src/HOL/Fun_Def begin thm A.size B.size end Hence, my original idea was to solve the name clash problem for all types by replicating the size trick, and perhaps to move the logic up either to the individual hooks or even to Pure/interpretation.ML. However, this does not solve all problems, as we will see in Scenario 2. Scenario 2: The Diamond theory D imports ~~/src/HOL/Datatype begin datatype t = T end theory E imports D ~~/src/HOL/Fun_Def begin end theory F imports D ~~/src/HOL/Fun_Def begin end theory G imports E F begin end *** Duplicate constant declaration D.t.t_size vs. D.t.t_size The problem is that these constants are defined by both E and F with the same name, so the merge in G fails. Scenario 3: The Specification Duplicate I thought I could work around the issue raised by Scenario 2 by having Isabelle generate names that combine the original theory name where the type was introduced and that where the merge took place that generated the name. In other words, generate E.D.t.t_size and F.D.t.t_size above. I tried this out, and it *almost* works. For the above theory G, it gives *** Clash of specifications for constant Nat.size_class.size: *** F.D.t.size_t_inst.size_t_def (line 1 of ~/bugs/scenarios/F.thy) *** E.D.t.size_t_inst.size_t_def (line 1 of ~/bugs/scenarios/E.thy) *** At command theory (line 1 of /Users/blanchet/bugs/scenarios/G.thy) Here the problem is that we overloaded the same constant Nat.size_class.size twice for the same type. It happens to be harmless here because size is well behaved (i.e. if we disabled the check in Pure/defs.ML, I believe we still couldn't derive False). I cannot think of a workaround. What does this mean in practice? 1. As long as we define new interpretations (hook types) in the HOL image, we can reorganize the imports to avoid the evil scenarios. Problems arise when users define their own interpretations. 2. In particular, moving Quickcheck_Narrowing outside HOL and into Library raises this issue in JinjaThreads. I will see if I can reorganize the imports. 3. Despite the failure with Scenario 3, the way size does things looks superior to the other approach, and I'm tempted to standardize on this for the old-style and new-style datatype hooks. I have patches ready already (cf. testboard). Please stop me if you disagree. 4. If anybody has any ideas on how to address Scenario 3, please let me know! Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Issues with interpretations
Hi Jasmin, 1. As long as we define new interpretations (hook types) in the HOL image, we can reorganize the imports to avoid the evil scenarios. Problems arise when users define their own interpretations. I already ran into scenario 3 without registering my own interpretations just by using code_datatype (which internally uses interpretation, too). Here's the example: theory A imports Main begin typedecl foo consts Foo :: foo end theory B imports A begin code_datatype Foo end theory C imports A begin code_datatype Foo end theory D imports A B begin end This gives the same error message as in your scenario 3: Clash of specifications for constant Typerep.typerep_class.typerep: ScratchB.typerep_foo_inst.typerep_foo_def ScratchA.typerep_foo_inst.typerep_foo_def 4. If anybody has any ideas on how to address Scenario 3, please let me know! I don't think that scenario 3 is the one to address. IMO the hooks should behave as if they were executed in the name space of the datatype declaration, so size is doing something sensible already. Rather do I think that it seems worthwhile to address scenario 2 by making name space merges more liberal. If there is a duplicate declaration of a constant, one could check whether the declarations of the constants are equivalent, and accept if so. Since I am not familiar with the internals, I do not know whether such a change is feasible in the current implementation. Andreas On 02/04/14 15:34, Jasmin Christian Blanchette wrote: Hi all, My work on (co)datatypes and my desire to move Quickcheck_Narrowing out of HOL and into Library have lead me to discover several issues with the interpretation mechanism (Pure/interpretation.ML) that is used to hook into various modules (e.g., the size-generating extension to datatypes). I will summarize my findings below. It might well be that this is already (at least partially) known to some of you. In the following, I will talk concretely about datatype and their various hooks (size, Quickcheck random, Quickcheck narrowing, etc.), but the same issues can arise in principle with all the other hooking-mechanism based on Pure/interpretation.ML. Generally, the issues arise when a datatype is introduced in theory A and a hook is registered in theory B, and A does not import B. Scenario 1: Two Types, One Name In this scenario, we introduce two datatypes with the same base name (t) in two different theories: theory A imports ~~/src/HOL/Datatype begin datatype t = T end theory B imports ~~/src/HOL/Datatype begin datatype t = U | V end Then we get a name clash at merge time when pulling in a new hook (such as the one defined by Typerep below): theory C imports A B ~~/src/HOL/Typerep begin end *** Duplicate constant declaration C.typerep_t_inst.typerep_t vs. C.typerep_t_inst.typerep_t (line 1 of /Users/blanchet/bugs/scenarios/C.thy) *** At command theory (line 1 of /Users/blanchet/bugs/scenarios/C.thy) The examples above are self-contained and can be tested directly against a HOL or a Pure image. What's happening here is that the Typerep is generating theorems that contain the name t but not the unambiguous names A.t vs. B.t, and since the merge takes place in C, the prefix is C. for both. Interestingly, the size hook bypasses the problem by overriding the path using Sign.root_path and Sign.add_path. For example, this works: theory C2 imports A B ~~/src/HOL/Fun_Def begin thm A.size B.size end Hence, my original idea was to solve the name clash problem for all types by replicating the size trick, and perhaps to move the logic up either to the individual hooks or even to Pure/interpretation.ML. However, this does not solve all problems, as we will see in Scenario 2. Scenario 2: The Diamond theory D imports ~~/src/HOL/Datatype begin datatype t = T end theory E imports D ~~/src/HOL/Fun_Def begin end theory F imports D ~~/src/HOL/Fun_Def begin end theory G imports E F begin end *** Duplicate constant declaration D.t.t_size vs. D.t.t_size The problem is that these constants are defined by both E and F with the same name, so the merge in G fails. Scenario 3: The Specification Duplicate I thought I could work around the issue raised by Scenario 2 by having Isabelle generate names that combine the original theory name where the type was introduced and that where the merge took place that generated the name. In other words, generate E.D.t.t_size and F.D.t.t_size above. I tried this out, and it *almost* works. For the above theory G, it gives *** Clash of specifications for constant Nat.size_class.size: *** F.D.t.size_t_inst.size_t_def (line 1 of ~/bugs/scenarios/F.thy) *** E.D.t.size_t_inst.size_t_def (line 1 of ~/bugs/scenarios/E.thy) *** At command
