Re: [isabelle] Undefined facts in skip_proofs mode



This may be slightly more addressable. You’d have to look at what oops does for skip_proofs and if it can be caught somehow.

Cheers,
Gerwin

On 29 Jul 2014, at 4:04 pm, Andrew Boyton <andrew.boyton at nicta.com.au> wrote:

> The skip-proof semantics are confusing though.
> 
> When processing a theorem, skip_proofs takes a theorem ending with "oops" as a valid theorem, and so if you have two versions
> of a lemma in a single file, one that has been oopsed, and one later with the same name which is "done", then the second one fails
> to be processed, which is unfortunate.
> 
> Andrew
> 
> 
> On 28 Jul 2014, at 11:39 pm, Gerwin Klein <gerwin.klein at nicta.com.au> wrote:
> 
>> Isn’t that as specified? The proofs are skipped, so Cons.hyps won’t be generated in the induct call.
>> 
>> Cheers,
>> Gerwin
>> 
>> On 28 Jul 2014, at 3:21 pm, Lars Hupel <hupel at in.tum.de> wrote:
>> 
>>> Hello,
>>> 
>>> Cornelius and I noticed an oddity when using the system option
>>> "skip_proofs". Consider this simple proof:
>>> 
>>> lemma "(xs::'a list) = xs"
>>> proof (induct xs)
>>> case Cons
>>> thm Cons.hyps
>>> from Cons show ?case by auto
>>> qed auto
>>> 
>>> Notice the "thm" command in the middle. Without "skip_proofs", this goes
>>> through fine. Enabling "skip_proofs" produces this message:
>>> 
>>> *** Undefined fact: "Cons.hyps" (line 8 of
>>> "~/tmp/Skip_Proof/Skip_Proof.thy")
>>> *** At command "thm" (line 8 of "~/tmp/Skip_Proof/Skip_Proof.thy")
>>> 
>>> I have attached a session demonstrating the difference. Run with
>>> 
>>> $ isabelle build -d . -v Skip_Proof
>>> 
>>> Reproducible in all official releases since 2013-2.
>>> 
>>> Cheers
>>> Lars
>>> <skip_proofs.zip>
>> 
>> 
>> ________________________________
>> 
>> The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
>> 
> 





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