CI: fix the guard that skips Apalache on Unicode specs - #228
Merged
Conversation
[ ${{ matrix.unicode }} ] is a single-argument test asking whether the
string is non-empty, which both true and false are, so --skip_apalache
reached every job. No small symbolic model has been checked since
38f89e1 added the flag; f1aaf96 recorded the truthiness the same day
without fixing it.
The two symbolic models above the 30s threshold, APFlashWithMutex and
APGermanData, are smoke-tested rather than checked. That step allows
five seconds and counts a timeout as success, so it only detects
Apalache failing to start, which is all it caught when Apalache raised
its minimum JVM.
Also raise the hard timeout for symbolic models to 120s. APbosco takes
42s on the macOS runners and APtcp 32s, and the 60s that suffices for
TLC does not cover Apalache's JVM and solver startup. Raising it rather
than recording the measured runtimes, because the 30s threshold would
then move these two models into smoke_test_large_models.py, where an
Apalache model degenerates into a check that the launcher boots.
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
lemmy
force-pushed
the
mku-CIApalacheGuard
branch
from
August 18, 2026 16:49
c716b30 to
9f76bc2
Compare
lemmy
marked this pull request as ready for review
August 18, 2026 18:27
There was a problem hiding this comment.
Pull request overview
This PR fixes a CI logic bug that was unintentionally skipping Apalache (symbolic) checks in all matrix jobs, and adjusts the CI timeout to better reflect Apalache’s startup costs so symbolic models can run meaningfully when enabled.
Changes:
- Fixes the bash guard in the CI workflow so
--skip_apalacheis only passed whenmatrix.unicodeis actuallytrue. - Increases the hard timeout for symbolic (Apalache) models in
check_small_models.pyfrom 60s to 120s while keeping TLC models at 60s.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.
| File | Description |
|---|---|
| .github/workflows/CI.yml | Corrects the Unicode matrix guard so Apalache is skipped only for Unicode jobs. |
| .github/scripts/check_small_models.py | Extends hard timeout for symbolic models to account for JVM/solver startup overhead. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
if [ ${{ matrix.unicode }} ]in the "Check small models" step is a single-argument test that asks whether its argument is a non-empty string. Bothtrueandfalseare non-empty, so--skip_apalachehas been passed in every matrix job since 38f89e1 introduced it on 2026-04-25. f1aaf96 noted the same truthiness on the same day but only fixed the Windows launcher that it had been masking.Consequently no small symbolic model has ever been checked by CI. Of the 46 symbolic models in the manifests, only
EinsteinRiddle/Einstein.cfgpredates the flag, and before then the same guard was unconditionally skipping it by name.The only Apalache that CI exercised are the two symbolic models above the 30 second threshold,
APFlashWithMutexandAPGermanData, which go tosmoke_test_large_models.py. That script has no--skip_apalacheoption, allows five seconds, and countsTimeoutExpiredas success. A working Apalache always times out and passes; a broken one exits immediately and fails. That is why Apalache raising its minimum JVM was caught while the model checking itself stayed dormant.Test plan
Draft on purpose. This is being opened to find out what happens when 44 Apalache models run in CI for the first time, in particular:
00:00:01runtimes are realistic, given that Apalache's JVM startup alone exceeds that; models over the 60 second hard timeout are reported as failures bycheck_small_models.pyapalache-mc.batrouting from f1aaf96 works, since it has never executed