Re: [isabelle] Setting quick_and_dirty mode for a fragment of a theory only



Hi Andreas,

That's perfect! Thank you!

Sincerely,

Rafal Kolanski

On 21/10/15 22:06, Andreas Lochbihler wrote:
> Hi Rafal,
> 
> Have you tried declaring it locally in a context block:
> 
>   context notes [[quick_and_dirty]] begin
>   lemma foo sorry
>   end
> 
> It should be reset automatically at the end of the context block,
> although I have not yet tried this.
> 
> Best,
> Andreas
> 
> On 21/10/15 12:58, Rafal Kolanski wrote:
>> Hello,
>>
>> We have something we need to sorry temporarily while other toolwork is
>> being fixed, but still want the batch build to go through. The lemma in
>> question is in a local context:
>>
>> context kernel_m begin
>> [...]
>>
>> My attempt which looks like it might work in interactive mode, and I
>> thought worked last night, doesn't work in batch mode:
>>
>> ML {*
>> val old_quick_and_dirty =  let fun get_bool (Config.Bool b) = b in
>>    Config.get @{context} quick_and_dirty_raw |> get_bool
>> end
>> *}
>> local_setup {* Config.put quick_and_dirty true *}
>>
>> [my sorry goes here]
>>
>> local_setup {* Config.put quick_and_dirty old_quick_and_dirty *}
>>
>>
>> When the theory gets processed in batch mode, however:
>>
>> *** Cheating requires quick_and_dirty mode!
>>
>> *** At command "sorry" (line 451 of
>> "~/repos/priority-bitmap/l4v/proof/crefine/Schedule_C.thy")
>>
>> Now obviously I can do declare [[quick_and_dirty=true]], but I don't
>> know how to reset it to the old value after the segment is finished.
>>
>> Any advice?
>>
>> Sincerely,
>>
>> Rafal Kolanski
>>
> 





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