Skip to content

Commit

Permalink
rename coqworker -> rocqworker
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Jan 6, 2025
1 parent 863ecc9 commit b76eea2
Show file tree
Hide file tree
Showing 37 changed files with 74 additions and 74 deletions.
2 changes: 1 addition & 1 deletion dev/dune
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@
(deps
dune-dbg.in
../checker/coqchk.bc
../topbin/coqworker.bc
../topbin/rocqworker.bc
../topbin/rocqnative.bc
../ide/coqide/rocqide_main.bc
; We require all the OCaml libs to be in place and searchable
Expand Down
2 changes: 1 addition & 1 deletion dev/dune-dbg.in
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ while [[ $# -gt 0 ]]; do
;;
coqc)
shift
exe="_build/default/topbin/coqworker.bc --kind=compile"
exe="_build/default/topbin/rocqworker.bc --kind=compile"
break
;;
coqtop)
Expand Down
4 changes: 2 additions & 2 deletions dev/shim/dune
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@
(name coqc-prelude)
(deps
%{bin:coqc}
%{bin:coqworker}
%{bin:rocqworker}
%{project_root}/theories/Init/Prelude.vo))

(rule
Expand Down Expand Up @@ -111,7 +111,7 @@
; coqide from PATH instead of giving a nice error
; there is no problem with the other shims since they don't depend on optional build products
%{project_root}/ide/coqide/rocqide_main.exe
%{bin:coqworker}
%{bin:rocqworker}
%{bin:coqidetop}
%{project_root}/theories/Init/Prelude.vo
%{project_root}/coqide-server.install
Expand Down
2 changes: 1 addition & 1 deletion stm/asyncTaskQueue.ml
Original file line number Diff line number Diff line change
Expand Up @@ -129,7 +129,7 @@ module Make(T : Task) () = struct
in
Array.of_list (wselect :: spawn_args @ worker_opts) in
let env = Array.append (T.extra_env ()) (Unix.environment ()) in
let worker_name = get_toplevel_path "coqworker" in
let worker_name = get_toplevel_path "rocqworker" in
Worker.spawn ~env worker_name args in
name, proc, CThread.prepare_in_channel_for_thread_friendly_io ic, oc

Expand Down
2 changes: 1 addition & 1 deletion test-suite/misc/coqdep-require-filter-categories.sh
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ set -e

cd misc/coqdep-require-filter-categories

$coqdep -worker @COQWORKER@ -R . 'Bla' ./*.v > stdout 2> stderr
$coqdep -worker @ROCQWORKER@ -R . 'Bla' ./*.v > stdout 2> stderr

diff stdout.ref stdout
diff stderr.ref stderr
14 changes: 7 additions & 7 deletions test-suite/misc/coqdep-require-filter-categories/stdout.ref
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
fA.vo fA.glob fA.v.beautified fA.required_vo: fA.v @COQWORKER@
fB.vo fB.glob fB.v.beautified fB.required_vo: fB.v fA.vo @COQWORKER@
fC.vo fC.glob fC.v.beautified fC.required_vo: fC.v fB.vo @COQWORKER@
fD.vo fD.glob fD.v.beautified fD.required_vo: fD.v fA.vo @COQWORKER@
fE.vo fE.glob fE.v.beautified fE.required_vo: fE.v fA.vo @COQWORKER@
fF.vo fF.glob fF.v.beautified fF.required_vo: fF.v fA.vo @COQWORKER@
fG.vo fG.glob fG.v.beautified fG.required_vo: fG.v fA.vo @COQWORKER@
fA.vo fA.glob fA.v.beautified fA.required_vo: fA.v @ROCQWORKER@
fB.vo fB.glob fB.v.beautified fB.required_vo: fB.v fA.vo @ROCQWORKER@
fC.vo fC.glob fC.v.beautified fC.required_vo: fC.v fB.vo @ROCQWORKER@
fD.vo fD.glob fD.v.beautified fD.required_vo: fD.v fA.vo @ROCQWORKER@
fE.vo fE.glob fE.v.beautified fE.required_vo: fE.v fA.vo @ROCQWORKER@
fF.vo fF.glob fF.v.beautified fF.required_vo: fF.v fA.vo @ROCQWORKER@
fG.vo fG.glob fG.v.beautified fG.required_vo: fG.v fA.vo @ROCQWORKER@
2 changes: 1 addition & 1 deletion test-suite/misc/deps-order-distinct-root.sh
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
# See also bugs #2242, #2337, #2339
rm -f misc/deps/DistinctRoot/*.vo misc/deps/DistinctRoot/*.vo/{A,B}/*.vo
output=misc/deps/DistinctRootDeps.real
(cd misc/deps; $coqdep -worker @COQWORKER@ -f _CoqDistinctRoot) > "$output" 2>&1
(cd misc/deps; $coqdep -worker @ROCQWORKER@ -f _CoqDistinctRoot) > "$output" 2>&1
diff -u --strip-trailing-cr misc/deps/DistinctRootDeps.out "$output"
R=$?
times
Expand Down
2 changes: 1 addition & 1 deletion test-suite/misc/deps-order-from.sh
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
# See bugs #11631, #14539
rm -f misc/deps/test-from/A/C.vo misc/deps/test-from/B/C.vo misc/deps/test-from/D.vo misc/deps/test-from/E.vo
output=misc/deps/deps-from.real
$coqdep -worker @COQWORKER@ -R misc/deps/test-from T misc/deps/test-from/D.v misc/deps/test-from/E.v > "$output" 2>&1
$coqdep -worker @ROCQWORKER@ -R misc/deps/test-from T misc/deps/test-from/D.v misc/deps/test-from/E.v > "$output" 2>&1
diff -u --strip-trailing-cr misc/deps/deps-from.out "$output"
R=$?
times
Expand Down
2 changes: 1 addition & 1 deletion test-suite/misc/deps-order-subdir1-file.sh
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
# the logical path (if any)
rm -f misc/deps/Theory1/*.vo misc/deps/Theory1/Subtheory?/*.vo misc/deps/Theory1/Subtheory?/Subsubtheory?/*.vo
output=misc/deps/Theory1Deps.real
(cd misc/deps; $coqdep -worker @COQWORKER@ -f _CoqTheory1Project) > "$output" 2>&1
(cd misc/deps; $coqdep -worker @ROCQWORKER@ -f _CoqTheory1Project) > "$output" 2>&1
diff -u --strip-trailing-cr misc/deps/Theory1Deps.out "$output"
R=$?
times
Expand Down
2 changes: 1 addition & 1 deletion test-suite/misc/deps-order-subdir2-file.sh
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ dotest=true
if [ $dotest = false ]; then exit 0; fi
rm -f misc/deps/Theory2/*.vo misc/deps/Theory2/Subtheory?/*.vo misc/deps/Theory2/Subtheory?/Subsubtheory?/*.vo
output=misc/deps/Theory2Deps.real
(cd misc/deps; $coqdep -worker @COQWORKER@ -f _CoqTheory2Project) > "$output" 2>&1
(cd misc/deps; $coqdep -worker @ROCQWORKER@ -f _CoqTheory2Project) > "$output" 2>&1
diff -u --strip-trailing-cr misc/deps/Theory2Deps.out $output
R=$?
if [ $R != 0 ]; then
Expand Down
2 changes: 1 addition & 1 deletion test-suite/misc/deps-order-subdir3-file.sh
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ dotest=true
if [ $dotest = false ]; then exit 0; fi
rm -f misc/deps/Theory3/*.vo misc/deps/Theory3/Subtheory?/*.vo misc/deps/Theory3/Subtheory?/Subsubtheory?/*.vo
output=misc/deps/Theory3Deps.real
(cd misc/deps; $coqdep -worker @COQWORKER@ -f _CoqTheory3Project) > "$output" 2>&1
(cd misc/deps; $coqdep -worker @ROCQWORKER@ -f _CoqTheory3Project) > "$output" 2>&1
diff -u --strip-trailing-cr misc/deps/Theory3Deps.out $output
R=$?
if [ $R != 0 ]; then
Expand Down
2 changes: 1 addition & 1 deletion test-suite/misc/deps-order.sh
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
rm -f misc/deps/lib/*.vo misc/deps/client/*.vo
output=misc/deps/deps.real

$coqdep -worker @COQWORKER@ -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > "$output"
$coqdep -worker @ROCQWORKER@ -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > "$output"
diff -u --strip-trailing-cr misc/deps/deps.out "$output" 2>&1
R=$?
times
Expand Down
6 changes: 3 additions & 3 deletions test-suite/misc/deps/DistinctRootDeps.out
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
DistinctRoot/A/File1.vo DistinctRoot/A/File1.glob DistinctRoot/A/File1.v.beautified DistinctRoot/A/File1.required_vo: DistinctRoot/A/File1.v @COQWORKER@
DistinctRoot/B/File1.vo DistinctRoot/B/File1.glob DistinctRoot/B/File1.v.beautified DistinctRoot/B/File1.required_vo: DistinctRoot/B/File1.v @COQWORKER@
DistinctRoot/File2.vo DistinctRoot/File2.glob DistinctRoot/File2.v.beautified DistinctRoot/File2.required_vo: DistinctRoot/File2.v DistinctRoot/B/File1.vo @COQWORKER@
DistinctRoot/A/File1.vo DistinctRoot/A/File1.glob DistinctRoot/A/File1.v.beautified DistinctRoot/A/File1.required_vo: DistinctRoot/A/File1.v @ROCQWORKER@
DistinctRoot/B/File1.vo DistinctRoot/B/File1.glob DistinctRoot/B/File1.v.beautified DistinctRoot/B/File1.required_vo: DistinctRoot/B/File1.v @ROCQWORKER@
DistinctRoot/File2.vo DistinctRoot/File2.glob DistinctRoot/File2.v.beautified DistinctRoot/File2.required_vo: DistinctRoot/File2.v DistinctRoot/B/File1.vo @ROCQWORKER@
16 changes: 8 additions & 8 deletions test-suite/misc/deps/Theory1Deps.out
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
Theory1/File1.vo Theory1/File1.glob Theory1/File1.v.beautified Theory1/File1.required_vo: Theory1/File1.v @COQWORKER@
Theory1/File2.vo Theory1/File2.glob Theory1/File2.v.beautified Theory1/File2.required_vo: Theory1/File2.v Theory1/File1.vo @COQWORKER@
Theory1/Subtheory1/File1.vo Theory1/Subtheory1/File1.glob Theory1/Subtheory1/File1.v.beautified Theory1/Subtheory1/File1.required_vo: Theory1/Subtheory1/File1.v @COQWORKER@
Theory1/Subtheory1/Subsubtheory1/File1.vo Theory1/Subtheory1/Subsubtheory1/File1.glob Theory1/Subtheory1/Subsubtheory1/File1.v.beautified Theory1/Subtheory1/Subsubtheory1/File1.required_vo: Theory1/Subtheory1/Subsubtheory1/File1.v @COQWORKER@
Theory1/Subtheory1/Subsubtheory2/File1.vo Theory1/Subtheory1/Subsubtheory2/File1.glob Theory1/Subtheory1/Subsubtheory2/File1.v.beautified Theory1/Subtheory1/Subsubtheory2/File1.required_vo: Theory1/Subtheory1/Subsubtheory2/File1.v @COQWORKER@
Theory1/Subtheory2/File1.vo Theory1/Subtheory2/File1.glob Theory1/Subtheory2/File1.v.beautified Theory1/Subtheory2/File1.required_vo: Theory1/Subtheory2/File1.v @COQWORKER@
Theory1/Subtheory2/Subsubtheory1/File1.vo Theory1/Subtheory2/Subsubtheory1/File1.glob Theory1/Subtheory2/Subsubtheory1/File1.v.beautified Theory1/Subtheory2/Subsubtheory1/File1.required_vo: Theory1/Subtheory2/Subsubtheory1/File1.v @COQWORKER@
Theory1/Subtheory2/Subsubtheory2/File1.vo Theory1/Subtheory2/Subsubtheory2/File1.glob Theory1/Subtheory2/Subsubtheory2/File1.v.beautified Theory1/Subtheory2/Subsubtheory2/File1.required_vo: Theory1/Subtheory2/Subsubtheory2/File1.v @COQWORKER@
Theory1/File1.vo Theory1/File1.glob Theory1/File1.v.beautified Theory1/File1.required_vo: Theory1/File1.v @ROCQWORKER@
Theory1/File2.vo Theory1/File2.glob Theory1/File2.v.beautified Theory1/File2.required_vo: Theory1/File2.v Theory1/File1.vo @ROCQWORKER@
Theory1/Subtheory1/File1.vo Theory1/Subtheory1/File1.glob Theory1/Subtheory1/File1.v.beautified Theory1/Subtheory1/File1.required_vo: Theory1/Subtheory1/File1.v @ROCQWORKER@
Theory1/Subtheory1/Subsubtheory1/File1.vo Theory1/Subtheory1/Subsubtheory1/File1.glob Theory1/Subtheory1/Subsubtheory1/File1.v.beautified Theory1/Subtheory1/Subsubtheory1/File1.required_vo: Theory1/Subtheory1/Subsubtheory1/File1.v @ROCQWORKER@
Theory1/Subtheory1/Subsubtheory2/File1.vo Theory1/Subtheory1/Subsubtheory2/File1.glob Theory1/Subtheory1/Subsubtheory2/File1.v.beautified Theory1/Subtheory1/Subsubtheory2/File1.required_vo: Theory1/Subtheory1/Subsubtheory2/File1.v @ROCQWORKER@
Theory1/Subtheory2/File1.vo Theory1/Subtheory2/File1.glob Theory1/Subtheory2/File1.v.beautified Theory1/Subtheory2/File1.required_vo: Theory1/Subtheory2/File1.v @ROCQWORKER@
Theory1/Subtheory2/Subsubtheory1/File1.vo Theory1/Subtheory2/Subsubtheory1/File1.glob Theory1/Subtheory2/Subsubtheory1/File1.v.beautified Theory1/Subtheory2/Subsubtheory1/File1.required_vo: Theory1/Subtheory2/Subsubtheory1/File1.v @ROCQWORKER@
Theory1/Subtheory2/Subsubtheory2/File1.vo Theory1/Subtheory2/Subsubtheory2/File1.glob Theory1/Subtheory2/Subsubtheory2/File1.v.beautified Theory1/Subtheory2/Subsubtheory2/File1.required_vo: Theory1/Subtheory2/Subsubtheory2/File1.v @ROCQWORKER@
14 changes: 7 additions & 7 deletions test-suite/misc/deps/Theory2Deps.out
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
Theory2/File2.vo Theory2/File2.glob Theory2/File2.v.beautified Theory2/File2.required_vo: Theory2/File2.v Theory2/Subtheory1/File1.vo Theory2/Subtheory1/Subsubtheory1/File1.vo Theory2/Subtheory1/Subsubtheory2/File1.vo Theory2/Subtheory2/File1.vo Theory2/Subtheory2/Subsubtheory1/File1.vo Theory2/Subtheory2/Subsubtheory2/File1.vo @COQWORKER@
Theory2/Subtheory1/File1.vo Theory2/Subtheory1/File1.glob Theory2/Subtheory1/File1.v.beautified Theory2/Subtheory1/File1.required_vo: Theory2/Subtheory1/File1.v @COQWORKER@
Theory2/Subtheory1/Subsubtheory1/File1.vo Theory2/Subtheory1/Subsubtheory1/File1.glob Theory2/Subtheory1/Subsubtheory1/File1.v.beautified Theory2/Subtheory1/Subsubtheory1/File1.required_vo: Theory2/Subtheory1/Subsubtheory1/File1.v @COQWORKER@
Theory2/Subtheory1/Subsubtheory2/File1.vo Theory2/Subtheory1/Subsubtheory2/File1.glob Theory2/Subtheory1/Subsubtheory2/File1.v.beautified Theory2/Subtheory1/Subsubtheory2/File1.required_vo: Theory2/Subtheory1/Subsubtheory2/File1.v @COQWORKER@
Theory2/Subtheory2/File1.vo Theory2/Subtheory2/File1.glob Theory2/Subtheory2/File1.v.beautified Theory2/Subtheory2/File1.required_vo: Theory2/Subtheory2/File1.v @COQWORKER@
Theory2/Subtheory2/Subsubtheory1/File1.vo Theory2/Subtheory2/Subsubtheory1/File1.glob Theory2/Subtheory2/Subsubtheory1/File1.v.beautified Theory2/Subtheory2/Subsubtheory1/File1.required_vo: Theory2/Subtheory2/Subsubtheory1/File1.v @COQWORKER@
Theory2/Subtheory2/Subsubtheory2/File1.vo Theory2/Subtheory2/Subsubtheory2/File1.glob Theory2/Subtheory2/Subsubtheory2/File1.v.beautified Theory2/Subtheory2/Subsubtheory2/File1.required_vo: Theory2/Subtheory2/Subsubtheory2/File1.v @COQWORKER@
Theory2/File2.vo Theory2/File2.glob Theory2/File2.v.beautified Theory2/File2.required_vo: Theory2/File2.v Theory2/Subtheory1/File1.vo Theory2/Subtheory1/Subsubtheory1/File1.vo Theory2/Subtheory1/Subsubtheory2/File1.vo Theory2/Subtheory2/File1.vo Theory2/Subtheory2/Subsubtheory1/File1.vo Theory2/Subtheory2/Subsubtheory2/File1.vo @ROCQWORKER@
Theory2/Subtheory1/File1.vo Theory2/Subtheory1/File1.glob Theory2/Subtheory1/File1.v.beautified Theory2/Subtheory1/File1.required_vo: Theory2/Subtheory1/File1.v @ROCQWORKER@
Theory2/Subtheory1/Subsubtheory1/File1.vo Theory2/Subtheory1/Subsubtheory1/File1.glob Theory2/Subtheory1/Subsubtheory1/File1.v.beautified Theory2/Subtheory1/Subsubtheory1/File1.required_vo: Theory2/Subtheory1/Subsubtheory1/File1.v @ROCQWORKER@
Theory2/Subtheory1/Subsubtheory2/File1.vo Theory2/Subtheory1/Subsubtheory2/File1.glob Theory2/Subtheory1/Subsubtheory2/File1.v.beautified Theory2/Subtheory1/Subsubtheory2/File1.required_vo: Theory2/Subtheory1/Subsubtheory2/File1.v @ROCQWORKER@
Theory2/Subtheory2/File1.vo Theory2/Subtheory2/File1.glob Theory2/Subtheory2/File1.v.beautified Theory2/Subtheory2/File1.required_vo: Theory2/Subtheory2/File1.v @ROCQWORKER@
Theory2/Subtheory2/Subsubtheory1/File1.vo Theory2/Subtheory2/Subsubtheory1/File1.glob Theory2/Subtheory2/Subsubtheory1/File1.v.beautified Theory2/Subtheory2/Subsubtheory1/File1.required_vo: Theory2/Subtheory2/Subsubtheory1/File1.v @ROCQWORKER@
Theory2/Subtheory2/Subsubtheory2/File1.vo Theory2/Subtheory2/Subsubtheory2/File1.glob Theory2/Subtheory2/Subsubtheory2/File1.v.beautified Theory2/Subtheory2/Subsubtheory2/File1.required_vo: Theory2/Subtheory2/Subsubtheory2/File1.v @ROCQWORKER@
*** Warning: in file Theory2/File2.v,
required library File1 matches several files in path
(found File1.v in Theory2/Subtheory2/Subsubtheory2, Theory2/Subtheory2/Subsubtheory1, Theory2/Subtheory2, Theory2/Subtheory1/Subsubtheory2, Theory2/Subtheory1/Subsubtheory1 and Theory2/Subtheory1; Require will fail).
10 changes: 5 additions & 5 deletions test-suite/misc/deps/Theory3Deps.out
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
Theory3/File2.vo Theory3/File2.glob Theory3/File2.v.beautified Theory3/File2.required_vo: Theory3/File2.v Theory3/Subtheory1/File1.vo Theory3/Subtheory1/Subsubtheory1/File1.vo Theory3/Subtheory1/Subsubtheory2/File1.vo Theory3/Subtheory2/File1.vo @COQWORKER@
Theory3/Subtheory1/File1.vo Theory3/Subtheory1/File1.glob Theory3/Subtheory1/File1.v.beautified Theory3/Subtheory1/File1.required_vo: Theory3/Subtheory1/File1.v @COQWORKER@
Theory3/Subtheory1/Subsubtheory1/File1.vo Theory3/Subtheory1/Subsubtheory1/File1.glob Theory3/Subtheory1/Subsubtheory1/File1.v.beautified Theory3/Subtheory1/Subsubtheory1/File1.required_vo: Theory3/Subtheory1/Subsubtheory1/File1.v @COQWORKER@
Theory3/Subtheory1/Subsubtheory2/File1.vo Theory3/Subtheory1/Subsubtheory2/File1.glob Theory3/Subtheory1/Subsubtheory2/File1.v.beautified Theory3/Subtheory1/Subsubtheory2/File1.required_vo: Theory3/Subtheory1/Subsubtheory2/File1.v @COQWORKER@
Theory3/Subtheory2/File1.vo Theory3/Subtheory2/File1.glob Theory3/Subtheory2/File1.v.beautified Theory3/Subtheory2/File1.required_vo: Theory3/Subtheory2/File1.v @COQWORKER@
Theory3/File2.vo Theory3/File2.glob Theory3/File2.v.beautified Theory3/File2.required_vo: Theory3/File2.v Theory3/Subtheory1/File1.vo Theory3/Subtheory1/Subsubtheory1/File1.vo Theory3/Subtheory1/Subsubtheory2/File1.vo Theory3/Subtheory2/File1.vo @ROCQWORKER@
Theory3/Subtheory1/File1.vo Theory3/Subtheory1/File1.glob Theory3/Subtheory1/File1.v.beautified Theory3/Subtheory1/File1.required_vo: Theory3/Subtheory1/File1.v @ROCQWORKER@
Theory3/Subtheory1/Subsubtheory1/File1.vo Theory3/Subtheory1/Subsubtheory1/File1.glob Theory3/Subtheory1/Subsubtheory1/File1.v.beautified Theory3/Subtheory1/Subsubtheory1/File1.required_vo: Theory3/Subtheory1/Subsubtheory1/File1.v @ROCQWORKER@
Theory3/Subtheory1/Subsubtheory2/File1.vo Theory3/Subtheory1/Subsubtheory2/File1.glob Theory3/Subtheory1/Subsubtheory2/File1.v.beautified Theory3/Subtheory1/Subsubtheory2/File1.required_vo: Theory3/Subtheory1/Subsubtheory2/File1.v @ROCQWORKER@
Theory3/Subtheory2/File1.vo Theory3/Subtheory2/File1.glob Theory3/Subtheory2/File1.v.beautified Theory3/Subtheory2/File1.required_vo: Theory3/Subtheory2/File1.v @ROCQWORKER@
*** Warning: in file Theory3/File2.v,
required library File1 matches several files in path
(found File1.v in Theory3/Subtheory2, Theory3/Subtheory1/Subsubtheory2, Theory3/Subtheory1/Subsubtheory1 and Theory3/Subtheory1; Require will fail).
4 changes: 2 additions & 2 deletions test-suite/misc/deps/deps-from.out
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
misc/deps/test-from/D.vo misc/deps/test-from/D.glob misc/deps/test-from/D.v.beautified misc/deps/test-from/D.required_vo: misc/deps/test-from/D.v misc/deps/test-from/A/C.vo @COQWORKER@
misc/deps/test-from/E.vo misc/deps/test-from/E.glob misc/deps/test-from/E.v.beautified misc/deps/test-from/E.required_vo: misc/deps/test-from/E.v misc/deps/test-from/B/C.vo @COQWORKER@
misc/deps/test-from/D.vo misc/deps/test-from/D.glob misc/deps/test-from/D.v.beautified misc/deps/test-from/D.required_vo: misc/deps/test-from/D.v misc/deps/test-from/A/C.vo @ROCQWORKER@
misc/deps/test-from/E.vo misc/deps/test-from/E.glob misc/deps/test-from/E.v.beautified misc/deps/test-from/E.required_vo: misc/deps/test-from/E.v misc/deps/test-from/B/C.vo @ROCQWORKER@
2 changes: 1 addition & 1 deletion test-suite/misc/deps/deps.out
Original file line number Diff line number Diff line change
@@ -1 +1 @@
misc/deps/client/bar.vo misc/deps/client/bar.glob misc/deps/client/bar.v.beautified misc/deps/client/bar.required_vo: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo @COQWORKER@
misc/deps/client/bar.vo misc/deps/client/bar.glob misc/deps/client/bar.v.beautified misc/deps/client/bar.required_vo: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo @ROCQWORKER@
12 changes: 6 additions & 6 deletions test-suite/misc/external-deps.sh
Original file line number Diff line number Diff line change
Expand Up @@ -4,26 +4,26 @@ set -e

# Set Extra Dependency syntax
output=misc/external-deps/file1.found.real
$coqdep -worker @COQWORKER@ -Q misc/external-deps/deps foo.bar misc/external-deps/file1.v > $output 2>&1
$coqdep -worker @ROCQWORKER@ -Q misc/external-deps/deps foo.bar misc/external-deps/file1.v > $output 2>&1
diff -u --strip-trailing-cr misc/external-deps/file1.found.deps $output

output=misc/external-deps/file1.ambiguous.real
$coqdep -worker @COQWORKER@ -Q misc/external-deps/deps foo.bar -Q misc/external-deps/more foo.bar misc/external-deps/file1.v > $output 2>&1
$coqdep -worker @ROCQWORKER@ -Q misc/external-deps/deps foo.bar -Q misc/external-deps/more foo.bar misc/external-deps/file1.v > $output 2>&1
diff -u --strip-trailing-cr misc/external-deps/file1.ambiguous.deps $output

output=misc/external-deps/file1.notfound.real
$coqdep -worker @COQWORKER@ misc/external-deps/file1.v > $output 2>&1
$coqdep -worker @ROCQWORKER@ misc/external-deps/file1.v > $output 2>&1
diff -u --strip-trailing-cr misc/external-deps/file1.notfound.deps $output

# From bla Extra Dependency syntax
output=misc/external-deps/file2.found.real
$coqdep -worker @COQWORKER@ -Q misc/external-deps/deps foo.bar misc/external-deps/file2.v > $output 2>&1
$coqdep -worker @ROCQWORKER@ -Q misc/external-deps/deps foo.bar misc/external-deps/file2.v > $output 2>&1
diff -u --strip-trailing-cr misc/external-deps/file2.found.deps $output

output=misc/external-deps/file2.ambiguous.real
$coqdep -worker @COQWORKER@ -Q misc/external-deps/deps foo.bar -Q misc/external-deps/more foo.bar misc/external-deps/file2.v > $output 2>&1
$coqdep -worker @ROCQWORKER@ -Q misc/external-deps/deps foo.bar -Q misc/external-deps/more foo.bar misc/external-deps/file2.v > $output 2>&1
diff -u --strip-trailing-cr misc/external-deps/file2.ambiguous.deps $output

output=misc/external-deps/file2.notfound.real
$coqdep -worker @COQWORKER@ misc/external-deps/file2.v > $output 2>&1
$coqdep -worker @ROCQWORKER@ misc/external-deps/file2.v > $output 2>&1
diff -u --strip-trailing-cr misc/external-deps/file2.notfound.deps $output
2 changes: 1 addition & 1 deletion test-suite/misc/external-deps/file1.ambiguous.deps
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
misc/external-deps/file1.vo misc/external-deps/file1.glob misc/external-deps/file1.v.beautified misc/external-deps/file1.required_vo: misc/external-deps/file1.v @COQWORKER@ misc/external-deps/more/d1
misc/external-deps/file1.vo misc/external-deps/file1.glob misc/external-deps/file1.v.beautified misc/external-deps/file1.required_vo: misc/external-deps/file1.v @ROCQWORKER@ misc/external-deps/more/d1
*** Warning: in file misc/external-deps/file1.v,
required external file d1 exactly matches several files in path
(found d1 in misc/external-deps/deps and misc/external-deps/more; used the latter).
2 changes: 1 addition & 1 deletion test-suite/misc/external-deps/file1.found.deps
Original file line number Diff line number Diff line change
@@ -1 +1 @@
misc/external-deps/file1.vo misc/external-deps/file1.glob misc/external-deps/file1.v.beautified misc/external-deps/file1.required_vo: misc/external-deps/file1.v @COQWORKER@ misc/external-deps/deps/d1
misc/external-deps/file1.vo misc/external-deps/file1.glob misc/external-deps/file1.v.beautified misc/external-deps/file1.required_vo: misc/external-deps/file1.v @ROCQWORKER@ misc/external-deps/deps/d1
Loading

0 comments on commit b76eea2

Please sign in to comment.