Skip to content

Commit 097d2d8

Browse files
rlepigrerlepigre
committed
Improve coq -I argument scrubbing.
Signed-off-by: Rodolphe Lepigre <[email protected]>
1 parent 1372188 commit 097d2d8

File tree

7 files changed

+425
-422
lines changed

7 files changed

+425
-422
lines changed

‎test/blackbox-tests/test-cases/coq/coqtop/coqtop-flags.t/run.t‎

Lines changed: 42 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -12,27 +12,27 @@ The flags passed to coqc:
1212
-native-compiler on
1313
-nI lib/coq-core/kernel
1414
-nI .
15-
-I lib/coq/../coq-core/plugins/btauto
16-
-I lib/coq/../coq-core/plugins/cc
17-
-I lib/coq/../coq-core/plugins/derive
18-
-I lib/coq/../coq-core/plugins/extraction
19-
-I lib/coq/../coq-core/plugins/firstorder
20-
-I lib/coq/../coq-core/plugins/funind
21-
-I lib/coq/../coq-core/plugins/ltac
22-
-I lib/coq/../coq-core/plugins/ltac2
23-
-I lib/coq/../coq-core/plugins/micromega
24-
-I lib/coq/../coq-core/plugins/nsatz
25-
-I lib/coq/../coq-core/plugins/number_string_notation
26-
-I lib/coq/../coq-core/plugins/ring
27-
-I lib/coq/../coq-core/plugins/rtauto
28-
-I lib/coq/../coq-core/plugins/ssreflect
29-
-I lib/coq/../coq-core/plugins/ssrmatching
30-
-I lib/coq/../coq-core/plugins/tauto
31-
-I lib/coq/../coq-core/plugins/tutorial/p0
32-
-I lib/coq/../coq-core/plugins/tutorial/p1
33-
-I lib/coq/../coq-core/plugins/tutorial/p2
34-
-I lib/coq/../coq-core/plugins/tutorial/p3
35-
-I lib/coq/../coq-core/plugins/zify
15+
-I .../plugins/btauto
16+
-I .../plugins/cc
17+
-I .../plugins/derive
18+
-I .../plugins/extraction
19+
-I .../plugins/firstorder
20+
-I .../plugins/funind
21+
-I .../plugins/ltac
22+
-I .../plugins/ltac2
23+
-I .../plugins/micromega
24+
-I .../plugins/nsatz
25+
-I .../plugins/number_string_notation
26+
-I .../plugins/ring
27+
-I .../plugins/rtauto
28+
-I .../plugins/ssreflect
29+
-I .../plugins/ssrmatching
30+
-I .../plugins/tauto
31+
-I .../plugins/tutorial/p0
32+
-I .../plugins/tutorial/p1
33+
-I .../plugins/tutorial/p2
34+
-I .../plugins/tutorial/p3
35+
-I .../plugins/zify
3636
-R coq/theories Coq
3737
-R . minimal
3838
Test.v
@@ -49,26 +49,26 @@ The flags passed to coqtop:
4949
-native-compiler on
5050
-nI lib/coq-core/kernel
5151
-nI $TESTCASE_ROOT/_build/default
52-
-I lib/coq/../coq-core/plugins/btauto
53-
-I lib/coq/../coq-core/plugins/cc
54-
-I lib/coq/../coq-core/plugins/derive
55-
-I lib/coq/../coq-core/plugins/extraction
56-
-I lib/coq/../coq-core/plugins/firstorder
57-
-I lib/coq/../coq-core/plugins/funind
58-
-I lib/coq/../coq-core/plugins/ltac
59-
-I lib/coq/../coq-core/plugins/ltac2
60-
-I lib/coq/../coq-core/plugins/micromega
61-
-I lib/coq/../coq-core/plugins/nsatz
62-
-I lib/coq/../coq-core/plugins/number_string_notation
63-
-I lib/coq/../coq-core/plugins/ring
64-
-I lib/coq/../coq-core/plugins/rtauto
65-
-I lib/coq/../coq-core/plugins/ssreflect
66-
-I lib/coq/../coq-core/plugins/ssrmatching
67-
-I lib/coq/../coq-core/plugins/tauto
68-
-I lib/coq/../coq-core/plugins/tutorial/p0
69-
-I lib/coq/../coq-core/plugins/tutorial/p1
70-
-I lib/coq/../coq-core/plugins/tutorial/p2
71-
-I lib/coq/../coq-core/plugins/tutorial/p3
72-
-I lib/coq/../coq-core/plugins/zify
52+
-I .../plugins/btauto
53+
-I .../plugins/cc
54+
-I .../plugins/derive
55+
-I .../plugins/extraction
56+
-I .../plugins/firstorder
57+
-I .../plugins/funind
58+
-I .../plugins/ltac
59+
-I .../plugins/ltac2
60+
-I .../plugins/micromega
61+
-I .../plugins/nsatz
62+
-I .../plugins/number_string_notation
63+
-I .../plugins/ring
64+
-I .../plugins/rtauto
65+
-I .../plugins/ssreflect
66+
-I .../plugins/ssrmatching
67+
-I .../plugins/tauto
68+
-I .../plugins/tutorial/p0
69+
-I .../plugins/tutorial/p1
70+
-I .../plugins/tutorial/p2
71+
-I .../plugins/tutorial/p3
72+
-I .../plugins/zify
7373
-R coq/theories Coq
7474
-R $TESTCASE_ROOT/_build/default minimal

‎test/blackbox-tests/test-cases/coq/coqtop/coqtop-nested.t/run.t‎

Lines changed: 42 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -19,27 +19,27 @@ Checking that we compute the directory and file for dune coq top correctly
1919
-w -deprecated-native-compiler-option
2020
-w -native-compiler-disabled
2121
-native-compiler ondemand
22-
-I lib/coq/../coq-core/plugins/btauto
23-
-I lib/coq/../coq-core/plugins/cc
24-
-I lib/coq/../coq-core/plugins/derive
25-
-I lib/coq/../coq-core/plugins/extraction
26-
-I lib/coq/../coq-core/plugins/firstorder
27-
-I lib/coq/../coq-core/plugins/funind
28-
-I lib/coq/../coq-core/plugins/ltac
29-
-I lib/coq/../coq-core/plugins/ltac2
30-
-I lib/coq/../coq-core/plugins/micromega
31-
-I lib/coq/../coq-core/plugins/nsatz
32-
-I lib/coq/../coq-core/plugins/number_string_notation
33-
-I lib/coq/../coq-core/plugins/ring
34-
-I lib/coq/../coq-core/plugins/rtauto
35-
-I lib/coq/../coq-core/plugins/ssreflect
36-
-I lib/coq/../coq-core/plugins/ssrmatching
37-
-I lib/coq/../coq-core/plugins/tauto
38-
-I lib/coq/../coq-core/plugins/tutorial/p0
39-
-I lib/coq/../coq-core/plugins/tutorial/p1
40-
-I lib/coq/../coq-core/plugins/tutorial/p2
41-
-I lib/coq/../coq-core/plugins/tutorial/p3
42-
-I lib/coq/../coq-core/plugins/zify
22+
-I .../plugins/btauto
23+
-I .../plugins/cc
24+
-I .../plugins/derive
25+
-I .../plugins/extraction
26+
-I .../plugins/firstorder
27+
-I .../plugins/funind
28+
-I .../plugins/ltac
29+
-I .../plugins/ltac2
30+
-I .../plugins/micromega
31+
-I .../plugins/nsatz
32+
-I .../plugins/number_string_notation
33+
-I .../plugins/ring
34+
-I .../plugins/rtauto
35+
-I .../plugins/ssreflect
36+
-I .../plugins/ssrmatching
37+
-I .../plugins/tauto
38+
-I .../plugins/tutorial/p0
39+
-I .../plugins/tutorial/p1
40+
-I .../plugins/tutorial/p2
41+
-I .../plugins/tutorial/p3
42+
-I .../plugins/zify
4343
-R coq/theories Coq
4444
-R $TESTCASE_ROOT/_build/default/theories foo
4545

@@ -52,27 +52,27 @@ Checking that we compute the directory and file for dune coq top correctly
5252
-w -deprecated-native-compiler-option
5353
-w -native-compiler-disabled
5454
-native-compiler ondemand
55-
-I lib/coq/../coq-core/plugins/btauto
56-
-I lib/coq/../coq-core/plugins/cc
57-
-I lib/coq/../coq-core/plugins/derive
58-
-I lib/coq/../coq-core/plugins/extraction
59-
-I lib/coq/../coq-core/plugins/firstorder
60-
-I lib/coq/../coq-core/plugins/funind
61-
-I lib/coq/../coq-core/plugins/ltac
62-
-I lib/coq/../coq-core/plugins/ltac2
63-
-I lib/coq/../coq-core/plugins/micromega
64-
-I lib/coq/../coq-core/plugins/nsatz
65-
-I lib/coq/../coq-core/plugins/number_string_notation
66-
-I lib/coq/../coq-core/plugins/ring
67-
-I lib/coq/../coq-core/plugins/rtauto
68-
-I lib/coq/../coq-core/plugins/ssreflect
69-
-I lib/coq/../coq-core/plugins/ssrmatching
70-
-I lib/coq/../coq-core/plugins/tauto
71-
-I lib/coq/../coq-core/plugins/tutorial/p0
72-
-I lib/coq/../coq-core/plugins/tutorial/p1
73-
-I lib/coq/../coq-core/plugins/tutorial/p2
74-
-I lib/coq/../coq-core/plugins/tutorial/p3
75-
-I lib/coq/../coq-core/plugins/zify
55+
-I .../plugins/btauto
56+
-I .../plugins/cc
57+
-I .../plugins/derive
58+
-I .../plugins/extraction
59+
-I .../plugins/firstorder
60+
-I .../plugins/funind
61+
-I .../plugins/ltac
62+
-I .../plugins/ltac2
63+
-I .../plugins/micromega
64+
-I .../plugins/nsatz
65+
-I .../plugins/number_string_notation
66+
-I .../plugins/ring
67+
-I .../plugins/rtauto
68+
-I .../plugins/ssreflect
69+
-I .../plugins/ssrmatching
70+
-I .../plugins/tauto
71+
-I .../plugins/tutorial/p0
72+
-I .../plugins/tutorial/p1
73+
-I .../plugins/tutorial/p2
74+
-I .../plugins/tutorial/p3
75+
-I .../plugins/zify
7676
-R coq/theories Coq
7777
-R $TESTCASE_ROOT/_build/default/theories foo
7878

‎test/blackbox-tests/test-cases/coq/coqtop/coqtop-no-build.t‎

Lines changed: 42 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -26,27 +26,27 @@ On a fresh build, this should do nothing but should pass the correct flags:
2626
-nI lib/coq-core/kernel
2727
-nI $TESTCASE_ROOT/_build/default/dir
2828
-boot
29-
-I lib/coq/../coq-core/plugins/btauto
30-
-I lib/coq/../coq-core/plugins/cc
31-
-I lib/coq/../coq-core/plugins/derive
32-
-I lib/coq/../coq-core/plugins/extraction
33-
-I lib/coq/../coq-core/plugins/firstorder
34-
-I lib/coq/../coq-core/plugins/funind
35-
-I lib/coq/../coq-core/plugins/ltac
36-
-I lib/coq/../coq-core/plugins/ltac2
37-
-I lib/coq/../coq-core/plugins/micromega
38-
-I lib/coq/../coq-core/plugins/nsatz
39-
-I lib/coq/../coq-core/plugins/number_string_notation
40-
-I lib/coq/../coq-core/plugins/ring
41-
-I lib/coq/../coq-core/plugins/rtauto
42-
-I lib/coq/../coq-core/plugins/ssreflect
43-
-I lib/coq/../coq-core/plugins/ssrmatching
44-
-I lib/coq/../coq-core/plugins/tauto
45-
-I lib/coq/../coq-core/plugins/tutorial/p0
46-
-I lib/coq/../coq-core/plugins/tutorial/p1
47-
-I lib/coq/../coq-core/plugins/tutorial/p2
48-
-I lib/coq/../coq-core/plugins/tutorial/p3
49-
-I lib/coq/../coq-core/plugins/zify
29+
-I .../plugins/btauto
30+
-I .../plugins/cc
31+
-I .../plugins/derive
32+
-I .../plugins/extraction
33+
-I .../plugins/firstorder
34+
-I .../plugins/funind
35+
-I .../plugins/ltac
36+
-I .../plugins/ltac2
37+
-I .../plugins/micromega
38+
-I .../plugins/nsatz
39+
-I .../plugins/number_string_notation
40+
-I .../plugins/ring
41+
-I .../plugins/rtauto
42+
-I .../plugins/ssreflect
43+
-I .../plugins/ssrmatching
44+
-I .../plugins/tauto
45+
-I .../plugins/tutorial/p0
46+
-I .../plugins/tutorial/p1
47+
-I .../plugins/tutorial/p2
48+
-I .../plugins/tutorial/p3
49+
-I .../plugins/zify
5050
-R coq/theories Coq
5151
-R $TESTCASE_ROOT/_build/default/dir basic
5252

@@ -61,26 +61,26 @@ And for comparison normally a build would happen:
6161
-nI lib/coq-core/kernel
6262
-nI $TESTCASE_ROOT/_build/default/dir
6363
-boot
64-
-I lib/coq/../coq-core/plugins/btauto
65-
-I lib/coq/../coq-core/plugins/cc
66-
-I lib/coq/../coq-core/plugins/derive
67-
-I lib/coq/../coq-core/plugins/extraction
68-
-I lib/coq/../coq-core/plugins/firstorder
69-
-I lib/coq/../coq-core/plugins/funind
70-
-I lib/coq/../coq-core/plugins/ltac
71-
-I lib/coq/../coq-core/plugins/ltac2
72-
-I lib/coq/../coq-core/plugins/micromega
73-
-I lib/coq/../coq-core/plugins/nsatz
74-
-I lib/coq/../coq-core/plugins/number_string_notation
75-
-I lib/coq/../coq-core/plugins/ring
76-
-I lib/coq/../coq-core/plugins/rtauto
77-
-I lib/coq/../coq-core/plugins/ssreflect
78-
-I lib/coq/../coq-core/plugins/ssrmatching
79-
-I lib/coq/../coq-core/plugins/tauto
80-
-I lib/coq/../coq-core/plugins/tutorial/p0
81-
-I lib/coq/../coq-core/plugins/tutorial/p1
82-
-I lib/coq/../coq-core/plugins/tutorial/p2
83-
-I lib/coq/../coq-core/plugins/tutorial/p3
84-
-I lib/coq/../coq-core/plugins/zify
64+
-I .../plugins/btauto
65+
-I .../plugins/cc
66+
-I .../plugins/derive
67+
-I .../plugins/extraction
68+
-I .../plugins/firstorder
69+
-I .../plugins/funind
70+
-I .../plugins/ltac
71+
-I .../plugins/ltac2
72+
-I .../plugins/micromega
73+
-I .../plugins/nsatz
74+
-I .../plugins/number_string_notation
75+
-I .../plugins/ring
76+
-I .../plugins/rtauto
77+
-I .../plugins/ssreflect
78+
-I .../plugins/ssrmatching
79+
-I .../plugins/tauto
80+
-I .../plugins/tutorial/p0
81+
-I .../plugins/tutorial/p1
82+
-I .../plugins/tutorial/p2
83+
-I .../plugins/tutorial/p3
84+
-I .../plugins/zify
8585
-R coq/theories Coq
8686
-R $TESTCASE_ROOT/_build/default/dir basic

0 commit comments

Comments
 (0)