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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and