Email Gateway (Feb 17 2022 at 15:13): Email Gateway (Feb 17 2022 at 15:13):From: Fabian Huch <huch@in.tum.de>
When quick_and_dirty mode is enabled, some regular proofs get replaced
with skip proofs in an Isabelle build. For example, the following will
throw an Exception when isabelle build is used (curiously, the
interactive session works just fine, despite the fact that
quick_and_dirty is always active there):
|fun ex :: "'a ⇒ nat" where "ex _ = 0" theorem ex_const: "ex 5 = ex 7"
by auto ML ‹ exception E; if (Thm_Deps.has_skip_proof [@{thm ex_const}])
then raise E else () ›|
I though that while the oracle would be present from the point of the
session graph where quick_and_dirty was enabled, proofs that do not use
it would not have it as a dependency. Am i mistaken?
Also, is there a reason why headless build and interactive session
diverge here?
Fabian
Last updated: Jul 15 2022 at 23:21 UTC