wip dynlink

tools/coqdep/lib/common.ml

@@ -158,8 +158,19 @@ let rec find_dependencies st basename =
     let add_dep dep = dependencies := DepSet.add dep !dependencies in
     let add_dep_other s = add_dep (Dep_info.Dep.Other s) in
 
+    let add_dep_ml (meta_files, cmxss) =
+      List.iter add_dep_other meta_files;
+      List.iter (fun str ->
+          let plugin_file = Filename.chop_extension str in
+          if not (StrSet.mem plugin_file !visited_ml) then begin
+            visited_ml := StrSet.add plugin_file !visited_ml;
+            add_dep (Dep_info.Dep.Ml plugin_file)
+          end)
+        cmxss
+    in
+
     (* worker dep *)
-    let () = add_dep_other (Loadpath.get_worker_path st) in
+    let () = add_dep_ml (Loadpath.get_worker_path st) in
 
     (* Reading file contents *)
     let f = basename ^ ".v" in
@@ -188,17 +199,7 @@ let rec find_dependencies st basename =
         | Declare sl ->
           (* We resolve "pkg_name" to a .cma file, using the META *)
           let sl = List.map (declare_ml_to_file f) sl in
-          let decl (meta_files, cmxss) =
-            List.iter add_dep_other meta_files;
-            List.iter (fun str ->
-            let plugin_file = Filename.chop_extension str in
-            if not (StrSet.mem plugin_file !visited_ml) then begin
-                visited_ml := StrSet.add plugin_file !visited_ml;
-                add_dep (Dep_info.Dep.Ml plugin_file)
-              end)
-              cmxss
-          in
-          List.iter decl sl
+          List.iter add_dep_ml sl
         | Load file ->
           let canon =
             match file with

tools/coqdep/lib/dune

@@ -5,11 +5,11 @@
 (ocamllex lexer)
 
 (rule
- (targets static_toplevel_libs.ml)
+ (targets static_libs.ml)
  (deps %{project_root}/_build/install/%{context_name}/lib/coq-core/META)
  (action
   (with-stdout-to %{targets}
-   (run ocamlfind query -recursive -predicates native coq-core.toplevel
-        -prefix "let static_toplevel_libs = [\n"
-        -format "\"%p\";"
-        -suffix "\n]\n"))))
+    (run ocamlfind query -recursive -predicates native coq-core.rocqloader
+         -prefix "let static_loader_libs = [\n"
+         -format "\"%p\";"
+         -suffix "\n]\n"))))

tools/coqdep/lib/fl.ml

@@ -72,12 +72,12 @@ let findlib_resolve ~package =
   let cmxs_file = List.map relative_if_dune cmxss in
   (meta_file, cmxs_file)
 
-let static_libs = CString.Set.of_list Static_toplevel_libs.static_toplevel_libs
+let static_loader_libs = CString.Set.of_list Static_libs.static_loader_libs
 
 let findlib_deep_resolve ~package =
   let packages = Findlib.package_deep_ancestors coqc_predicates [package] in
   let packages = CList.filter (fun package ->
-      not (CString.Set.mem package static_libs))
+      not (CString.Set.mem package static_loader_libs))
       packages
   in
   List.fold_left (fun (metas,cmxss) package ->
@@ -93,12 +93,5 @@ let findlib_deep_resolve ~file ~package =
 
 module Internal = struct
   let get_worker_path () =
-    let top = "coqworker" in
-    let dir = Findlib.package_directory "coq-core" in
-    let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in
-    let file = Filename.concat dir (top^exe) in
-    match Sys.getenv_opt "DUNE_SOURCEROOT" with
-    | Some dune when CString.is_prefix dune file ->
-      normalize_path (to_relative_path file)
-    | _ -> normalize_path file
+    findlib_deep_resolve ~file:"N/A" ~package:"coq-core.rocqworker"
 end

tools/coqdep/lib/fl.mli

@@ -25,5 +25,5 @@ val findlib_deep_resolve
 
 module Internal : sig
   (** Call Loadpath.get_worker_path instead *)
-  val get_worker_path : unit -> string
+  val get_worker_path : unit -> string list * string list
 end

tools/coqdep/lib/loadpath.ml

@@ -151,15 +151,15 @@ module State = struct
     ; coqlib : (dirpath * dirpath, result) Hashtbl.t
     ; other : (dirpath * dirpath, result) Hashtbl.t
     ; boot : bool
-    ; mutable worker : string option
+    ; mutable worker : (string list * string list) option
     }
 
   let make ~worker ~boot =
     { vfiles = Hashtbl.create 4101
     ; coqlib = Hashtbl.create 19
     ; other = Hashtbl.create 17317
     ; boot
-    ; worker
+    ; worker = Option.map (fun worker -> ([worker], [])) worker
     }
 
 end

tools/coqdep/lib/loadpath.mli

@@ -29,7 +29,7 @@ module State : sig
   val make : worker:string option -> boot:bool -> t
 end
 
-val get_worker_path : State.t -> string
+val get_worker_path : State.t -> string list * string list
 
 val search_v_known : State.t -> ?from:dirpath -> dirpath -> result option
 val search_other_known : State.t -> ?from:dirpath -> dirpath -> result option

tools/coqdep/lib/static_toplevel_libs.mli → tools/coqdep/lib/static_libs.mli

@@ -8,4 +8,4 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val static_toplevel_libs : string list
+val static_loader_libs : string list

topbin/coqc_bin.ml

@@ -8,12 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Rocqshim
-
 let () =
   let args = List.tl (Array.to_list Sys.argv) in
-  let {debug_shim}, args = Rocqshim.init args in
-  let prog = get_worker_path { package = "coq-core"; basename = "coqworker" } in
-  let () = if 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
+  let args = Rocqloader.init args in
+  let argv = "--kind=compile" :: args in
+  Rocqloader.load_and_run "coq-core.rocqworker" argv

topbin/coqworker_bin.ml

@@ -8,35 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-module WProof = AsyncTaskQueue.MakeWorker(Stm.ProofTask) ()
-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;
-  exit 1
-
-type kind =
-  | Worker of { init : unit -> unit; loop : unit -> unit }
-  | Compile
-
-let start kind args = match kind with
-  | Worker { init; loop } -> WorkerLoop.start ~init ~loop args
-  | Compile -> Coqc.main args
-
 let () =
-  if Array.length Sys.argv < 2
-  then error "no argument" ()
-  else
-    let argv = List.tl (Array.to_list Sys.argv) in
-    let kind = List.hd argv in
-    let argv = List.tl argv in
-    let kind =
-      match kind with
-      | "--kind=compile" -> Compile
-      | "--kind=proof" -> Worker { init = WProof.init_stdout; loop = WProof.main_loop }
-      | "--kind=query" -> Worker { init = WQuery.init_stdout; loop = WQuery.main_loop }
-      | "--kind=tactic" -> Worker { init = WTactic.init_stdout; loop = WTactic.main_loop }
-      | s -> error s ()
-    in
-    start kind argv
+  let args = List.tl (Array.to_list Sys.argv) in
+  let args = Rocqloader.init args in
+  Rocqloader.load_and_run "coq-core.rocqworker" args

topbin/coqworker_bin.mli

@@ -0,0 +1,9 @@
+(************************************************************************)
+(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)

topbin/dune

@@ -1,17 +1,24 @@
 (library
  (name rocqshim)
  (public_name coq-core.rocqshim)
- (synopsis "Rocq support for finding and exec-ing subcommands")
- (wrapped false) ; no point repeating the Rocqshim name
  (modules rocqshim)
- (libraries boot unix findlib))
+ (wrapped false) ; no point repeating the rocqshim name
+ (synopsis "Rocq shim for dynlinked subcommands"))
+
+(library
+ (name rocqloader)
+ (public_name coq-core.rocqloader)
+ (synopsis "Rocq support for finding and dynlinking subcommands")
+ (wrapped false) ; no point repeating the Rocqloader name
+ (modules rocqloader)
+ (libraries boot unix findlib.dynload rocqshim))
 
 (executable
  (public_name rocq)
  (package coq-core)
  (modules rocq)
  (modes exe byte)
- (libraries rocqshim))
+ (libraries rocqloader))
 
 (install
  (section bin)
@@ -38,7 +45,7 @@
  (public_name coqc)
  (package coq-core)
  (modules coqc_bin)
- (libraries rocqshim))
+ (libraries rocqloader))
 
 (executable
  (name coqnative_bin)
@@ -49,12 +56,18 @@
  (modes exe byte)
  (link_flags -linkall))
 
+(library
+ (name rocqworker_lib)
+ (public_name coq-core.rocqworker)
+ (modules rocqworker_lib)
+ (libraries coq-core.toplevel rocqshim))
+
 ; Workers
 (executable
  (name coqworker_bin)
  (modules coqworker_bin)
  (modes exe byte)
- (libraries coq-core.toplevel))
+ (libraries rocqloader))
  ; Adding -ccopt -flto to links options could be interesting, however,
  ; it doesn't work on Windows
 

topbin/rocq.ml

@@ -17,15 +17,13 @@ let () =
   if Array.length Sys.argv < 2 then error_usage ();
 
   let args = List.tl (Array.to_list Sys.argv) in
-  let {Rocqshim.debug_shim}, args = Rocqshim.init args in
+  let args = Rocqloader.init args in
 
   match args with
   | "-v" :: _ | "--version" :: _ -> Boot.Usage.version ()
   | ("c" | "compile") :: args ->
-    let prog = Rocqshim.get_worker_path { package = "coq-core"; basename = "coqworker" } in
-    let () = if debug_shim then Printf.eprintf "Using %s\n%!" prog in
-    let argv = Array.of_list (prog :: "--kind=compile" :: args) in
-    Rocqshim.exec_or_create_process prog argv
+    let argv = "--kind=compile" :: args in
+    Rocqloader.load_and_run "coq-core.rocqworker" argv
   | prog :: _ ->
     fatal_error "Unknown argument %s" prog
   | [] -> error_usage ()

topbin/rocqloader.ml

@@ -0,0 +1,112 @@
+(************************************************************************)
+(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+let debug_loader = ref false
+
+let ppdebug fmt =
+  if !debug_loader then Printf.eprintf fmt
+  else Printf.ifprintf stderr fmt
+
+type init_opts = {
+  boot : bool;
+  coqlib : string option;
+  ml_includes : string list;
+}
+
+let default_opts = {
+  boot = false;
+  coqlib = None;
+  ml_includes = [];
+}
+
+let rec parse_args opts = function
+  | [] -> opts
+  | "-boot" :: rest -> parse_args {opts with boot = true} rest
+  | "-coqlib" :: lib :: rest -> parse_args {opts with coqlib = Some lib} rest
+  | "-I" :: ml :: rest -> parse_args {opts with ml_includes = ml :: opts.ml_includes} rest
+  | _ :: rest -> parse_args opts rest
+
+let parse_args args =
+  let opts = parse_args default_opts args in
+  let opts = { opts with ml_includes = List.rev opts.ml_includes } in
+  opts
+
+let with_ic file f =
+  let ic = open_in file in
+  try
+    let rc = f ic in
+    close_in ic;
+    rc
+  with e -> close_in ic; raise e
+
+let parse_env_line l =
+  try Scanf.sscanf l "%[^=]=%S" (fun name value -> Some(name,value))
+  with Scanf.Scan_failure _ | End_of_file -> None
+
+(** We [putenv] instead of wrapping [getenv] calls because the
+    subprocess also needs the updated env, and usually doesn't have
+    the env file next to its binary. *)
+let putenv_from_file () =
+  let base = Filename.dirname Sys.executable_name in
+  let f = base ^ "/coq_environment.txt" in
+  try
+    with_ic f (fun ic ->
+        let () = ppdebug "using env vars from %s\n%!" f in
+        let rec iter () =
+          match input_line ic with
+          | exception End_of_file -> ()
+          | l ->
+            let () = match parse_env_line l with
+              | Some(n,v) ->
+                begin match Sys.getenv_opt n with
+                | None -> Unix.putenv n v
+                | Some _ -> ()
+                end
+              | None -> ()
+            in
+            iter ()
+        in
+        iter ())
+  with
+  | Sys_error s -> ()
+
+let make_ocamlpath opts =
+  let boot_ml_path =
+    if opts.boot then []
+    else
+      let () = Option.iter Boot.Env.set_coqlib opts.coqlib in
+      let coqenv = Boot.Env.init () in
+      Boot.Env.Path.[to_string (relative (Boot.Env.corelib coqenv) "..")]
+  in
+  let env_ocamlpath =
+    try [Sys.getenv "OCAMLPATH"]
+    with Not_found -> []
+  in
+  let path = List.concat [opts.ml_includes; boot_ml_path; env_ocamlpath] in
+  let ocamlpathsep = if Sys.unix then ":" else ";" in
+  String.concat ocamlpathsep path
+
+let init args =
+  let args = match args with
+    | "-debug-loader" :: args -> debug_loader := true; args
+    | _ -> args
+  in
+  (* important to putenv before reading OCAMLPATH / COQLIB *)
+  let () = putenv_from_file () in
+  let opts = parse_args args in
+  let env_ocamlpath = make_ocamlpath opts in
+  let () = ppdebug "OCAMLPATH = %s\n%!" env_ocamlpath in
+  Findlib.init ~env_ocamlpath ();
+  args
+
+let load_and_run package args =
+  Dynlink.allow_unsafe_modules true;
+  Fl_dynload.load_packages ~debug:!debug_loader [package];
+  !Rocqshim.run args