Commit 945e0e8
Install before building kdist to ensure kdist cache hash does not change (#38)
This PR addresses an issue in the Dockerfile where the kdist cache hash
was not what we expected. This was identified due to failures of proofs
that were using the generated image with `Directory does not exist`.
### Problem description
The Docker image had mismatched kdist cache hashes. The Dockerfile ran
`make && pip install .`:
1. `make` (via `uv run`) built kdist targets into cache hash `c7ca3c1`
2. `pip install .` changed the installed packages, causing kdist to
compute a different hash `45ae7da` at runtime
Result: `kdist which kompass.haskell` resolved to `45ae7da`, but the
built targets were in `c7ca3c1`. Proofs failed with `Directory does not
exist`.
### Fix
Swap the order: `pip install .` first, then `kdist build`. This ensures
the build uses the same package state as runtime, producing a consistent
cache hash.
Replace `make` with a direct `kdist -v build kompass.* -j4` call, since:
- `make` runs `check` (flake8, mypy) which is unnecessary in the image —
`test.yml` already exercises `make check`, `make build`, and `make
test-integration` in CI
- `make build` uses `uv run` which creates a separate environment with a
different hash than `pip install`
### Testing
I tested this locally by:
- Built modified image with `docker build`
- Verified single kdist cache (`kdist-45ae7da`) with all kompass targets
- `kdist which kompass.haskell` resolves correctly
- Successfully ran `test_ptoken_domain_data` proof end-to-end
---------
Co-authored-by: devops <devops@runtimeverification.com>1 parent 9351ea2 commit 945e0e8
4 files changed
Lines changed: 5 additions & 5 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
14 | 14 | | |
15 | 15 | | |
16 | 16 | | |
17 | | - | |
18 | | - | |
| 17 | + | |
| 18 | + | |
19 | 19 | | |
20 | 20 | | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | | - | |
| 1 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
4 | 4 | | |
5 | 5 | | |
6 | 6 | | |
7 | | - | |
| 7 | + | |
8 | 8 | | |
9 | 9 | | |
10 | 10 | | |
| |||
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.
0 commit comments