Re: [isabelle-dev] Feedback from a Isabelle tutorial
Jasmin Blanchette wrote: This motivates me to attack the "linarith" problem. If nobody objects, I'll call the property "linarith_verbose" and have it on by default (for compatibility) but off in "try_methods" and "try". I've also taken the liberty to reword the "counterexample trace" message to make it clear that the counterexample might be spurious. Adding such a flag is certainly helpful, and I was considering to do exactly that, but you're obviously faster. Anyway, Tobias and me briefly discussed to reduce the number of linarith messages dramatically as most counterexamples are actually none. This will be addressed by us in the near future. Cheers, Sascha ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
>> you get the warning >> >> ### Metis: Unused theorems: "List.map.simps_2" >> >> which is strange because in Metis's code that warning is only printed if >> "verbose" is true. Is "Proof.map_context" not the thing I should be using? > > Proof.map_context is right, also the use of the context later on, as far as I > can see in the sources. > > In fact, I cannot reproduce the above problem in Isabelle/0d78c8d31d0d. OK, I now understand what went wrong. I have a special hackish setup for loading Metis and Sledgehammer, which I often use without even thinking about it, and the problem was related to that. I'm glad the issue doesn't exist after all -- it's been on my TODO list for several months now. ;) This motivates me to attack the "linarith" problem. If nobody objects, I'll call the property "linarith_verbose" and have it on by default (for compatibility) but off in "try_methods" and "try". I've also taken the liberty to reword the "counterexample trace" message to make it clear that the counterexample might be spurious. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
On Sun, 26 Jun 2011, Jasmin Christian Blanchette wrote: Now, this all sounds well and good, but there is a little glitch. In "try_methods.ML" the line val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false) is meant to tell Metis to be quiet, but somehow it is ignored. If you do lemma "map f [] = []" using map.simps try_methods you get the warning ### Metis: Unused theorems: "List.map.simps_2" which is strange because in Metis's code that warning is only printed if "verbose" is true. Is "Proof.map_context" not the thing I should be using? Proof.map_context is right, also the use of the context later on, as far as I can see in the sources. In fact, I cannot reproduce the above problem in Isabelle/0d78c8d31d0d. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
Am 24.06.2011 um 11:32 schrieb Lukas Bulwahn: > I only noticed that using "try" you often get a misleading response from > linarith that "linarith found a counterexample" which beginners might stumble > on. > It might be better to switch off this warning by default (and offer a > configuration to switch it on if it is of interest). I totally agree "try", actually "try_methods", should be silent or succeed, following the Unix tradition. We should add an "linarith_verbose" or "arith_verbose" configuration option to control verbosity, as we have for other tools (e.g. Metis). Whether it's on or off by default isn't for me to decide (I'd vote for "off" unless arith can be sure the counterexample is valid, as it probably could in some cases), but it would be off when "try" is run. Now, this all sounds well and good, but there is a little glitch. In "try_methods.ML" the line val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false) is meant to tell Metis to be quiet, but somehow it is ignored. If you do lemma "map f [] = []" using map.simps try_methods you get the warning ### Metis: Unused theorems: "List.map.simps_2" which is strange because in Metis's code that warning is only printed if "verbose" is true. Is "Proof.map_context" not the thing I should be using? Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
Command completion needs to be context aware to work well. Otherwise it can indeed become a distraction. Tobias Am 24/06/2011 22:01, schrieb Alexander Krauss: Hi all, Now that this topic is already active, here is more: In a small course here at TUM (http://www4.in.tum.de/lehre/vorlesungen/perlen/SS11/) we are also using jedit exclusively for the first time, and I can confirm the observation that it makes it slightly easier for newbies to get started. In particular, the "How can I copy and paste?", "How do I open a file?" questions all go away, since the editor commands/key sequences are less obscure. There are also less installation issues (we have no virtualbox image, but a custom bundle, which I built from a development version). Here are two (minor) issues I noticed, which do get in the way and may be easy to fix: 1) Command completion: This may be one of the features that look nice but are useless in practice and often get in the way: Some frequent commands are prefixes of other rather obscure commands, which will then be suggested by the auto-completion: When I type "apply" and pause for a moment to think, the editor suggests "apply_end", which many users don't even know about. This steals (a) the focus, as I cannot move the cursor up/down at this point and (b) my attention. Another instance, which comes up in an exploratory/teaching context, is the following scenario: lemma "x = y" -- some false conjecture try -- see if it "works" ^ -> counterexample found immediately cursor is here At this point I would like to go up and correct the lemma, but I cannot, since the editor suggests "try_methods" as a completion of "try". I have to press escape first. Of course, in an ideal world, I would not have to type "try" in the first place, but currently this is our way of working. Suggestion: Simply kill completion of commands (not symbols)??? 2) Since entering non-ascii versions of arrows takes two extra keystrokes and some attention, students tend to just use the ascii variants. I don't know if this is good or bad, but when I give them a file for editing that has nice arrows, after editing, it usually has both versions, and I have to explain that they are the same. I principle, this could happen with PG/Emacs too, but it normally wouldn't, because of the automatic substitution. It is a known issue (if an issue at all) that in Isabelle/jEdit it is sometimes necessary to cut-and-paste some lines in order to "synchronize." This behaviour is indeed getting in the way in practice. It works according to the "specification" of the editing model, but What is actually the specification of the editing model? I am just curious here, and if you can explain it quickly, it may give me an intuition of what's happening when something goes "wrong" (i.e., as specified). Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
On Sat, 25 Jun 2011, Clemens Ballarin wrote: Quoting Makarius : In principle everything is possible, but one needs to try hard to minimize "options" and "features". Otherwise it becomes impossible to maintain robustness of the application. There are no proper automated test procedures, which means I usually play through all the important things manually (on 3 platform families). Java provides support for GUI tests through a Robot class, and there are frameworks out there since everybode has this problem. It'll sure be worth investigating automatic testing (student project?). I have heard of such things before, but have not tried anything so far. After a few years working with JVM frameworks I no longer take anything for granted by default. It always requires a lot of extra work to make things work more than half way. What did these people do in all these years with all the ? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
Quoting Makarius : In principle everything is possible, but one needs to try hard to minimize "options" and "features". Otherwise it becomes impossible to maintain robustness of the application. There are no proper automated test procedures, which means I usually play through all the important things manually (on 3 platform families). Java provides support for GUI tests through a Robot class, and there are frameworks out there since everybode has this problem. It'll sure be worth investigating automatic testing (student project?). Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
On Sat, 25 Jun 2011, Lawrence Paulson wrote: Is it possible to restrict command completion to a select collection of commonly used commands? Or to make it the user-configurable? Larry On 24 Jun 2011, at 21:01, Alexander Krauss wrote: Suggestion: Simply kill completion of commands (not symbols)??? In principle everything is possible, but one needs to try hard to minimize "options" and "features". Otherwise it becomes impossible to maintain robustness of the application. There are no proper automated test procedures, which means I usually play through all the important things manually (on 3 platform families). I have already spent a lot of time looking through the existing mechanisms of Java, Swing, jEdit, and make as much sense of it as is feasible at the moment. This needs to continue, of course. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
Is it possible to restrict command completion to a select collection of commonly used commands? Or to make it the user-configurable? Larry On 24 Jun 2011, at 21:01, Alexander Krauss wrote: > Suggestion: Simply kill completion of commands (not symbols)??? ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
On Fri, 24 Jun 2011, Alexander Krauss wrote: Another instance, which comes up in an exploratory/teaching context, is the following scenario: lemma "x = y"-- some false conjecture try -- see if it "works" ^ -> counterexample found immediately cursor is here At this point I would like to go up and correct the lemma, but I cannot, since the editor suggests "try_methods" as a completion of "try". I have to press escape first. Of course, in an ideal world, I would not have to type "try" in the first place, but currently this is our way of working. Suggestion: Simply kill completion of commands (not symbols)??? The inlining of diagnostic commands into the text is awkward in several ways. There should be a completely different way to do it, without intruding the text area in the first place. In general the command language is designed to have completion of some form. This explains the relatively long and explicit command names, e.g. "definition", "theorem" instead of cryptic abbreviations. The physical mechanism to be used is a different question. jEdit alone has about 5 such mechanisms as part of the main editor framework or plugins, and in the greater Java/Swing world there are some more such frameworks. What you see right now is the builtin auto-completion of jEdit/Sidekick. The regular jEdit completion/abbreviation mechanism needs to be requested explicitly by certain command sequences, and it is not configured by default. One needs to make a market survey to find really good mechanisms that do not intrude the editing process (as in newer Proof General versions, for example). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
On Fri, 24 Jun 2011, Alexander Krauss wrote:
It is a known issue (if an issue at all) that in Isabelle/jEdit it is
sometimes necessary to cut-and-paste some lines in order to
"synchronize."
This behaviour is indeed getting in the way in practice. It works
according to the "specification" of the editing model, but
What is actually the specification of the editing model? I am just
curious here, and if you can explain it quickly, it may give me an
intuition of what's happening when something goes "wrong" (i.e., as
specified).
The incremental parsing process tries to recognize "command spans", while
preserving already recognized commands. This means command fragments
inside an unbalanced quoted entity (" or {*) get "stuck". The copy-paste
workaround forces a complete reparse. There is also an add-on heuristic
to reparse the current line completely.
The plan is to give up all the special arrangements and reparse the
visible area eagerly, while treating the invisible one lazyly.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
Hi all, Now that this topic is already active, here is more: In a small course here at TUM (http://www4.in.tum.de/lehre/vorlesungen/perlen/SS11/) we are also using jedit exclusively for the first time, and I can confirm the observation that it makes it slightly easier for newbies to get started. In particular, the "How can I copy and paste?", "How do I open a file?" questions all go away, since the editor commands/key sequences are less obscure. There are also less installation issues (we have no virtualbox image, but a custom bundle, which I built from a development version). Here are two (minor) issues I noticed, which do get in the way and may be easy to fix: 1) Command completion: This may be one of the features that look nice but are useless in practice and often get in the way: Some frequent commands are prefixes of other rather obscure commands, which will then be suggested by the auto-completion: When I type "apply" and pause for a moment to think, the editor suggests "apply_end", which many users don't even know about. This steals (a) the focus, as I cannot move the cursor up/down at this point and (b) my attention. Another instance, which comes up in an exploratory/teaching context, is the following scenario: lemma "x = y"-- some false conjecture try -- see if it "works" ^ -> counterexample found immediately cursor is here At this point I would like to go up and correct the lemma, but I cannot, since the editor suggests "try_methods" as a completion of "try". I have to press escape first. Of course, in an ideal world, I would not have to type "try" in the first place, but currently this is our way of working. Suggestion: Simply kill completion of commands (not symbols)??? 2) Since entering non-ascii versions of arrows takes two extra keystrokes and some attention, students tend to just use the ascii variants. I don't know if this is good or bad, but when I give them a file for editing that has nice arrows, after editing, it usually has both versions, and I have to explain that they are the same. I principle, this could happen with PG/Emacs too, but it normally wouldn't, because of the automatic substitution. It is a known issue (if an issue at all) that in Isabelle/jEdit it is sometimes necessary to cut-and-paste some lines in order to "synchronize." This behaviour is indeed getting in the way in practice. It works according to the "specification" of the editing model, but What is actually the specification of the editing model? I am just curious here, and if you can explain it quickly, it may give me an intuition of what's happening when something goes "wrong" (i.e., as specified). Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
On Fri, 24 Jun 2011, Christian Sternagel wrote: It is a known issue (if an issue at all) that in Isabelle/jEdit it is sometimes necessary to cut-and-paste some lines in order to "synchronize." Some students found this unexpected or even weren't able to solve exercises in the beginning since they didn't know that the solution was cutting and pasting. After I told them, everything went fine. This behaviour is indeed getting in the way in practice. It works according to the "specification" of the editing model, but that needs improvement. Some weeks ago I've got some new ideas for the near future: take the existing ways of jEdit to expose or hide parts of the text as hints of what needs to be reparsed and rechecked by the prover. The "folding" and "narrowing" of jEdit could then be used effectively to mark the spots where updates happen frequently, while other parts will be left untouched. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
On 06/24/2011 01:37 PM, Makarius wrote: On Fri, 24 Jun 2011, Lukas Bulwahn wrote: Johannes Hoelzl and me, gave a two-and-half-hour tutorial to Isabelle at a workshop meeting of PhD students in computer science in Dagstuhl (cf. http://www.model.in.tum.de/um/vernetzungstreffen/). Thanks for the feedback. I would like to add the page of a recent course of ours at Paris: http://www.lri.fr/~wenzel/Isabelle2011-Paris/ where we were using the Isabelle/jEdit IDE of official Isabelle2011. The feedback was quite positive even with this old version. My general impression is that the "first contact" with Isabelle has become much easier. Things are still lacking for power users, but there has been quite some progress in the past few months. I have already reworked the rendering in the editor substantially, and are now about to revise the interaction model again to burn less CPU cycles. This reminds me that I also wanted to give feedback concerning Isabelle/jEdit. In a recent course (using Isabelle2011) http://cl-informatik.uibk.ac.at/teaching/ss11/eve/ I initially introduced students to GNU Emacs + Proof General as well as jEdit (as possible Isabelle interfaces) and then let them freely choose their preferred interface. Almost all students (except those that where using Emacs already heavily before) exclusively used jEdit after a while. It is a known issue (if an issue at all) that in Isabelle/jEdit it is sometimes necessary to cut-and-paste some lines in order to "synchronize." Some students found this unexpected or even weren't able to solve exercises in the beginning since they didn't know that the solution was cutting and pasting. After I told them, everything went fine. Overall also in this course the feedback was quite positive. chris Overall, we got a positive feedback from many participants. Working with the interaction model of Isabelle/jEdit seemed not to pose any problem for the students and we had no crash or unexpected behaviour with the current version. Good to hear. If you do encounter unexpected behaviour, just tell me so that I can address it. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
On Fri, 24 Jun 2011, Lukas Bulwahn wrote: Johannes Hoelzl and me, gave a two-and-half-hour tutorial to Isabelle at a workshop meeting of PhD students in computer science in Dagstuhl (cf. http://www.model.in.tum.de/um/vernetzungstreffen/). Thanks for the feedback. I would like to add the page of a recent course of ours at Paris: http://www.lri.fr/~wenzel/Isabelle2011-Paris/ where we were using the Isabelle/jEdit IDE of official Isabelle2011. The feedback was quite positive even with this old version. My general impression is that the "first contact" with Isabelle has become much easier. Things are still lacking for power users, but there has been quite some progress in the past few months. I have already reworked the rendering in the editor substantially, and are now about to revise the interaction model again to burn less CPU cycles. Overall, we got a positive feedback from many participants. Working with the interaction model of Isabelle/jEdit seemed not to pose any problem for the students and we had no crash or unexpected behaviour with the current version. Good to hear. If you do encounter unexpected behaviour, just tell me so that I can address it. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Feedback from a Isabelle tutorial
Hello all, this week, we, Johannes Hoelzl and me, gave a two-and-half-hour tutorial to Isabelle at a workshop meeting of PhD students in computer science in Dagstuhl (cf. http://www.model.in.tum.de/um/vernetzungstreffen/). We used Isabelle/jEdit with some latest development snapshot and bundled this as a VirtualBox VM configuration. Setting-up the system (installing VirtualBox, importing the VM configuation) in most cases took less than 10 minutes, which we assisted in the evening the day before the tutorial session. We presented two basic examples, addition on natural number and reversal of lists, and let them work themselves with some guidance to prove one or two lemmas on their own. In the end, Johannes presented a student exercise from a first-semester undergraduate analysis course and how he would solve that with Isabelle to give the PhD students an idea what the system can do and how real proofs are developed and look like and not to leave the impression everything is proved by "induct auto/simp". Overall, we got a positive feedback from many participants. Working with the interaction model of Isabelle/jEdit seemed not to pose any problem for the students and we had no crash or unexpected behaviour with the current version. I only noticed that using "try" you often get a misleading response from linarith that "linarith found a counterexample" which beginners might stumble on. It might be better to switch off this warning by default (and offer a configuration to switch it on if it is of interest). Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
