Skip to content

Commit

Permalink
fix(test): correctly scrub coq and coq/theories (#10657)
Browse files Browse the repository at this point in the history
In `[^\s\f]*`, the `\` is interpreted literally, matching a backslash
character. Instead we use `[:space:]` which corresponds to `\s`, but
works in a `[]` context.

In addition, we have to fix the pattern so that it only matches
directories that end with `coq` or `coq/theories`, otherwise it replaces
too many directories and `$TESTCASE_ROOT` gets eaten.

This has the nice benefit of making the coq test suite work under nix,
where `coq/theories` is installed elsewhere.

Signed-off-by: Etienne Millon <me@emillon.org>
  • Loading branch information
emillon committed Jun 19, 2024
1 parent 3d6d55a commit 172566e
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 3 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ Now we check the flags that were passed to coqdep and coqc:
$ tail -4 A/_build/log | head -2 | ../scrub_coq_args.sh
coqdep
-boot
-R $TESTCASE_ROOT/lib/coq/theories Coq
-R coq/theories Coq
-Q $TESTCASE_ROOT/lib/coq/user-contrib/B B
-R . A -dyndep opt -vos a.v >
_build/default/.A.theory.d
Expand All @@ -67,7 +67,7 @@ Now we check the flags that were passed to coqdep and coqc:
-nI lib/coq-core/kernel
-nI .
-boot
-R $TESTCASE_ROOT/lib/coq/theories Coq
-R coq/theories Coq
-Q $TESTCASE_ROOT/lib/coq/user-contrib/B B
-R . A
a.v
3 changes: 2 additions & 1 deletion test/blackbox-tests/test-cases/coq/scrub_coq_args.sh
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,8 @@ sed 's/ -Q/\f-Q/g' | # new line for each -Q
sed 's/ -w/\f-w/g' | # new line for each -w
sed 's/ -boot/\f-boot/g' | # new line for each -boot
sed 's/ -native-compiler /\f-native-compiler /g' | # new line for each -native-compiler
sed 's/-R [^\s\f]*coq/-R coq/g' | # scrub -R with coq
sed 's/-R [^[:space:]]*coq /-R coq /g' | # scrub -R with coq
sed 's#-R [^[:space:]]*coq/theories #-R coq/theories #g' | # scrub -R with coq/theories
sed 's/-I [-A-Za-z0-9\/_\.]*lib\//-I lib\//g' | # scrub -I with lib/
sed 's/-nI [-A-Za-z0-9\/_\.]*lib\//-nI lib\//g' | # scrub -nI with lib/
sed 's/\(-R [^\f]* [^\f]*\) \(.*\)/\1\f\2/g' | # new line after each -R
Expand Down

0 comments on commit 172566e

Please sign in to comment.