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



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.

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.