Re: [isabelle] jEdit apparantly proves False

On Wed, 20 Nov 2013, Peter Lammich wrote:

It seems to work with any diverging command, not only simp.

Thus, a minimal example is to type

 lemma False by (intro TrueE) <RETURN>

and after you typed RETURN, the thing appears proven in jEdit.

I still need to check what actually happens here.

In the meantime just a few hints:

  * jEdit is a plain text editor, it proves nothing.

  * Isabelle/jEdit is a Prover IDE, which gives you some view on the
    interactive document model of Isabelle/Scala, where things really
    happen in conjunction with the Isabelle/ML process.

  * Just like in Proof General Emacs, there is no guarantee that something
    that "looks checked" actually is checked.  In Proof General the
    quick_and_dirty flag is enabled by default, and Isabelle/jEdit
    is likewise relatively bold in favour of performance, instead of
    strictness of checking.

I've occasionally seen very bad drop-outs in the past, when some Swing GUI component was crashing and displaying outdated content, e.g. a solved goal state instead of a failed one.

This does not mean that such things should happen too easily. I do have the ambition to make the Prover IDE appear as correctly as feasible, even though authentic proof checking only happens in batch mode. We have this principle for almost 20 years already: only batch builds really count.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.