Skip to content

Commit 2c5f4ad

Browse files
hanno-beckermkannwischer
authored andcommitted
nix: Anchor HOL-Light shellHook to repo root, not $PWD
The holLightShellHook set PROOF_DIR (and thus IMPORTS_DIR) from $PWD, which is whatever directory the user ran `nix develop` from. Entering the shell from a subdirectory (e.g. proofs/cbmc/) caused PROOF_DIR to resolve to a non-existent nested path, and the .imports/ directory plus its `mldsa_native` / `s2n_bignum` symlinks were created under that wrong location -- with `mldsa_native` pointing at a path that does not exist. Resolve the repo root via `git rev-parse --show-toplevel` (matching the pattern already used in nix/hol_light/hol-server.sh), with a $PWD fallback for non-git invocations, so PATH / PROOF_DIR / IMPORTS_DIR are stable regardless of the invocation cwd. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
1 parent 429b66a commit 2c5f4ad

1 file changed

Lines changed: 7 additions & 2 deletions

File tree

flake.nix

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -44,8 +44,13 @@
4444
];
4545
};
4646
holLightShellHook = ''
47-
export PATH=$PWD/scripts:$PATH
48-
export PROOF_DIR="$PWD/proofs/hol_light"
47+
# Resolve the repo root independently of the directory from which
48+
# `nix develop` was invoked, so that PROOF_DIR / IMPORTS_DIR always
49+
# point at the real proofs/hol_light tree (and .imports is not
50+
# created in a spurious subdirectory-nested path).
51+
REPO_ROOT="$(git rev-parse --show-toplevel 2>/dev/null || echo "$PWD")"
52+
export PATH="$REPO_ROOT/scripts:$PATH"
53+
export PROOF_DIR="$REPO_ROOT/proofs/hol_light"
4954
# Namespaced imports root for HOL-Light proofs.
5055
# See scripts/check-hol-light-imports for the enforced rule.
5156
export IMPORTS_DIR="$PROOF_DIR/.imports"

0 commit comments

Comments
 (0)