Email Gateway (Aug 22 2022 at 11:32): Email Gateway (Aug 22 2022 at 11:32):From: Rafal Kolanski <xs@xaph.net>
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
Email Gateway (Aug 22 2022 at 11:32):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 11:32):From: Rafal Kolanski <xs@xaph.net>
Hi Andreas,
That's perfect! Thank you!
Sincerely,
Rafal Kolanski
Last updated: Apr 19 2024 at 20:15 UTC