Conversation
There was a problem hiding this comment.
🟡 Changes recommended
Two critical build issues remain unresolved in the configure invocation and Alpine/musl dependency handling.
Get a fresh assessment by requesting another Copilot review.
Pull request overview
This pull request works around Spot’s libatomic dependency by statically linking libatomic.a in portable non-macOS builds.
Changes:
- Adds conditional static
libatomiclinker flags. - Passes them to Spot’s configure command.
- Adds explanatory comments.
File summaries
| File | Summary |
|---|---|
resources/3rdparty/include_spot.cmake |
Configures Spot to statically link libatomic. Findings: two critical issues (3 and 1 votes) and one nit (1 vote). |
Review details
Suppressed comments (1)
resources/3rdparty/include_spot.cmake:77
- The new comment uses the grammatically incomplete phrase “As fix”; please change it to “As a fix”.
# As fix, we pre-seed LIBS with a statically linked libatomic so that the check already succeeds.
- Files reviewed: 1/1 changed files
- Comments generated: 2
- Review effort level: Lite
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
| # As fix, we pre-seed LIBS with a statically linked libatomic so that the check already succeeds. | ||
| set(STORM_SPOT_LIBS "") | ||
| if (NOT MACOSX AND STORM_PORTABLE) | ||
| set(STORM_SPOT_LIBS "LIBS=-l:libatomic.a") |
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
|
The picture has slightly changed. Since 2 days ago, Ubuntu and Debian Docker images now seem to ship with libatomic. Only the Fedora image is now failing for the wheel CI. Under these circumstances we could also argue that libatomic is assumed to be present (auditwheel at least has this assumption). Then we would not need this PR and could just manually install libatomic in the Fedora image. |
The stormpy wheels have recently started failing, because importing stormpy cannot find libatomic, see e.g. this run.
This library is excluded by auditwheel when repairing the wheel, since
libatomic.so.1is treated as part of the manylinux baseline system and therefore not bundled. However, not all systems ship with libatomic. The Debian/Ubuntu default Docker images for example do not have it and the tests therefore fail.The issue appeared when starting to use Spot 2.16. While Spot does not have libatomic as a new dependency, they fixed the inclusion such that it now is used if the default CMPXCHG16B is missing. As we are using
STORM_PORTABLE=ON, this is missing and our Spot build falls back to libatomic.Long story short: we now explicitly include libatomic as a static library and the stormpy wheels are successful again (tested on my fork).