Re: [isabelle-dev] NEWS: more informative errors in lazy enumerations
On Fri, 23 Nov 2012, Lars Noschinski wrote: On 20.11.2012 16:05, Makarius wrote: What might happen before the release is a move from Sidekick/completion subplugin, to the new Completion standalone-plugin from the jEdit guys. It depends if their release schedule recovers after the summer break -- I don't see any important activity there since 01-Sep-2012, whicj was the original plan for jEdit 5.0 to be rolled out. It seems to have recovered just half an hour ago. I've updated myself to this jedit-5.0.0 release, and will do so for Isabelle/jEdit when I am sufficiently convinced that it is really stable. BTW, the Completion plugin that lead to this side-thread was a misunderstanding of mine: someone forked it off the Sidekick subplugin some years ago, but it was not updated recently. It adds a few features, such as immediate completion without pupup, but also some problems. The "completion service" is forked as independent thread, but that has to access the mutable buffer to read its content and potentially some GUI components. So it is the usual problem of Scylla and Charybdis in concurrent programming with mutable state: lock too little and hope for the best (that the user is typing slowly), or lock too much and lock-up the application in the worst case. Mutability sucks ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: more informative errors in lazy enumerations
On 20.11.2012 16:05, Makarius wrote: What might happen before the release is a move from Sidekick/completion subplugin, to the new Completion standalone-plugin from the jEdit guys. It depends if their release schedule recovers after the summer break -- I don't see any important activity there since 01-Sep-2012, whicj was the original plan for jEdit 5.0 to be rolled out. It seems to have recovered just half an hour ago. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: more informative errors in lazy enumerations
On Tue, 20 Nov 2012, Tjark Weber wrote: On Tue, 2012-11-20 at 15:24 +0100, Makarius wrote: I have many more things on my list to improve the completion mechanism, before such a detail would be considered again. A huge step forward, in my humble opinion, would be context-sensitive completion. For instance, I would ideally like the IDE to figure out whether I am typing "le" to obtain "lemma" or "≤". If this works well, one could then also consider completion for methods, theorem names, logical constants, and whatnot. Yes, this is one of the things on the list (not for the coming release, though). What might happen before the release is a move from Sidekick/completion subplugin, to the new Completion standalone-plugin from the jEdit guys. It depends if their release schedule recovers after the summer break -- I don't see any important activity there since 01-Sep-2012, whicj was the original plan for jEdit 5.0 to be rolled out. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: more informative errors in lazy enumerations
On Tue, 2012-11-20 at 15:24 +0100, Makarius wrote: > I have many more things on my list to improve the completion mechanism, > before such a detail would be considered again. A huge step forward, in my humble opinion, would be context-sensitive completion. For instance, I would ideally like the IDE to figure out whether I am typing "le" to obtain "lemma" or "≤". If this works well, one could then also consider completion for methods, theorem names, logical constants, and whatnot. Anyway, just dreaming. Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: more informative errors in lazy enumerations
On Tue, 20 Nov 2012, Peter Lammich wrote: Wouldn't it be better to just enumerate "censored" completions always last in the completion list? Or are there technical difficulties to do so? There is no technical difficulty, but it would be yet another feature. Every feature is a burden, first to implement it, and then doubly-so in the long-term maintenance. (I spend most of my time on the latter these days.) I have many more things on my list to improve the completion mechanism, before such a detail would be considered again. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: more informative errors in lazy enumerations
On Di, 2012-11-20 at 14:47 +0100, Makarius wrote: > On Wed, 17 Oct 2012, Makarius wrote: > > > Does anybody remember a use of the 'apply_end' command? Many years ago > > it was introduced to help analyse the failure of 'qed', in symmetry to > > 'apply' to break up 'proof' and 'by' steps. That should now work > > without it, just by letting 'qed' crash and looking at the error > > message. Of course, 'apply' has other uses and is not affected here. > > > > Myself I've almost forgotten about 'apply_end', before constantly > > reminded of its existence by the Isabelle/jEdit completion, which > > proposes it when the user tries to write 'apply'. So there is a clear > > motivation to get rid of the old 'apply_end' feature. > > The conclusion of this side-remark is now in Isabelle/599c935aac82: > apply_end stays as before, but there is a way to censor the command > completion table. I am not very fond of censorship, but there is no need > to encumber users by the full complexity of the history of Isar commands > that happens to be still active today. > > Users can lead a happy live over several decades without ever getting > exposed to apply_end. And people who happen to know it and use it > occasionally, can easily type in the keyword as a whole. Wouldn't it be better to just enumerate "censored" completions always last in the completion list? Or are there technical difficulties to do so? > > > 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] NEWS: more informative errors in lazy enumerations
On Wed, 17 Oct 2012, Makarius wrote: Does anybody remember a use of the 'apply_end' command? Many years ago it was introduced to help analyse the failure of 'qed', in symmetry to 'apply' to break up 'proof' and 'by' steps. That should now work without it, just by letting 'qed' crash and looking at the error message. Of course, 'apply' has other uses and is not affected here. Myself I've almost forgotten about 'apply_end', before constantly reminded of its existence by the Isabelle/jEdit completion, which proposes it when the user tries to write 'apply'. So there is a clear motivation to get rid of the old 'apply_end' feature. The conclusion of this side-remark is now in Isabelle/599c935aac82: apply_end stays as before, but there is a way to censor the command completion table. I am not very fond of censorship, but there is no need to encumber users by the full complexity of the history of Isar commands that happens to be still active today. Users can lead a happy live over several decades without ever getting exposed to apply_end. And people who happen to know it and use it occasionally, can easily type in the keyword as a whole. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: more informative errors in lazy enumerations
On Thu, 18 Oct 2012, Andreas Lochbihler wrote: Does anybody remember a use of the 'apply_end' command? Yes, there are two in JinjaThreads (theory J/ProgressThreaded), although they could be fused into the qed. However, I regularly use apply_end when I develop the method call for qed to finish off all the remaining cases after having dealt with the interesting ones. This is more or less the classic use of it. In the rather massive proof here, the two apply_end steps are indeed easily fused into one qed. http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/6881d417d5d5 -- actually I was merely experimented here, and pushed the first half by accident, in the present confusion of the AFP state. It usually saves me reprocessing the first 42 goals when goal 43 needs another intro/simp/elim rule - and I can interactively explore goal 43 immediately. Before I knew about apply_end, I used "case goal_43 thus ?case", but proof methods behave differently there, because the variables are fixed in the context (e.g., tuples are not split automatically). The question on this thread is if the traditional techniques are still relevant. The exploration of a tiny 'qed' script would just be done as 'qed' attempts, without breaking it up into seperate 'apply_end' steps. There is a potential cost for that, since the qed is just one step that needs to be repeated. In the massive example proof it is still below a few seconds, or less. There many more possibilties for the initial refinedment stage before 'proof', with 'apply', 'defer', 'prefer', and potentially proof methods restricted to intervals via the [...] postfix notation. Going back over 42 goals is still an issue right now when using Proof General, with its built-in sequentialism. But that will hopefully be forgotton soon, after more people have retrained their fingers. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: more informative errors in lazy enumerations
>> Does anybody remember a use of the 'apply_end' command? > Yes, there are two in JinjaThreads (theory J/ProgressThreaded), although > they could be fused into the qed. However, I regularly use apply_end > when I develop the method call for qed to finish off all the remaining > cases after having dealt with the interesting ones. I sometimes use a similar pattern, although in my situations a rewrite from apply … proof … to proof … qed … is no problem. So, I personally do not care about, but I acknowledge Andreas' use case. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: more informative errors in lazy enumerations
Hi Makarius, > Side remark: > > Does anybody remember a use of the 'apply_end' command? Yes, there are two in JinjaThreads (theory J/ProgressThreaded), although they could be fused into the qed. However, I regularly use apply_end when I develop the method call for qed to finish off all the remaining cases after having dealt with the interesting ones. It usually saves me reprocessing the first 42 goals when goal 43 needs another intro/simp/elim rule - and I can interactively explore goal 43 immediately. Before I knew about apply_end, I used "case goal_43 thus ?case", but proof methods behave differently there, because the variables are fixed in the context (e.g., tuples are not split automatically). So I opt for keeping apply_end. Andreas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: more informative errors in lazy enumerations
Am 17/10/2012 11:09, schrieb Makarius: > *** ML *** > > * Type Seq.results and related operations support embedded error > messages within lazy enumerations, and thus allow to provide > informative errors in the absence of any usable results. > > > *** General *** > > * More informative error messages for Isar proof commands involving > lazy enumerations (method applications etc.). > > > This refers to Isabelle/bd370af308f0. The latter application means that the > laconic "empty result sequence" should hardly ever happen again in practice -- > it depends on the proof command implementation how nice the error message > becomes. Some more hot spots of the system may be brushed up eventually, but > note that plain tactics are inherently restricted to the classic failure and > backtracking model without error messages. > Excellent! > Side remark: > > Does anybody remember a use of the 'apply_end' command? Many years ago it was > introduced to help analyse the failure of 'qed', in symmetry to 'apply' to > break > up 'proof' and 'by' steps. That should now work without it, just by letting > 'qed' crash and looking at the error message. Of course, 'apply' has other > uses > and is not affected here. I could never remember what apply_end was called and how to apply it although I frequently needed it. I did a quick test of the new behaviour and it does indeed seem to give the information that one really wants: which goals are left over (although it may take some staring at the left overs to figure out where they came from, but that was no better with apply_end). Hence I have no complaint if apply_end goes. Tobias > Myself I've almost forgotten about 'apply_end', before constantly reminded of > its existence by the Isabelle/jEdit completion, which proposes it when the > user > tries to write 'apply'. So there is a clear motivation to get rid of the old > 'apply_end' feature. > > > 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] NEWS: more informative errors in lazy enumerations
On Wed, 17 Oct 2012, Peter Lammich wrote: On Mi, 2012-10-17 at 11:09 +0200, Makarius wrote: *** ML *** * Type Seq.results and related operations support embedded error messages within lazy enumerations, and thus allow to provide informative errors in the absence of any usable results. Cool, no more writing of error messages to the trace buffer when debugging tactics. It probably does not help here: On Wed, 17 Oct 2012, Makarius wrote: note that plain tactics are inherently restricted to the classic failure and backtracking model without error messages. BTW, the trace buffer is only relevant for Proof General in order to get messages past its built-in filtering and priority model of writeln/warning/error. In Isabelle/jEdit you would just use plain writeln by default and then inspect the output or hover over the squiggles in the source. Tracing did get a new meaning in Isabelle/jEdit recently, when I introduced some means to restrict its volume at the very source of the message stream. Thus a simp trace gone wild would just expire the command transaction. For example in Isabelle/b0d6d2e7a522: declare [[simp_trace]] datatype foo = Foo | Bar foo This gives you 0.5 MB of message content -- 184 Tracing messages shown in the Output window if the radio button is enabled -- and finally some error "Tracing limit exceeded: 509725" before any further harm is done. This is a relatively cheap trick to address an ancient problem. I would be interested to hear from early adopters how it works out in hard work. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: more informative errors in lazy enumerations
On Mi, 2012-10-17 at 11:09 +0200, Makarius wrote: > *** ML *** > > * Type Seq.results and related operations support embedded error > messages within lazy enumerations, and thus allow to provide > informative errors in the absence of any usable results. Cool, no more writing of error messages to the trace buffer when debugging tactics. > Side remark: > > Does anybody remember a use of the 'apply_end' command? Many years ago it > was introduced to help analyse the failure of 'qed', in symmetry to > 'apply' to break up 'proof' and 'by' steps. That should now work without > it, just by letting 'qed' crash and looking at the error message. Of > course, 'apply' has other uses and is not affected here. I never knew it, but already got many questions from students whether such a command exists, and I always denied it. Peter ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: more informative errors in lazy enumerations
*** ML *** * Type Seq.results and related operations support embedded error messages within lazy enumerations, and thus allow to provide informative errors in the absence of any usable results. *** General *** * More informative error messages for Isar proof commands involving lazy enumerations (method applications etc.). This refers to Isabelle/bd370af308f0. The latter application means that the laconic "empty result sequence" should hardly ever happen again in practice -- it depends on the proof command implementation how nice the error message becomes. Some more hot spots of the system may be brushed up eventually, but note that plain tactics are inherently restricted to the classic failure and backtracking model without error messages. Side remark: Does anybody remember a use of the 'apply_end' command? Many years ago it was introduced to help analyse the failure of 'qed', in symmetry to 'apply' to break up 'proof' and 'by' steps. That should now work without it, just by letting 'qed' crash and looking at the error message. Of course, 'apply' has other uses and is not affected here. Myself I've almost forgotten about 'apply_end', before constantly reminded of its existence by the Isabelle/jEdit completion, which proposes it when the user tries to write 'apply'. So there is a clear motivation to get rid of the old 'apply_end' feature. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
