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
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
[isabelle-dev] 0::'a
In jedit, numerals of polymorphic type are no longer tagged with the type variable as a warning. That is an extremely helpful warning not just for beginners, it would be a pity to lose that in jedit. Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] set_comprehension_pointfree simproc losing bounds
Hi Dmitriy,
If you update to changeset 89b118c0c070, the issue should be resolved.
Lukas
On 10/16/2012 01:41 PM, Dmitriy Traytel wrote:
Hi all,
the following produces a Loose bound variable with
Isabelle/4a15873c4ec9
theory Scratch
imports Main
begin
lemma finite {y |y. ∃x. y ∈ f x}
apply simp
oops
end
Fortunately, jedit treats a proof that used to work (but fails now due
to the above) as a sorry, such that I can continue working on whatever
follows in the theory until this issue is fixed.
Best wishes,
Dmitriy
___
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
