Stream: General

Topic: Reusing session heaps across CI cache restores

view this post on Zulip Amar Akshat (Jun 08 2026 at 17:43):

Hi all, question about isabelle build and CI caching.

I have a GitHub Actions job that builds a heavy session dependency cone:
AFP Berlekamp_Zassenhaus + Word_Lib + a small vendored session, around 50 min cold.

To avoid rebuilding on every run, I set ISABELLE_HOME_USER inside the workspace and cache it across runs, including the AFP/component directories. On a later run the cache restores cleanly. Sources and absolute paths appear identical; only mtimes differ. But isabelle build -bv <Session> still rebuilds the whole dependency cone instead of reusing the restored heaps.

What I’m trying to understand:

  1. Is isabelle build’s up-to-date check expected to be content/path based, so restored heaps should be reused if sources and paths are identical?

  2. Or are mtimes, component registration state, build logs, session database identity, etc. part of the validity check in a way that can legitimately force a rebuild after a CI cache restore?

  3. Is there an idiomatic/supported way to make session images reusable across CI runs? For example, should I cache a particular ISABELLE_HEAPS layout, use a prebuilt component, avoid changing ISABELLE_HOME_USER, or something else?

One possible culprit: my setup re-runs

isabelle components -u <afp>/thys
isabelle components -u <saw-lib>

on every CI run before building. Could repeated component registration perturb the session graph or invalidate the restored build state?

The concrete repo is here if useful:
https://github.com/amarshat/pqc-assay

The relevant setup script is scripts/setup_isabelle_cryptol.sh, and the GitHub Actions verify job does the caching.

view this post on Zulip Fabian Huch (Jun 10 2026 at 14:55):

Digests depend only on content and options. To make them resuable in a CI system I would pull them into a database and materialize them when needed, like how it is done for the distributed build already.

view this post on Zulip Amar Akshat (Jun 10 2026 at 23:08):

Thanks - this sent me to actually measure it. Locally, session-heap reuse is exactly content+options digest based: it survives a tar round-trip of the store, and even survives touching the AFP sources to newer than the heaps (no rebuild). So mtimes/paths aren't the issue.

Turns out my CI just wasn't persisting the right thing - I was caching only the toolchain dir, not ~/.isabelle/.../heaps (the heaps + per-session build database).
Once I cache that store, the warm path reuses the AFP/Cryptol cone instead of rebuilding. Confirming on the actual runner now.

For a single runner that on-disk store seems sufficient; I can see why the build_process database is the right answer once you're distributing across machines. Thanks for the pointer.

view this post on Zulip Amar Akshat (Jun 11 2026 at 09:39):

Confirmed on the runner: persisting the heap store makes the warm build reuse the AFP/Cryptol cone - the "Build AFP + Cryptol" step dropped from ~60–90 min to 21 seconds, total verify run ~3 min. As you said, it's purely the content+options digest; my CI just wasn't persisting ~/.isabelle/.../heaps (I was caching only the toolchain dir).
Config: https://github.com/amarshat/pqc-assay/blob/main/.github/workflows/verify.yml - and the warm run showing the 21s step: https://github.com/amarshat/pqc-assay/actions/runs/27334580624

Thanks again - for a single runner the on-disk store is enough.

Last updated: Jun 12 2026 at 11:44 UTC