Email Gateway (Oct 05 2026 at 23:46): Email Gateway (Oct 05 2026 at 23:46):From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Subject: [isabelle] conditional thy imports in ROOT files in Isabelle2026-RC3
The new handling of theory options in ROOT files (empty theory instead of not loading the theory) is preventing us from applying this kind of pattern:
theories [condition = "SKIP_DUPLICATED_PROOFS", quick_and_dirty, skip_proofs]
"Include_C"
theories
"Include_C"
We’re doing that to speed up development builds significantly when the dependencies of theory Include_C are already checked in other sessions. Of course we do want them to be properly checked for “real” proof check runs when we are not developing and SKIP_DUPLICATED_PROOFS is off.
Have others run into this? What are our options?
Cheers,
Gerwin
Email Gateway (Oct 08 2026 at 19:51):From: Makarius <makarius@sketis.net>
Subject: [isabelle] conditional thy imports in ROOT files in Isabelle2026-RC3
On 06/10/2026 01:46, Gerwin Klein wrote:
The new handling of theory options in ROOT files (empty theory instead of not loading the theory) is preventing us from applying this kind of pattern:
theories [condition = "SKIP_DUPLICATED_PROOFS", quick_and_dirty, skip_proofs]
"Include_C"
theories
"Include_C"We’re doing that to speed up development builds significantly when the dependencies of theory Include_C are already checked in other sessions. Of course we do want them to be properly checked for “real” proof check runs when we are not developing and SKIP_DUPLICATED_PROOFS is off.
That is a very strange pattern, not to call it abuse.
I have occasionally thought about improving "isabelle build" to skip proofs
from theories from imported sessions on demand, but it would require yet
another round of refinement of this increasingly complex tool environment.
That will happen eventually.
For now the main observation is that the re-interpreted "condition" for
theories is conceptually close to old skip_proofs. Thus the following change
on isabelle-release will help on the spot:
changeset: 85780:a06cb1ccadaf
tag: tip
user: wenzelm
date: Thu Oct 08 17:35:04 2026 +0200
files: NEWS etc/options src/Doc/System/Sessions.thy
src/Pure/Build/build.ML src/Pure/Build/resources.ML
src/Pure/Build/resources.scala src/Pure/Isar/toplevel.ML
src/Pure/PIDE/document.ML src/Pure/Thy/thy_conditions.scala
description:
support system option "condition_proofs", which is analogous to "condition",
but for skipping proofs (implicit 'sorry');
This will be in Isabelle2026-RC4, presumably published 14-Oct-2026. Better try
it now from the isabelle-release repository, it tell me if anything else needs
to be refined in this area (where I have spent many weeks recently).
Further note that the above option "quick_and_dirty" is not required for
skip_proofs, but maybe you've had something else in mind.
Makarius
Email Gateway (Oct 09 2026 at 04:43):From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Subject: [isabelle] conditional thy imports in ROOT files in Isabelle2026-RC3
On 9 Oct 2026, at 06:51, Makarius <makarius@sketis.net> wrote:
For now the main observation is that the re-interpreted "condition" for theories is conceptually close to old skip_proofs. Thus the following change on isabelle-release will help on the spot:
changeset: 85780:a06cb1ccadaf
tag: tip
user: wenzelm
date: Thu Oct 08 17:35:04 2026 +0200
files: NEWS etc/options src/Doc/System/Sessions.thy src/Pure/Build/build.ML src/Pure/Build/resources.ML src/Pure/Build/resources.scala src/Pure/Isar/toplevel.ML src/Pure/PIDE/document.ML src/Pure/Thy/thy_conditions.scala
description:
support system option "condition_proofs", which is analogous to "condition", but for skipping proofs (implicit 'sorry');This will be in Isabelle2026-RC4, presumably published 14-Oct-2026. Better try it now from the isabelle-release repository, it tell me if anything else needs to be refined in this area (where I have spent many weeks recently).
Thank you, I had not expected that before the release. This is very welcome and I can confirm that it works for l4v.
A further refinement could be to make skip_proofs visible on the ML side when it is set like this via condition_proofs. Currently, ML code that checks for skip_proofs explicitly, still sees skip_proofs = false. This is not urgent, though, happy to discuss after the release.
Further note that the above option "quick_and_dirty" is not required for skip_proofs, but maybe you've had something else in mind.
The quick_and_dirty was intended for packages like datatype, BNF, etc, which are checking quick_and_dirty explicitly to reduce work. The difference is marginal, though, not worth spending time on. It was a leftover from times when machines were a lot slower.
Cheers,
Gerwin
Email Gateway (Oct 09 2026 at 12:32):From: Makarius <makarius@sketis.net>
Subject: [isabelle] conditional thy imports in ROOT files in Isabelle2026-RC3
On 09/10/2026 06:43, Gerwin Klein wrote:
On 9 Oct 2026, at 06:51, Makarius <makarius@sketis.net> wrote:
For now the main observation is that the re-interpreted "condition" for theories is conceptually close to old skip_proofs. Thus the following change on isabelle-release will help on the spot:
changeset: 85780:a06cb1ccadaf
A further refinement could be to make skip_proofs visible on the ML side when it is set like this via condition_proofs. Currently, ML code that checks for skip_proofs explicitly, still sees skip_proofs = false. This is not urgent, though, happy to discuss after the release.
The current approach does not use skip_proofs at all, but a newly introduced
concept Toplevel.skipped: the overall idea is to separate management of
command execution (by the system) from the execution itself (in user space).
I was tempted to schedule skip_proofs for removal after the release. So we
could already discuss the canonical question now: What are remaining uses of
skip_proofs / Goal.skip_proofs_enabled?
The quick_and_dirty was intended for packages like datatype, BNF, etc, which are checking quick_and_dirty explicitly to reduce work. The difference is marginal, though, not worth spending time on. It was a leftover from times when machines were a lot slower.
OK, this is what I suspected.
Makarius
Email Gateway (Oct 12 2026 at 07:20):From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Subject: [isabelle] conditional thy imports in ROOT files in Isabelle2026-RC3
On 9 Oct 2026, at 23:32, Makarius <makarius@sketis.net> wrote:
On 09/10/2026 06:43, Gerwin Klein wrote:
On 9 Oct 2026, at 06:51, Makarius <makarius@sketis.net> wrote:
For now the main observation is that the re-interpreted "condition" for theories is conceptually close to old skip_proofs. Thus the following change on isabelle-release will help on the spot:
changeset: 85780:a06cb1ccadaf
A further refinement could be to make skip_proofs visible on the ML side when it is set like this via condition_proofs. Currently, ML code that checks for skip_proofs explicitly, still sees skip_proofs = false. This is not urgent, though, happy to discuss after the release.
The current approach does not use skip_proofs at all, but a newly introduced concept Toplevel.skipped: the overall idea is to separate management of command execution (by the system) from the execution itself (in user space).
I was tempted to schedule skip_proofs for removal after the release. So we could already discuss the canonical question now: What are remaining uses of skip_proofs / Goal.skip_proofs_enabled?
We use skip_proofs in the following ways in l4v:
This is for when you are certain the proofs will work, but you have for instance changed a definition that is far away. I think Toplevel.skipped as proposed is likely to work for this, the jEdit toggle just needs to be adapted.
The 2025-2 version of this is here:
https://github.com/seL4/isabelle/commit/a9f7c5724f03586c021b344ac34c415ffd70ffaa
This is for when you are less certain the proofs will work and they need to be re-checked, but you still need to get back quickly. It is almost as fast as pure skip_proofs to return to the previous editing position, but will check proofs eventually. Error behaviour is different to normal proof check mode, because it initially assumes all lemma statements are true. The implementation of this is hacky, which is why we never contributed it back, but we use it almost daily.
This currently uses the Skipped_Proof node and init_skipped_proof in Toplevel, and Proof.global_skip_proof. It introduces its own Goal.defer_proofs_enabled which is modelled on Goal.skip_proofs_enabled. I think this can also be ported to the top-level-only proposal, but I am less sure without actually attempting it.
Not sure if you really want to look at it (like I said, it’s hacky), but the 2025-2 version of this is here:
https://github.com/seL4/isabelle/commit/ac38b545457822ae2d9f4144eb9c97dd34e4453a
fun maybe_cheat_tac ctxt thm =
if (Goal.skip_proofs_enabled ())
then ALLGOALS (Skip_Proof.cheat_tac ctxt) thm
else all_tac thm;
The quick_and_dirty was intended for packages like datatype, BNF, etc, which are checking quick_and_dirty explicitly to reduce work. The difference is marginal, though, not worth spending time on. It was a leftover from times when machines were a lot slower.
OK, this is what I suspected.
For completeness, I should say that we do have a separate use of quick_and_dirty in the C parser, which declares many small records and some very large records. Having quick_and_dirty on for that invocation makes a larger difference (about 4-5 min wall time and 20 min CPU time), but we are planning to use a different mechanism for this (switching on/off the option just around the relevant command, instead of in the ROOT file).
Cheers,
Gerwin
Email Gateway (Oct 12 2026 at 19:44):From: Makarius <makarius@sketis.net>
Subject: [isabelle] conditional thy imports in ROOT files in Isabelle2026-RC3
On 12/10/2026 09:19, Gerwin Klein wrote:
On 9 Oct 2026, at 23:32, Makarius <makarius@sketis.net> wrote:
I was tempted to schedule skip_proofs for removal after the release. So we could already discuss the canonical question now: What are remaining uses of skip_proofs / Goal.skip_proofs_enabled?
We use skip_proofs in the following ways in l4v:
Thank you for the explanations. Some of this will have to be sorted out at a
later stage, to eliminate odd adhoc scheduling of PIDE documents with
intrusion of ancient REPL semantics.
For now, i.e. the Isabelle2026 release, I have converged the new
"condition_proofs" with the old "skip_proofs" to minimized potential problems.
This also fits better with existing uses of Goal.skip_proofs_enabled in
Isabelle/Pure.
See in particular:
changeset: 85806:9dadbd042068
tag: tip
user: wenzelm
date: Mon Oct 12 20:25:18 2026 +0200
files: src/Pure/Build/build.ML src/Pure/Build/resources.ML
src/Pure/Build/resources.scala src/Pure/Isar/toplevel.ML src/Pure/PIDE/document.ML
description:
more conservative treatment of "condition_proofs" (see also a06cb1ccadaf):
better co-existence with historic "skip_proofs", including support for
Goal.skip_proofs_enabled in Isabelle/ML (e.g. see a06cb1ccadaf);
changeset: 85805:5f0eaafb9996
user: wenzelm
date: Mon Oct 12 20:54:39 2026 +0200
files: src/Pure/Isar/proof.ML
description:
proper runtime scope of Interactive.setmp (amending 87548e3da196), e.g.
relevant for "isabelle build -o skip_proofs -o document=pdf";
The next, and hopefully the last release candidate is scheduled for 14-Oct-2026.
Makarius
Last updated: Oct 29 2026 at 04:52 UTC