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

Hi Rafal,

Have you tried declaring it locally in a context block:

  context notes [[quick_and_dirty]] begin
  lemma foo sorry

It should be reset automatically at the end of the context block, although I have not yet tried this.


On 21/10/15 12:58, Rafal Kolanski wrote:

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

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?


Rafal Kolanski

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