chore(docker): pin Clam and its three dependencies to SHAs - #59
Merged
Conversation
clam, sea-dsa and llvm-seahorn were cloned from dev16 and Crab from dev -- four moving branches. The contents of the published image could therefore change with no change in this repository, and the failure mode is the one that just cost a red develop: a build that worked yesterday breaks today for reasons no diff explains. crab@dev moved on 2026-08-21, one day before this. Clam's own crab/extra targets are plain `git clone -b dev<N>` custom commands with nowhere to pass a commit, so pinning means not using them. Its CMakeLists already prefers an in-tree dependency over cloning one, so placing all four by hand works -- and since everything is present before the first configure, the configure/clone/reconfigure sequence collapses to one `cmake ..`. Verified in the image before pushing this time: all four pinned checkouts resolve, and a single configure detects sea-dsa, Crab and llvm-seahorn with no "required but not found" warning. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
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.
Why
Dockerfile.devbuilt Clam from four repositories, all of them tracked on moving branches:seahorn/clamdev16302bf49aseahorn/sea-dsadev16661855a3seahorn/llvm-seahorndev168e7e6c62seahorn/crabdev5c740fccSo the contents of the published image could change with no change in this repository. That is not hypothetical:
crab@devmoved one day before this was written, and #58 was a reddevelopcaused by a Clam build nobody had touched. Pinning turns an upstream break into a deliberate bump with a diff, instead of a build that worked yesterday and fails today for reasons no diff explains.Follow-up to the item flagged in #58.
How
Clam's
crabandextratargets are plaingit clone -b dev<N>custom commands (cmake/{crab,seadsa,llvm-seahorn}-git.cmake) with nowhere to pass a commit — pinning means not using them. Clam'sCMakeLists.txtalready prefers a dependency found in-tree over cloning one, so all four are placed by hand at their pinned SHAs.Two things fall out of that:
git init+fetch --depth 1 <sha>instead ofclone -b <branch>— the only shallow form that takes a commit, so pinning costs no extra history.cmake→--target crab→cmake→--target extra→cmakedance collapses to a singlecmake ...The SHAs are
ARGs, so a bump is a one-line diff, and the comment above them says how to do it.Verified before pushing
Ran the pinned layout and configure inside the image (
-u 0 --cpus=2, exit 0):All four checkouts resolve and one configure detects sea-dsa, Crab and llvm-seahorn — no
required but not found, which is what the previous unpinned recipe emitted before its first two targets ran.The
Build & Push to GHCRjob added in #58 builds this PR'sDockerfile.devwithpush: false, so the full compile and theverifier.assumeinjection probe are checked here, pre-merge.