Re: [isabelle] Isabelle2014-RC0: add_assoc hidden, causes error, but proof passes



On 14-07-09 14:40, Peter Lammich wrote:
You have to watch out for the error markers. If there is an error marker
somewhere, you're theory has not passed through. To get an overview of
error markers, use the theory-panel, there you see a tiny red bar on
every theory that has been processed *and* contains an error. Mark the
little check-boxes in the theory-panel to ensure that a theory gets
processed.

Peter,

Okay. I guess I've been conditioned by the PIDE to think that there's something wrong when a proof goal has been proved, yet there's an error in the "apply" or "by" statement.

That normally doesn't happen. Normally, if "apply" or "by" is marked red because of an error, the proof goal isn't proved. But, I can adapt, if I can remember to. In this case, multiple things were going wrong due to the changes with Isabelle2014-RC0.

Thanks,
GB



Additionally, you might see a red mark on the right-hand side of the
text area in the theory file, that can be used to navigate to the error
location in the text buffer, where you see a squiggly red line that
indicates the exact position of the error.


To get a more definite answer on whether your stuff contains errors or
not, you have to use "isabelle build".

--
   Peter



On Mi, 2014-07-09 at 14:11 -0500, Gottfried Barrow wrote:
Hi,

There's "Groups.semigroup_add.add_assoc", followed in Groups.thy by
"hide_fact add_assoc". The "hide_fact" is new in Groups.thy and causes
an error in a proof.

The proof passes even through there's an error 'Undefined fact:
"add_assoc"'. I attach a screen shot showing the error.

Trying to fix that problem, I ran Sledgehammer and have a more serious
problem, which is that Cygwin temp files can't be deleted, which causes
the prover process to terminate. I'll put that that in another email.

Regards,
GB










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