diff --git a/dev/dune b/dev/dune index dcd49ab0c4e4..76060bd7296f 100644 --- a/dev/dune +++ b/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 diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index bb475a0feca6..8f377b4aafcc 100755 --- a/dev/dune-dbg.in +++ b/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) diff --git a/dev/shim/dune b/dev/shim/dune index 5c58758ee060..56bcdd216b19 100644 --- a/dev/shim/dune +++ b/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 diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 3ecfc3041718..872c21e03e1f 100644 --- a/stm/asyncTaskQueue.ml +++ b/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 diff --git a/test-suite/misc/coqdep-require-filter-categories.sh b/test-suite/misc/coqdep-require-filter-categories.sh index 8582f42c93da..9861f9ce311f 100755 --- a/test-suite/misc/coqdep-require-filter-categories.sh +++ b/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 diff --git a/test-suite/misc/coqdep-require-filter-categories/stdout.ref b/test-suite/misc/coqdep-require-filter-categories/stdout.ref index c1c9de761ed6..53916d8ea1b4 100644 --- a/test-suite/misc/coqdep-require-filter-categories/stdout.ref +++ b/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@ diff --git a/test-suite/misc/deps-order-distinct-root.sh b/test-suite/misc/deps-order-distinct-root.sh index f320bd9f7cad..a368c0c980de 100755 --- a/test-suite/misc/deps-order-distinct-root.sh +++ b/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 diff --git a/test-suite/misc/deps-order-from.sh b/test-suite/misc/deps-order-from.sh index 5c6a1100f9da..750f8c288131 100755 --- a/test-suite/misc/deps-order-from.sh +++ b/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 diff --git a/test-suite/misc/deps-order-subdir1-file.sh b/test-suite/misc/deps-order-subdir1-file.sh index ce7e53cfb407..38778c7b48e3 100755 --- a/test-suite/misc/deps-order-subdir1-file.sh +++ b/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 diff --git a/test-suite/misc/deps-order-subdir2-file.sh b/test-suite/misc/deps-order-subdir2-file.sh index 034fe938d9d5..8cc8a695d8de 100755 --- a/test-suite/misc/deps-order-subdir2-file.sh +++ b/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 diff --git a/test-suite/misc/deps-order-subdir3-file.sh b/test-suite/misc/deps-order-subdir3-file.sh index e119f2ad1d55..1bbc9d82be16 100755 --- a/test-suite/misc/deps-order-subdir3-file.sh +++ b/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 diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh index 5e80c0e4ffa8..2711ab34d9e8 100755 --- a/test-suite/misc/deps-order.sh +++ b/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 diff --git a/test-suite/misc/external-deps.sh b/test-suite/misc/external-deps.sh index 4c35b361f678..6c3c6fff58be 100755 --- a/test-suite/misc/external-deps.sh +++ b/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 diff --git a/test-suite/misc/external-deps/file1.ambiguous.deps b/test-suite/misc/external-deps/file1.ambiguous.deps index 7fc0902a5729..9117630bf347 100644 --- a/test-suite/misc/external-deps/file1.ambiguous.deps +++ b/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). diff --git a/test-suite/misc/external-deps/file1.found.deps b/test-suite/misc/external-deps/file1.found.deps index 269ad1f04841..5b20c0df8894 100644 --- a/test-suite/misc/external-deps/file1.found.deps +++ b/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 diff --git a/test-suite/misc/external-deps/file1.notfound.deps b/test-suite/misc/external-deps/file1.notfound.deps index cf9d032b2e14..2b3d7ab40db0 100644 --- a/test-suite/misc/external-deps/file1.notfound.deps +++ b/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@ diff --git a/test-suite/misc/external-deps/file2.ambiguous.deps b/test-suite/misc/external-deps/file2.ambiguous.deps index a4140549a50a..1e3a55d11b0b 100644 --- a/test-suite/misc/external-deps/file2.ambiguous.deps +++ b/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). diff --git a/test-suite/misc/external-deps/file2.found.deps b/test-suite/misc/external-deps/file2.found.deps index ef8663badfc9..9c89399b9229 100644 --- a/test-suite/misc/external-deps/file2.found.deps +++ b/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 diff --git a/test-suite/misc/external-deps/file2.notfound.deps b/test-suite/misc/external-deps/file2.notfound.deps index ae77d637c30f..90cf56ec4a78 100644 --- a/test-suite/misc/external-deps/file2.notfound.deps +++ b/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@ diff --git a/tools/coqdep/lib/args.ml b/tools/coqdep/lib/args.ml index 1e59e2ec96bd..ea4796692eeb 100644 --- a/tools/coqdep/lib/args.ml +++ b/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 diff --git a/tools/coqdep/lib/fl.ml b/tools/coqdep/lib/fl.ml index afc76c5f2f47..f6dc7275d8a2 100644 --- a/tools/coqdep/lib/fl.ml +++ b/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 diff --git a/topbin/coqc_bin.ml b/topbin/coqc_bin.ml index 350d34863e05..055a021a91a1 100644 --- a/topbin/coqc_bin.ml +++ b/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 diff --git a/topbin/coqtop_bin.ml b/topbin/coqtop_bin.ml index 1f2712121780..7b7bf88d3ef8 100644 --- a/topbin/coqtop_bin.ml +++ b/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 diff --git a/topbin/coqtop_byte_bin.ml b/topbin/coqtop_byte_bin.ml index 0cb7ffe449c3..67b8069d1c4b 100644 --- a/topbin/coqtop_byte_bin.ml +++ b/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 diff --git a/topbin/dune b/topbin/dune index 68e7ae7143a4..e360e906bf01 100644 --- a/topbin/dune +++ b/topbin/dune @@ -56,16 +56,16 @@ ; 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)) @@ -73,7 +73,7 @@ (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))) diff --git a/topbin/rocq.ml b/topbin/rocq.ml index edb1a90f2a26..d4a6da4e79af 100644 --- a/topbin/rocq.ml +++ b/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 *) diff --git a/topbin/coqworker.ml b/topbin/rocqworker.ml similarity index 94% rename from topbin/coqworker.ml rename to topbin/rocqworker.ml index 6ef13275a653..b095d8e8b68a 100644 --- a/topbin/coqworker.ml +++ b/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 = diff --git a/topbin/coqworker.mli b/topbin/rocqworker.mli similarity index 100% rename from topbin/coqworker.mli rename to topbin/rocqworker.mli diff --git a/topbin/coqworker_with_drop.ml b/topbin/rocqworker_with_drop.ml similarity index 100% rename from topbin/coqworker_with_drop.ml rename to topbin/rocqworker_with_drop.ml diff --git a/topbin/coqworker_with_drop.mli b/topbin/rocqworker_with_drop.mli similarity index 100% rename from topbin/coqworker_with_drop.mli rename to topbin/rocqworker_with_drop.mli diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index fd12c17e0827..83502f23f119 100644 --- a/toplevel/workerLoop.ml +++ b/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"); }