test: copy ver_clash test data to temp dir before modifying (#13134)

Avoids git/(especially) jj thinking the files have vanished from the
root repo
This commit is contained in:
Sebastian Ullrich 2026-03-27 11:25:58 +01:00 committed by GitHub
parent 215aa4010b
commit fda4793215
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 12 additions and 9 deletions

1
tests/pkg/ver_clash/.gitignore vendored Normal file
View file

@ -0,0 +1 @@
/work/

View file

@ -1,3 +1 @@
rm -rf DiamondExample-*/.git
rm -rf DiamondExample-*/.lake DiamondExample-*/lake-manifest.json
rm -f DiamondExample-D/produced.out
rm -rf work

View file

@ -18,6 +18,16 @@
# Setup
# ---
./clean.sh
# Copy test data to a working directory to avoid initializing Git repositories
# inside the checked-in source tree. Cleaned at the start so artifacts from a
# failed run remain available for inspection.
WORK_DIR="$PWD/work"
mkdir -p "$WORK_DIR"
cp -r DiamondExample-A DiamondExample-B DiamondExample-C DiamondExample-D lean-toolchain "$WORK_DIR/"
cd "$WORK_DIR"
# Since committing a Git repository to a Git repository is not well-supported,
# We reinitialize the repositories on each test.
@ -42,8 +52,6 @@ init_git() {
set +x
}
./clean.sh
pushd DiamondExample-A
sed_i s/add_left_comm/poorly_named_lemma/ DiamondExampleA/Ring/Lemmas.lean
lake update
@ -107,7 +115,3 @@ capture_fail lake build
check_out_contains 'could not disambiguate the module `DiamondExampleA.Ring.Lemmas`'
popd
# Cleanup
rm -rf DiamondExample-*/.git
rm -rf DiamondExample-*/.lake