Don't use .opt in binary names when compiled in "best" mode

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

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)

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

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

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
 

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

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