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



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.