rename coqworker -> rocqworker

dev/dune

@@ -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
     ../tools/coqdep/coqdep.bc

dev/dune-dbg.in

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

dev/shim/dune

@@ -46,7 +46,7 @@
  (name coqc-prelude)
  (deps
   %{bin:coqc}
-  %{bin:coqworker}
+  %{bin:rocqworker}
   %{project_root}/theories/Init/Prelude.vo))
 
 (rule
@@ -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

stm/asyncTaskQueue.ml

@@ -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
 

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

@@ -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

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 @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@

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 -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

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 -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

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 -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

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 -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

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 -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

test-suite/misc/deps-order.sh

@@ -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

test-suite/misc/external-deps.sh

@@ -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

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

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 @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

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 @COQWORKER@
+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@

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

@@ -1,4 +1,4 @@
-misc/external-deps/file2.vo misc/external-deps/file2.glob misc/external-deps/file2.v.beautified misc/external-deps/file2.required_vo: misc/external-deps/file2.v @COQWORKER@ misc/external-deps/more/d1
+misc/external-deps/file2.vo misc/external-deps/file2.glob misc/external-deps/file2.v.beautified misc/external-deps/file2.required_vo: misc/external-deps/file2.v @ROCQWORKER@ misc/external-deps/more/d1
 *** Warning: in file misc/external-deps/file2.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/file2.found.deps

@@ -1 +1 @@
-misc/external-deps/file2.vo misc/external-deps/file2.glob misc/external-deps/file2.v.beautified misc/external-deps/file2.required_vo: misc/external-deps/file2.v @COQWORKER@ misc/external-deps/deps/d1
+misc/external-deps/file2.vo misc/external-deps/file2.glob misc/external-deps/file2.v.beautified misc/external-deps/file2.required_vo: misc/external-deps/file2.v @ROCQWORKER@ misc/external-deps/deps/d1

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

@@ -1,4 +1,4 @@
 Warning: in file misc/external-deps/file2.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/file2.vo misc/external-deps/file2.glob misc/external-deps/file2.v.beautified misc/external-deps/file2.required_vo: misc/external-deps/file2.v @COQWORKER@
+misc/external-deps/file2.vo misc/external-deps/file2.glob misc/external-deps/file2.v.beautified misc/external-deps/file2.required_vo: misc/external-deps/file2.v @ROCQWORKER@

tools/coqdep/lib/args.ml

@@ -53,7 +53,7 @@ let usage () =
   eprintf "  -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n";
   eprintf "  -coqlib dir : set the coq standard library directory\n";
   eprintf "  -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n";
-  eprintf "  -worker WORKER : output WORKER instead of the coqworker path\n";
+  eprintf "  -worker WORKER : output WORKER instead of the rocqworker path\n";
   eprintf "  -w (w1,..,wn) : configure display of warnings\n";
   eprintf "%!"; (* flush *)
   exit 1

tools/coqdep/lib/fl.ml

@@ -93,7 +93,7 @@ let findlib_deep_resolve ~file ~package =
 
 module Internal = struct
   let get_worker_path () =
-    let top = "coqworker" in
+    let top = "rocqworker" in
     let dir = Findlib.package_directory "rocq-runtime" in
     let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in
     let file = Filename.concat dir (top^exe) in

topbin/coqc_bin.ml

@@ -14,7 +14,7 @@ let () =
   let args = List.tl (Array.to_list Sys.argv) in
   let opts, args = Rocqshim.parse_opts args in
   let () = Rocqshim.init opts args in
-  let prog = get_worker_path { package = "rocq-runtime"; basename = "coqworker" } in
+  let prog = get_worker_path { package = "rocq-runtime"; basename = "rocqworker" } in
   let () = if opts.debug_shim then Printf.eprintf "Using %s\n%!" prog in
   let argv = Array.of_list (prog :: "--kind=compile" :: args) in
   exec_or_create_process prog argv

topbin/coqtop_bin.ml

@@ -14,7 +14,7 @@ let () =
   let args = List.tl (Array.to_list Sys.argv) in
   let opts, args = Rocqshim.parse_opts args in
   let () = Rocqshim.init opts args in
-  let prog = get_worker_path { package = "rocq-runtime"; basename = "coqworker" } in
+  let prog = get_worker_path { package = "rocq-runtime"; basename = "rocqworker" } in
   let () = if opts.debug_shim then Printf.eprintf "Using %s\n%!" prog in
   let argv = Array.of_list (prog :: "--kind=repl" :: args) in
   exec_or_create_process prog argv

topbin/coqtop_byte_bin.ml

@@ -14,7 +14,7 @@ let () =
   let args = List.tl (Array.to_list Sys.argv) in
   let opts, args = Rocqshim.parse_opts args in
   let () = Rocqshim.init opts args in
-  let prog = get_worker_path { package = "rocq-runtime"; basename = "coqworker_with_drop" } in
+  let prog = get_worker_path { package = "rocq-runtime"; basename = "rocqworker_with_drop" } in
   let () = if opts.debug_shim then Printf.eprintf "Using %s\n%!" prog in
   let argv = Array.of_list (prog :: args) in
   exec_or_create_process prog argv

topbin/dune

@@ -56,24 +56,24 @@
 
 ; Workers
 (executable
- (name coqworker)
- (modules coqworker)
+ (name rocqworker)
+ (modules rocqworker)
  (modes exe byte)
  (libraries rocq-runtime.toplevel))
  ; Adding -ccopt -flto to links options could be interesting, however,
  ; it doesn't work on Windows
 
 (executable
- (name coqworker_with_drop)
- (modules coqworker_with_drop)
+ (name rocqworker_with_drop)
+ (modules rocqworker_with_drop)
  (modes byte)
  (libraries compiler-libs.toplevel rocq-runtime.config.byte rocq-runtime.toplevel rocq-runtime.dev findlib.top))
 
 (install
  (section libexec)
  (package rocq-runtime)
  (files
-  (coqworker.exe as coqworker)
-  (coqworker.bc as coqworker.byte)
-  (coqworker_with_drop.bc as coqworker_with_drop)
+  (rocqworker.exe as rocqworker)
+  (rocqworker.bc as rocqworker.byte)
+  (rocqworker_with_drop.bc as rocqworker_with_drop)
   (rocqnative.exe as rocqnative)))

topbin/rocq.ml

@@ -21,7 +21,7 @@ let with_worker_gen opts basename args =
   Rocqshim.exec_or_create_process prog argv
 
 let with_worker opts kind args =
-  with_worker_gen opts "coqworker" (("--kind="^kind) :: args)
+  with_worker_gen opts "rocqworker" (("--kind="^kind) :: args)
 
 let with_sibling_exe opts prog args =
   let prog = System.get_toplevel_path prog in
@@ -41,7 +41,7 @@ let () =
   (* workers *)
   | ("c" | "compile") :: args -> with_worker opts "compile" args
   | ("top"|"repl") :: args -> with_worker opts "repl" args
-  | ("top-with-drop"|"repl-with-drop") :: args -> with_worker_gen opts "coqworker_with_drop" args
+  | ("top-with-drop"|"repl-with-drop") :: args -> with_worker_gen opts "rocqworker_with_drop" args
   | "native-precompile" :: args -> with_worker_gen opts "rocqnative" args
 
   (* public executables *)

topbin/coqworker.ml → topbin/rocqworker.ml

@@ -13,7 +13,7 @@ module WQuery = AsyncTaskQueue.MakeWorker(Stm.QueryTask) ()
 module WTactic = AsyncTaskQueue.MakeWorker(Partac.TacTask) ()
 
 let error s () =
-  Format.eprintf "Usage: coqworker.opt --kind=[compile|proof|query|tactic] $args@\ngot %s\n%!" s;
+  Format.eprintf "Usage: rocqworker --kind=[compile|repl|proof|query|tactic] $args@\ngot %s\n%!" s;
   exit 1
 
 type kind =

toplevel/workerLoop.ml

@@ -18,9 +18,9 @@ let worker_init init ((),stm_opts)  injections ~opts : Vernac.State.t =
   Coqtop.init_toploop opts stm_opts injections
 
 let usage = Boot.Usage.{
-  executable_name = "coqworker";
+  executable_name = "rocqworker";
   extra_args = "";
-  extra_options = ("\n" ^ "coqworker" ^ " specific options:\
+  extra_options = ("\n" ^ "rocqworker" ^ " specific options:\
 \n  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format\n");
 }