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