Re: [isabelle] Track sorry



> 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. I
don't know exactly when or even whether it's just me, but I remember
it being there two years ago, and it's gone now. Unfortunately, the
NEWS file only mentions its introduction.

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.
>
>   -- Lars
>




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