Email Gateway (Aug 19 2022 at 15:05): Email Gateway (Aug 19 2022 at 15:05):From: Lars Hupel <hupel@in.tum.de>
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
Email Gateway (Aug 19 2022 at 15:06):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Isn’t that as specified? The proofs are skipped, so Cons.hyps won’t be generated in the induct call.
Cheers,
Gerwin
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.
Email Gateway (Aug 19 2022 at 15:06):From: Andrew Boyton <Andrew.Boyton@nicta.com.au>
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
Email Gateway (Aug 19 2022 at 15:07):From: Makarius <makarius@sketis.net>
skip_proofs is one of many add-on features that try to address certain
situations, without telling what that was years ago or what it might be
today. The doc-strings say "skip over proofs (implicit 'sorry')" in
Isabelle/Scala or "Skip over proofs" in Proof.
So what did have have in mind when using it? It might explain the
confusion. Or it might lead to new insight which general principles may
supersede skip_proofs at some point -- and absorb similar or different
features in the usual manner.
Makarius
Email Gateway (Aug 19 2022 at 15:09):From: Makarius <makarius@sketis.net>
Which proof documents actually? When I have this situation, the time is
usually spent on latex (several sequential runs), not the proofs (which
run in parallel anyway).
In the longer run, the document preparation should become part of the
Prover IDE -- but so far it did not worked out due to too many odd options
and "modes" of the system in that particular respect.
Makarius
Email Gateway (Aug 19 2022 at 15:10):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
As historical intention goes, skip_proofs was a hack, AFAIR introduced for Verisoft, to speed up processing of large amounts of proofs for interactive development.
Say for example, you have 20 large theory imports in your chain between the image you are based on and the point where you are editing. Skip_proofs was intended to allow you to get to the current point quickly and without using the equivalent of a small forest in energy heating your office.
It is extremely useful for that, and we have used it extensively in L4.verified as well. It can reduce 2h wait time to 5min.
It remains a hack, though. It is quite likely that there are further unintended side effects.
I’m surprised that latex output works with it at all, for instance. It is even possible in some cases that the theorems you get out of skip_proofs are slightly different to the ones you would get from a normal run.
It would be nice to do skip_proofs properly. For instance, I could imagine that judicious use of futures may supersede the current skip_proofs implementation, but I don’t think it’s a project that we should tackle before the release.
Cheers,
Gerwin
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.
Email Gateway (Aug 19 2022 at 15:11):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
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
Email Gateway (Aug 19 2022 at 15:20):From: Makarius <makarius@sketis.net>
I am trying to do such reforms for years. Eventually it should be all
just one uniform concept to manage forked proofs, potentially with
different priorities and different policies to insist or not insist in
joining them later.
To get there, the usual layers of sediments need to be cleaned up slowly
and steadily. Moreover, one needs to have a clear picture of typical
applicaions, beyond accidental features inherited from the past.
That is why it is important to describe particular situations in a
meaningful way. Often the reports are isomorphic to "I want to use
feature X in the context of Y, but it fails".
Makarius
Last updated: Apr 19 2024 at 20:15 UTC