Rocq CLI prototype

Executable `rocq` can be called as `rocq compile args` (also `rocq c
args`) and will in turn call `coqworker --kind=compile
args`. (coqworker will be renamed later)

coqc has also been modified to call coqworker.

The design where `rocq` calls the worker executable instead of being
itself the worker executable is so that `rocq check` can work without
involving the main worker code.

We could also consider not having `rocq` handle `rocqchk` ie keeping
it completely separate.

TODO:

- make rocq handle coqtop mode
- make coqtop use the worker
- make rocq handle coqnative mode
- make coqnative use the worker(?)
- make rocq handle coqchk mode(?)
- make rocq handle misc modes (makefile, dep, doc, maybe tex, workmgr, votour?)
- make rocq handle coqidetop mode(?)
- make coqidetop use the worker(?) this would mean the worker depends
  on the xml protocol
- make rocq handle coqide mode(?)

Issues to be solved:

- (if coqtop.byte is to use the worker): figure out how to support
  coqtop.byte's extensions (dependency on coq-core.dev for printers,
  compiler-libs, findlib.top) without impacting worker.byte in non-coqtop
  modes

dev/dune

@@ -22,7 +22,7 @@
   (deps
     dune-dbg.in
     ../checker/coqchk.bc
-    ../topbin/coqc_byte_bin.bc
+    ../topbin/coqworker_byte_bin.bc
     ../topbin/coqnative_bin.bc
     ../ide/coqide/rocqide_main.bc
     ../tools/coqdep/coqdep.bc

dev/dune-dbg.in

@@ -21,7 +21,7 @@ while [[ $# -gt 0 ]]; do
             ;;
         coqc)
             shift
-            exe=_build/default/topbin/coqc_byte_bin.bc
+            exe="_build/default/topbin/coqworker_byte_bin.bc --kind=compile"
             break
             ;;
         coqtop)

ide/coqide/dune

@@ -14,7 +14,6 @@
  (package coqide-server)
  (modules idetop)
  (libraries coq-core.toplevel coqide-server.protocol platform_specific)
- (modes exe byte)
  (link_flags -linkall))
 
 ; IDE Client, we may want to add the macos_prehook.ml conditionally.

stm/asyncTaskQueue.ml

@@ -109,6 +109,11 @@ module Make(T : Task) () = struct
 
   let uid = ref 0
 
+  let get_toplevel_path top =
+    let dir = Findlib.package_directory "coq-core" in
+    let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in
+    Filename.concat dir (top^exe)
+
   let spawn ~spawn_args id priority =
     let name = Printf.sprintf "%s:%d:%d" T.name id !uid in
     incr uid;
@@ -124,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 = System.get_toplevel_path "coqworker" in
+      let worker_name = get_toplevel_path "coqworker" in
       Worker.spawn ~env worker_name args in
     name, proc, CThread.prepare_in_channel_for_thread_friendly_io ic, oc
 

test-suite/misc/coqdep-require-filter-categories.sh

@@ -4,7 +4,7 @@ set -e
 
 cd misc/coqdep-require-filter-categories
 
-$coqdep -R . 'Bla' ./*.v > stdout 2> stderr
+$coqdep -worker @COQWORKER@ -R . 'Bla' ./*.v > stdout 2> stderr
 
 diff stdout.ref stdout
 diff stderr.ref stderr

test-suite/misc/coqdep-require-filter-categories/stdout.ref

@@ -1,7 +1,7 @@
-fA.vo fA.glob fA.v.beautified fA.required_vo: fA.v 
-fB.vo fB.glob fB.v.beautified fB.required_vo: fB.v fA.vo
-fC.vo fC.glob fC.v.beautified fC.required_vo: fC.v fB.vo
-fD.vo fD.glob fD.v.beautified fD.required_vo: fD.v fA.vo
-fE.vo fE.glob fE.v.beautified fE.required_vo: fE.v fA.vo
-fF.vo fF.glob fF.v.beautified fF.required_vo: fF.v fA.vo
-fG.vo fG.glob fG.v.beautified fG.required_vo: fG.v fA.vo
+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 @COQWORKER@ fA.vo
+fC.vo fC.glob fC.v.beautified fC.required_vo: fC.v @COQWORKER@ fB.vo
+fD.vo fD.glob fD.v.beautified fD.required_vo: fD.v @COQWORKER@ fA.vo
+fE.vo fE.glob fE.v.beautified fE.required_vo: fE.v @COQWORKER@ fA.vo
+fF.vo fF.glob fF.v.beautified fF.required_vo: fF.v @COQWORKER@ fA.vo
+fG.vo fG.glob fG.v.beautified fG.required_vo: fG.v @COQWORKER@ fA.vo

test-suite/misc/deps-order-distinct-root.sh

@@ -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 -f _CoqDistinctRoot) > "$output" 2>&1
+(cd misc/deps; $coqdep -worker @COQWORKER@ -f _CoqDistinctRoot) > "$output" 2>&1
 diff -u --strip-trailing-cr misc/deps/DistinctRootDeps.out "$output"
 R=$?
 times

test-suite/misc/deps-order-from.sh

@@ -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 -R misc/deps/test-from T misc/deps/test-from/D.v misc/deps/test-from/E.v > "$output" 2>&1
+$coqdep -worker @COQWORKER@ -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

test-suite/misc/deps-order-subdir1-file.sh

@@ -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 -f _CoqTheory1Project) > "$output" 2>&1
+(cd misc/deps; $coqdep -worker @COQWORKER@ -f _CoqTheory1Project) > "$output" 2>&1
 diff -u --strip-trailing-cr misc/deps/Theory1Deps.out "$output"
 R=$?
 times

test-suite/misc/deps-order-subdir2-file.sh

@@ -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 -f _CoqTheory2Project) > "$output" 2>&1
+(cd misc/deps; $coqdep -worker @COQWORKER@ -f _CoqTheory2Project) > "$output" 2>&1
 diff -u --strip-trailing-cr misc/deps/Theory2Deps.out $output
 R=$?
 if [ $R != 0 ]; then

test-suite/misc/deps-order-subdir3-file.sh

@@ -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 -f _CoqTheory3Project) > "$output" 2>&1
+(cd misc/deps; $coqdep -worker @COQWORKER@ -f _CoqTheory3Project) > "$output" 2>&1
 diff -u --strip-trailing-cr misc/deps/Theory3Deps.out $output
 R=$?
 if [ $R != 0 ]; then

test-suite/misc/deps-order.sh

@@ -4,7 +4,8 @@
 # See bugs 2242, 2337, 2339
 rm -f misc/deps/lib/*.vo misc/deps/client/*.vo
 output=misc/deps/deps.real
-$coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > "$output"
+
+$coqdep -worker @COQWORKER@ -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

test-suite/misc/deps/DistinctRootDeps.out

@@ -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 
-DistinctRoot/B/File1.vo DistinctRoot/B/File1.glob DistinctRoot/B/File1.v.beautified DistinctRoot/B/File1.required_vo: DistinctRoot/B/File1.v 
-DistinctRoot/File2.vo DistinctRoot/File2.glob DistinctRoot/File2.v.beautified DistinctRoot/File2.required_vo: DistinctRoot/File2.v DistinctRoot/B/File1.vo
+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 @COQWORKER@ DistinctRoot/B/File1.vo

test-suite/misc/deps/Theory1Deps.out

@@ -1,8 +1,8 @@
-Theory1/File1.vo Theory1/File1.glob Theory1/File1.v.beautified Theory1/File1.required_vo: Theory1/File1.v 
-Theory1/File2.vo Theory1/File2.glob Theory1/File2.v.beautified Theory1/File2.required_vo: Theory1/File2.v Theory1/File1.vo
-Theory1/Subtheory1/File1.vo Theory1/Subtheory1/File1.glob Theory1/Subtheory1/File1.v.beautified Theory1/Subtheory1/File1.required_vo: Theory1/Subtheory1/File1.v 
-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 
-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 
-Theory1/Subtheory2/File1.vo Theory1/Subtheory2/File1.glob Theory1/Subtheory2/File1.v.beautified Theory1/Subtheory2/File1.required_vo: Theory1/Subtheory2/File1.v 
-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 
-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 
+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 @COQWORKER@ Theory1/File1.vo
+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@

test-suite/misc/deps/Theory2Deps.out

@@ -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
-Theory2/Subtheory1/File1.vo Theory2/Subtheory1/File1.glob Theory2/Subtheory1/File1.v.beautified Theory2/Subtheory1/File1.required_vo: Theory2/Subtheory1/File1.v 
-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 
-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 
-Theory2/Subtheory2/File1.vo Theory2/Subtheory2/File1.glob Theory2/Subtheory2/File1.v.beautified Theory2/Subtheory2/File1.required_vo: Theory2/Subtheory2/File1.v 
-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 
-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 
+Theory2/File2.vo Theory2/File2.glob Theory2/File2.v.beautified Theory2/File2.required_vo: Theory2/File2.v @COQWORKER@ 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
+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@
 *** 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).

test-suite/misc/deps/Theory3Deps.out

@@ -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
-Theory3/Subtheory1/File1.vo Theory3/Subtheory1/File1.glob Theory3/Subtheory1/File1.v.beautified Theory3/Subtheory1/File1.required_vo: Theory3/Subtheory1/File1.v 
-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 
-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 
-Theory3/Subtheory2/File1.vo Theory3/Subtheory2/File1.glob Theory3/Subtheory2/File1.v.beautified Theory3/Subtheory2/File1.required_vo: Theory3/Subtheory2/File1.v 
+Theory3/File2.vo Theory3/File2.glob Theory3/File2.v.beautified Theory3/File2.required_vo: Theory3/File2.v @COQWORKER@ Theory3/Subtheory1/File1.vo Theory3/Subtheory1/Subsubtheory1/File1.vo Theory3/Subtheory1/Subsubtheory2/File1.vo Theory3/Subtheory2/File1.vo
+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@
 *** 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).

test-suite/misc/deps/deps-from.out

@@ -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
-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
+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 @COQWORKER@ misc/deps/test-from/A/C.vo
+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 @COQWORKER@ misc/deps/test-from/B/C.vo

test-suite/misc/deps/deps.out

@@ -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
+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 @COQWORKER@ misc/deps/client/foo.vo misc/deps/lib/foo.vo

test-suite/misc/external-deps.sh

@@ -4,26 +4,26 @@ set -e
 
 # Set Extra Dependency syntax
 output=misc/external-deps/file1.found.real
-$coqdep -Q misc/external-deps/deps foo.bar misc/external-deps/file1.v > $output 2>&1
+$coqdep -worker @COQWORKER@ -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 -Q misc/external-deps/deps foo.bar -Q misc/external-deps/more foo.bar misc/external-deps/file1.v > $output 2>&1
+$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
 diff -u --strip-trailing-cr misc/external-deps/file1.ambiguous.deps $output
 
 output=misc/external-deps/file1.notfound.real
-$coqdep misc/external-deps/file1.v > $output 2>&1
+$coqdep -worker @COQWORKER@ 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 -Q misc/external-deps/deps foo.bar misc/external-deps/file2.v > $output 2>&1
+$coqdep -worker @COQWORKER@ -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 -Q misc/external-deps/deps foo.bar -Q misc/external-deps/more foo.bar misc/external-deps/file2.v > $output 2>&1
+$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
 diff -u --strip-trailing-cr misc/external-deps/file2.ambiguous.deps $output
 
 output=misc/external-deps/file2.notfound.real
-$coqdep misc/external-deps/file2.v > $output 2>&1
+$coqdep -worker @COQWORKER@ misc/external-deps/file2.v > $output 2>&1
 diff -u --strip-trailing-cr misc/external-deps/file2.notfound.deps $output

test-suite/misc/external-deps/file1.ambiguous.deps

@@ -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 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 @COQWORKER@ 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).

test-suite/misc/external-deps/file1.found.deps

@@ -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 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 @COQWORKER@ misc/external-deps/deps/d1

test-suite/misc/external-deps/file1.notfound.deps

@@ -1,4 +1,4 @@
 Warning: in file misc/external-deps/file1.v, external file d1 is required
          from root foo.bar and has not been found in the loadpath!
          [module-not-found,filesystem,default]
-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 
+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@