CI: fix the guard that skips Apalache on Unicode specs - #228
Merged
lemmy merged 1 commit intoAug 18, 2026
Merged
Conversation
Copy link
Copy Markdown
Member
Sorry, something went wrong.
[ ${{ 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
c716b30 to
9f76bc2
Compare
August 18, 2026 16:49
lemmy
marked this pull request as ready for review
August 18, 2026 18:27
Copy link
Copy Markdown
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_apalache is only passed when matrix.unicode is actually true.
- Increases the hard timeout for symbolic (Apalache) models in check_small_models.py from 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.
Sorry, something went wrong.
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. Both true and false are non-empty, so --skip_apalache has 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.cfg predates 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, APFlashWithMutex and APGermanData, which go to smoke_test_large_models.py. That script has no --skip_apalache option, allows five seconds, and counts TimeoutExpired as 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: