*To*: Julian Brunner <julianbrunner at gmail.com>*Subject*: Re: [isabelle] Track sorry*From*: Makarius <makarius at sketis.net>*Date*: Mon, 7 Apr 2014 15:11:06 +0200 (CEST)*Cc*: Lars Noschinski <noschinl at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAE5E_av9fmSpv=Op==DypD7oj62K1M75tmRh=4JtKSEKAyfsgw@mail.gmail.com>*References*: <53316FAE.6080703@gmail.com> <alpine.LNX.2.00.1403251830020.51729@lxbroy10.informatik.tu-muenchen.de> <5332B6A4.3060303@in.tum.de> <CAE5E_av9fmSpv=Op==DypD7oj62K1M75tmRh=4JtKSEKAyfsgw@mail.gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Sat, 5 Apr 2014, Julian Brunner wrote:

On Wed, Mar 26, 2014 at 12:14 PM, Lars Noschinski <noschinl at in.tum.de> wrote:On 25.03.2014 18:36, Makarius wrote:On Tue, 25 Mar 2014, bnord wrote:is there a tool (or similar) to track which theorems in a development depend in some way upon "sorry"? I've to assess student developments and doing this manually is a pain. ;) I'd imagine an Isabelle/jEdit "plugin".For a quick and dirty check, I usually just use the hypersearch of jEdit, which is one of the big assets of that text editor. The keywords "sorry" and "axiomatization" are the two main things to check. Further note that the Prover IDE is not obliged to be 100% authentic, although it tries its best to be so -- there might be optical illusions even if the system works properly. At the end of the day only batch builds count, with quick_and_dirty = false.This will only tell the user whether all theorems are valid; when grading student exercises it is often valuable to know which theorems can be trusted despite having some (invalid) sorry'd theorem present.

(1) In the Prover IDE, using hypersearch to look at the concrete syntax. (2) In batch mode, by using knowledge about the LCF kernel works.

This will only tell the user whether all theorems are valid; when grading student exercises it is often valuable to know which theorems can be trusted despite having some (invalid) sorry'd theorem present.I second this, I've always found that very useful. Unfortunately, the[!] marker seems to have been removed in one of the recent versions. Idon't know exactly when or even whether it's just me, but I remember itbeing there two years ago, and it's gone now. Unfortunately, the NEWSfile only mentions its introduction.

* Theorem status about oracles and unfinished/failed future proofs is no longer printed by default, since it is incompatible with incremental / parallel checking of the persistent document model. ML function Thm.peek_status may be used to inspect a snapshot of the ongoing evaluation process. Note that in batch mode --- notably isabelle build --- the system ensures that future proofs of all accessible theorems in the theory context are finished (as before).

Makarius

**Follow-Ups**:**Re: [isabelle] Track sorry***From:*Lars Noschinski

**References**:**Re: [isabelle] Track sorry***From:*Julian Brunner

- Previous by Date: [isabelle] 2nd CfP, VERIFY 2014, 8th Verification Workshop, *Abstract Deadline April 17th, 2014*, Focus Theme: Verification Beyond IT Systems
- Next by Date: Re: [isabelle] Track sorry
- Previous by Thread: Re: [isabelle] Track sorry
- Next by Thread: Re: [isabelle] Track sorry
- Cl-isabelle-users April 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