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
Last updated: Oct 08 2026 at 21:07 UTC