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