diff --git a/dev/shim/dune b/dev/shim/dune index 116480eebcb5..551b6d2f71bf 100644 --- a/dev/shim/dune +++ b/dev/shim/dune @@ -46,7 +46,7 @@ (name coqc-prelude) (deps %{bin:coqc} - %{bin:coqworker.opt} + %{bin:coqworker} %{project_root}/theories/Init/Prelude.vo)) (rule @@ -111,7 +111,8 @@ ; 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.opt} + %{bin:coqworker} + %{bin:coqidetop} %{project_root}/theories/Init/Prelude.vo %{project_root}/coqide-server.install %{project_root}/coqide.install)) diff --git a/ide/coqide/dune b/ide/coqide/dune index 68331ddb5207..9b8742ddff2f 100644 --- a/ide/coqide/dune +++ b/ide/coqide/dune @@ -10,18 +10,13 @@ (executable (name idetop) - (public_name coqidetop.opt) + (public_name coqidetop) (package coqide-server) (modules idetop) (libraries coq-core.toplevel coqide-server.protocol platform_specific) (modes exe byte) (link_flags -linkall)) -(install - (section bin) - (package coqide-server) - (files (idetop.bc as coqidetop.byte))) - ; IDE Client, we may want to add the macos_prehook.ml conditionally. (library (name coqide_gui) diff --git a/lib/system.ml b/lib/system.ml index 36dcb5bad3f8..91e704a5de80 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -420,10 +420,9 @@ let fmt_instructions_result r = str m ++ str "\"" ++ str status (* We use argv.[0] as we don't want to resolve symlinks *) -let get_toplevel_path ?(byte=Sys.(backend_type = Bytecode)) top = +let get_toplevel_path top = let open Filename in let dir = if String.equal (basename Sys.argv.(0)) Sys.argv.(0) then "" else dirname Sys.argv.(0) ^ dir_sep in let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in - let eff = if byte then ".byte" else ".opt" in - dir ^ top ^ eff ^ exe + dir ^ top ^ exe diff --git a/lib/system.mli b/lib/system.mli index 89274bcf6cda..1e7216a00f82 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -157,8 +157,7 @@ val fmt_instructions_result : 'a instructions_result -> Pp.t - locating the directory: we don't rely on PATH as to make calls to /foo/bin/coqtop chose the right /foo/bin/coqproofworker - - adding the proper suffixes: .opt/.byte depending on the current - mode, + .exe if in windows. + - adding the proper suffix: .exe if in windows. Note that this function doesn't check that the executable actually exists. This is left back to caller, as well as the choice of @@ -167,4 +166,4 @@ val fmt_instructions_result : 'a instructions_result -> Pp.t the right name you want you execution to fail rather than fall into choosing some random binary from the system-wide installation of Coq. *) -val get_toplevel_path : ?byte:bool -> string -> string +val get_toplevel_path : string -> string diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index a823bbefbae3..fc912c68d07e 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -124,7 +124,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 = System.get_toplevel_path "coqworker" 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/Makefile b/test-suite/Makefile index fc41c83ea2e9..0d495013c393 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -85,11 +85,7 @@ coqdoc := $(BIN)coqdoc coqtop := $(BIN)coqtop -q -test-mode -R prerequisite TestSuite coqtopbyte := $(BIN)coqtop.byte -q -ifeq ($(BEST),opt) -coqidetop := $(BIN)coqidetop.opt -else -coqidetop := $(BIN)coqidetop.byte -endif +coqidetop := $(BIN)coqidetop coqc_interactive := $(coqc) -test-mode coqdep := $(BIN)coqdep diff --git a/topbin/dune b/topbin/dune index b2bf1ef6c736..e6a7ab0f1126 100644 --- a/topbin/dune +++ b/topbin/dune @@ -42,7 +42,7 @@ ; Workers (executable (name coqworker_bin) - (public_name coqworker.opt) + (public_name coqworker) (package coq-core) (modules coqworker_bin) (libraries coq-core.toplevel))