Re: [isabelle] jEdit apparantly proves False



On Wed, 20 Nov 2013, Makarius wrote:

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.

I confirm that this is a serious problem.  Thanks for reporting this.

I need further digging in the sources and history to work to the bottom of it. I am also getting mentally ready for another release very soon.


Are there any further serious problems in Isabelle2013-1 that nobody has dared to report yet?

It is part of the routine of release management to "disprove" the need for immediate changes in the last moment. The incident here was actually introduced by trying to "fix" the sledgehammer panel at the end of September, just before the Isabelle2013-1-RC phase started (https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-September/004689.html).

This dilemma of accepting or not accepting issues sometimes discourages people to report things, but the principles of empiric science help: plain observations, no "fixes", no "bugs", no nonsense.


	Makarius




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