Skip to content

Install before building kdist to ensure kdist cache hash does not change#38

Open
mariaKt wants to merge 2 commits into
masterfrom
mk/fix-dockerfile
Open

Install before building kdist to ensure kdist cache hash does not change#38
mariaKt wants to merge 2 commits into
masterfrom
mk/fix-dockerfile

Conversation

@mariaKt
Copy link
Copy Markdown
Contributor

@mariaKt mariaKt commented May 15, 2026

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

@mariaKt mariaKt requested review from F-WRunTime and dkcumming May 15, 2026 19:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants