*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Undefined facts in skip_proofs mode*From*: Gerwin Klein <Gerwin.Klein at nicta.com.au>*Date*: Thu, 31 Jul 2014 00:15:31 +0000*Accept-language*: en-AU, en-US*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>, Lars Hupel <hupel at in.tum.de>, Cornelius Diekmann <c.diekmann at googlemail.com>*In-reply-to*: <alpine.LNX.2.00.1407292003190.58841@lxbroy10.informatik.tu-muenchen.de>*References*: <53D64E5A.60405@in.tum.de> <alpine.LNX.2.00.1407292003190.58841@lxbroy10.informatik.tu-muenchen.de>*Thread-index*: AQHPqmduiaMw5T2XSkC4TS4nZ2yo7Ju2tEGAgAH4YgA=*Thread-topic*: [isabelle] Undefined facts in skip_proofs mode

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 On 30 Jul 2014, at 4:10 am, Makarius <makarius at sketis.net> wrote: > On Mon, 28 Jul 2014, Lars Hupel wrote: > >> Cornelius and I noticed an oddity when using the system option "skip_proofs". > > 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 > ________________________________ 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.

**References**:**[isabelle] Undefined facts in skip_proofs mode***From:*Lars Hupel

**Re: [isabelle] Undefined facts in skip_proofs mode***From:*Makarius

- Previous by Date: Re: [isabelle] Isabelle2014-RC1: defaults for (co)datatype selectors
- Next by Date: Re: [isabelle] Undefined facts in skip_proofs mode
- Previous by Thread: Re: [isabelle] Undefined facts in skip_proofs mode
- Next by Thread: [isabelle] Proof_Context abstraction
- Cl-isabelle-users July 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list