Add ccache support to Dockerfiles and build workflow

[lukovdm]

The PR CI actions where slowing me down quite a bit thus I investigated a bit into how it could be sped up. I added caching of the homebrew downloads and added ccache in all builds with a github cached ccache.

[lukovdm]

It seems like using ccache together with precompiled headers (PCH) does not really work. You get a really low ccache hit rate like this:

Cacheable calls:                     57 / 649 ( 8.78%)
  Hits:                              57 /  57 (100.0%)
    Direct:                          57 /  57 (100.0%)
  Misses:                             0 /  57 ( 0.00%)
Uncacheable calls:                  592 / 649 (91.22%)
  Could not use precompiled header: 592 / 592 (100.0%)

I have done a quick benchmark (on a 24 core machine) of turning PCH on and off with and without a warm cache. These are the results:

PCH	cache state	build (s)	cacheable calls	hits	misses	uncacheable calls
on	cold	178.33	57/649(8.78%)	0/57(0.00%)	57/57(100.0%)	592/649(91.22%)
on	warm	172.48	57/649(8.78%)	57/57(100.0%)	0/57(0.00%)	592/649(91.22%)
off	cold	200.38	648/648(100.0%)	0/648(0.00%)	648/648(100.0%)	0
off	warm	56.97	648/648(100.0%)	648/648(100.0%)	0/648(0.00%)	0

So with a cold cache disabling PCH costs time. But with a warm cache all compile calls actually hit the cache, and it is thus much faster. Most time was taken up by the dependencies.

For the GitHub actions CI we would always have a warmish cache, and thus it seems like it would be worth it to me to disable PCH for them.

For people building storm themselves I don't know, it depends on how much we value cold cache builds versus warm cache builds.

[volkm]

Nice idea @lukovdm! I think it is good to try to decrease the building times in the CI.
I like the idea of using a cache to have incremental builds.

Some thoughts:

• I would probably opt to use the caching for PRs and branches other than master. That way, all feature branches have faster CI by incrementally building new commits. Seeing that most PRs nowadays have multiple iterations, this would decrease the computation times. On the master branch, I would still build from scratch to catch potential issues not detected by the incremental build. In general, I would also run more tests on the master than on the feature branch.
• Interesting to see that PCH have such a negative influence on the cache. Could this be somehow mitigated? I briefly googled and it seems that it should not be a general issues (at least people implemented fixes throughout the years).
• Do you see any cache issues with dependencies? On my local machine, it sometimes feels to me that a large rebuild is triggered even though not much has changed. I suspect a bit that some of the 3rdpary dependencies could have an influence.
• In CMake, I suggest to add a new option STORM_COMPILE_WITH_PCH which allows to enable/disable the PCH. This is similar to STORM_COMPILE_WITH_CCACHE. Edit: According to precompiled headers #451 there is cmake_disable_precompiled_headers
• Why are all the includes necessary now? It is interesting that it compiled before.

[lukovdm]

Thanks for the questions.

• The includes are necessary I think because https://github.com/lukovdm/storm/blob/fc5220f3e1920dab08030f4d47c00111e1883250/CMakeLists.txt#L315 includes several headers for many files.
• About the PCH, looking at these docs, using PCH and pragma once might be the issue: https://ccache.dev/manual/latest.html#_precompiled_headers. But I did not want to change pragma once in all files. I tested a several things to get PCH and ccache to properly work but could not do it.
• The flag and branch things I can implement.
• I have not noticed anything with the dependencies, but they are the slowest part of a warm cache clean build folder build now.

Also, some GitHub workflows are not properly caching yet, but the once that are, are running in 4-10 minutes.

[volkm]

Thanks for the detailed answers.

One thing I noticed looking at the latest CI run, for example here is that carl and sylvan seem to be rebuild each time. I think that might be due to the way how we configure the fetchcontent.

[sjunges]

Thanks Luko!

Do you have any profiling of the compilation process with a warm start? We do have some ways of profiling storm compilation processes and it would be nice to know where the time is lost.

I second Matthias: For the main branch, PCH seems preferable, in particular as I care about the cold start compile time a lot. (Although this is shifting with more people using binaries).
Should we use cmake_disable_precompiled_headers in the STORM_DEVELOPER mode?

If your goal is to speedup the CI, I think it also really gets time to exclude some tests --, for runs where the CI is failing during compilation, that probably doesn't matter that much, but we sometimes have to wait for CI as we cannot run too many things in parallel...

[volkm]

I opened a discussion for a CI revision #894

[volkm]

Related to #763

[lukovdm]

I got some profiles.

• Ignoring the dependencies, with a cold cache, with PCH takes 3m40s, without PCH takes 4m25s. This difference is caused by most files taking a few extra seconds, not one that takes way longer.
• A warm Ccache and PCH results in all dependencies except spot to be compiled basically instantly. Spot is not affected.
• Warm ccache without pch is dominated by spot:

[volkm]

Thanks for the investigation. Looks like spot will be recompiled any time. I think we should figure out why this is happening and whether we can prevent this.

[lukovdm]

I got spot to use ccache and this helped quite a bit again. These benchmarks also have ass tests enabled:

pch	cache_state	build_seconds	cacheable_calls	hits	misses	uncacheable_calls
off	cold	331.26	1558/2004(77.74%)	81/1558(5.20%)	1477/1558(94.80%)	446/2004(22.26%)
off	warm	22.46	1528/1961(77.92%)	1528/1528(100.0%)	0/1528(0.00%)	433/1961(22.08%)
on	cold	286.60	526/2007(26.21%)	24/526(4.56%)	502/526(95.44%)	1481/2007(73.79%)
on	warm	239.90	496/1964(25.25%)	496/496(100.0%)	0/496(0.00%)	1468/1964(74.75%)

And warm cache with PCH off:

[sjunges]

Ok, what I gather from this are a few questios:

• The tests are still really slow. I know I never optimized for them, but why do they not profit from the cache.
• I wonder whether there is more that can be compiled while spot is being built.
• Spot configure seems to be one of the main bottlenecks.

[sjunges]

Regarding spot: We could

1. use system-versions of spot again
2. or we could cache the configure step? (autotools supports cache for the configure step).
3. There also seem to be a few a configure options (such as disabling python bindings) which probably are useful.

[volkm]

• The time for the tests could be mostly the linking time? But ideally they do not need to be rebuild if nothing changed.
• The storm CMake target requires the resources target which contains spot. Other resources such as Cudd, sylvan can be build in parallel with Spot, but Spot takes significantly longer than those.
• The Python bindings should already be disabled.

Things to try:

• System version of Spot: we could install spot via homebrew and try to install the Debian-based packages for Debian and Ubuntu (https://spot.lre.epita.fr/install.html). We currently only use preinstalled Spot in the Docker storm-dependencies.
• Caching the configuration steps could be a good option. But in principle, the reconfiguration should only be run if things changed anyway. So it would be good to figure out why it is reconfigured in the first place.

[volkm]

The PCH changes were part of the separate #974 to clean up this PR a bit.

[Copilot]

Copilot encountered an error and was unable to review this pull request. You can try again by re-requesting a review.

[Copilot]

Pull request overview

Copilot reviewed 16 out of 17 changed files in this pull request and generated 7 comments.

Suppressed comments (8)

src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp:643

• These #pragma GCC diagnostic directives should be guarded to avoid toolchains that don’t recognize the warning group (notably Clang warninging on unknown warning groups under -Werror/-Wunknown-warning-option). Consider wrapping them in a compiler/version check (e.g., GCC-only and __GNUC__ >= 15) so the suppression only applies where needed.

// GCC 15 raises a false positive -Wfree-nonheap-object when compiling SparseDtmcEliminationModelChecker
// with GMP rational functions (STORM_USE_CLN_RF=OFF) in Release mode: the inlined std::vector destructor
// for MatrixEntry<..., RationalFunction<..., GMP>> is incorrectly flagged. Not a real memory error.
// See https://gcc.gnu.org/bugzilla/show_bug.cgi?id=108846
#pragma GCC diagnostic push
#pragma GCC diagnostic ignored "-Wfree-nonheap-object"

src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp:884

• These #pragma GCC diagnostic directives should be guarded to avoid toolchains that don’t recognize the warning group (notably Clang warninging on unknown warning groups under -Werror/-Wunknown-warning-option). Consider wrapping them in a compiler/version check (e.g., GCC-only and __GNUC__ >= 15) so the suppression only applies where needed.

#pragma GCC diagnostic pop

src/storm-parsers/parser/SpiritParserDefinitions.h:10

• This adds a conditional #pragma clang diagnostic push but the diff doesn’t show a corresponding conditional #pragma clang diagnostic pop. Without a matching pop under the same #if, the deprecation suppression can leak beyond the intended include scope. Prefer placing a matching pop shortly after the Boost Spirit includes (and under the same #if defined(__clang__) && defined(__apple_build_version__)).

// Boost Spirit's utf8.hpp uses char_traits<ucs4_char> which Apple libc++ (Xcode 26+) deprecated
#if defined(__clang__) && defined(__apple_build_version__)
#pragma clang diagnostic push
#pragma clang diagnostic ignored "-Wdeprecated-declarations"
#endif

resources/3rdparty/include_spot.cmake:70

• In the debug branch, --disable-devel looks inconsistent with the intention of “building Spot in DEBUG mode” (previously this was --enable-devel). If Spot’s debug builds rely on devel mode (common for autotools projects), this may unintentionally reduce debug functionality or change build outputs; consider restoring --enable-devel (or clarifying why devel must be disabled).

            set(STORM_SPOT_FLAGS "${STORM_SPOT_FLAGS};--disable-devel;--disable-debug;--enable-optimizations")
        else()
            message(WARNING "Storm - Building Spot in DEBUG mode.")
            set(STORM_SPOT_FLAGS "${STORM_SPOT_FLAGS};--disable-devel;--enable-debug;--disable-optimizations")
        endif()
        if (CCACHE_FOUND)
            set(STORM_SPOT_FLAGS "${STORM_SPOT_FLAGS};CC=ccache\\ ${CMAKE_C_COMPILER};CXX=ccache\\ ${CMAKE_CXX_COMPILER}")
        endif()

CMakeLists.txt:161

• This unconditionally overrides STORM_COMPILE_WITH_PCH whenever STORM_DEVELOPER is enabled, which can surprise users/CI callers explicitly setting -DSTORM_COMPILE_WITH_PCH=ON. Prefer only setting a default when the variable is not already defined (or making the behavior explicit via a separate option like STORM_DEVELOPER_DISABLE_PCH_BY_DEFAULT).

    # Turn off PCH for faster ccache usage on warm caches. PCH compiled files cannot be properly cached currently.
    # TODO: remove and explicitly set if needed
    set(STORM_COMPILE_WITH_PCH OFF)

.github/workflows/test-mac.yml:57

• This cache key hashes .github/workflows/buildtest.yml, but that workflow is removed in this PR. hashFiles(...) will become empty/constant, weakening invalidation when brew-related behavior changes. Consider hashing relevant current workflow files (or a dedicated dependency manifest) instead.

          key: buildtest-brew-${{ inputs.distro }}-${{ hashFiles('.github/workflows/buildtest.yml') }}

.github/workflows/test-mac.yml:69

• Using ${{ github.run_id }} in the primary cache key guarantees a new cache entry every run. While restore-keys will reuse prior caches, saving with a run-unique key can create excessive cache churn and wastes cache quota. Consider using a stable key (e.g., based on branch/ref + buildType + relevant hashes) and rely on restore-keys for fallback.

          key: buildtest-ccache-macos-${{ inputs.distro }}-${{ inputs.buildType }}-${{ github.run_id }}

.github/workflows/ci-weekly.yml:198

• Brand capitalization: change Github Actions to GitHub Actions for consistency.

          from: Github Actions <you-broke-it@stormchecker.org>

[Copilot]

Warning

Copilot couldn't run its full agentic review because it didn't start before the timeout. Make sure your repository has a runner available, or add a copilot-code-review.yml file specifying one with the runs-on attribute. See the docs for more details.

Pull request overview

Copilot reviewed 20 out of 20 changed files in this pull request and generated 8 comments.