Experiment: process nursery

lib/flags.ml

@@ -54,3 +54,5 @@ let if_silent f x = if !quiet then f x
 let if_verbose f x = if not !quiet then f x
 
 let test_mode = ref false
+
+let nursery = ref false

lib/flags.mli

@@ -73,3 +73,6 @@ val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b
     - display verbose information for [Fail]
     - print quickfix info in error printers *)
 val test_mode : bool ref
+
+(* XXX move this to higher layers (coqinit.ml?) *)
+val nursery : bool ref

sysinit/coqinit.ml

@@ -107,7 +107,9 @@ let boot_env usage opts =
   let coqlib = opts.config.coqlib in
   let warn_ignored_coqlib = CWarnings.warn_ignored_coqlib in
   match opts.main with
-  | Run -> Boot.Env.maybe_init ~boot ~coqlib ~warn_ignored_coqlib
+  | Run ->
+    if !Flags.nursery then Option.get @@ Boot.Env.initialized ()
+    else Boot.Env.maybe_init ~boot ~coqlib ~warn_ignored_coqlib
   | Queries qs ->
     let _ : Boot.Env.maybe_env =
       with_err
@@ -162,7 +164,7 @@ let init_runtime ~usage opts =
   let coqenv = boot_env usage opts in
 
   (* Paths for loading stuff *)
-  init_load_paths coqenv opts;
+  if not !Flags.nursery then init_load_paths coqenv opts;
 
   ()
 
@@ -172,7 +174,8 @@ let init_document opts =
   (* this isn't in init_load_paths because processes (typically
      vscoqtop) are allowed to have states with differing vo paths (but
      not with differing -boot or ml paths) *)
-  List.iter (fun x -> Loadpath.add_vo_path @@ to_vo_path x) opts.pre.vo_includes;
+  if not !Flags.nursery then
+    List.iter (fun x -> Loadpath.add_vo_path @@ to_vo_path x) opts.pre.vo_includes;
 
   (* Kernel configuration *)
   Global.set_impredicative_set opts.config.logic.impredicative_set;

sysinit/coqinit.mli

@@ -46,9 +46,11 @@ val parse_arguments :
     compilation. If Coq is used to process multiple libraries, what is set up
     here is really global and common to all of them.
 
-    This API must be called, typically jsut after parsing arguments. *)
+    This API must be called, typically just after parsing arguments. *)
 val init_runtime : usage:Boot.Usage.specific_usage -> Coqargs.t -> unit
 
+val init_load_paths : Boot.Env.maybe_env -> Coqargs.t -> unit
+
 val init_document : Coqargs.t -> unit
 
 (** 4 Start a library (sets options and loads objects like the prelude)

tools/CoqMakefile.in

@@ -420,7 +420,13 @@ ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) $(VDFILE)
 
 all:
 	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all
-	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all
+	rm -f .nursery-in .nursery-out
+	mkfifo .nursery-in .nursery-out
+	$(ROCQ) nursery $(COQLIBS) & \
+	export ROCQ_NURSERY=1 && \
+	$(MAKE) --no-print-directory -f "$(SELF)" real-all && \
+	echo Exit > .nursery-in && wait && \
+	rm .nursery-in .nursery-out
 	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all
 .PHONY: all
 

tools/coqdep/lib/args.ml

@@ -38,7 +38,7 @@ let make () =
 
 
 let warn_unknown_option =
-  CWarnings.create ~name:"unknown-option"
+  CWarnings.create ~name:"rocqdep-unknown-option"
     Pp.(fun opt -> str "Unknown option \"" ++ str opt ++ str "\".")
 
 let usage () =

topbin/rocq.ml

@@ -17,8 +17,20 @@ let with_worker_gen opts ?(package="rocq-runtime") basename args =
   let argv = Array.of_list (prog :: args) in
   Rocqshim.exec_or_create_process prog argv
 
-let with_worker opts kind args =
-  with_worker_gen opts "rocqworker" (("--kind="^kind) :: args)
+let with_worker ?(ignore_nursery=false) opts kind args =
+  let args = (("--kind="^kind) :: args) in
+  match if ignore_nursery then None else Sys.getenv_opt "ROCQ_NURSERY" with
+  | None -> with_worker_gen opts "rocqworker" args
+  | Some _ ->
+    let ch = open_out_gen [Open_wronly; Open_binary] 0 ".nursery-in" in
+    Printf.fprintf ch "Run\n";
+    Marshal.to_channel ch args [];
+    flush ch;
+    close_out ch;
+    let ch = open_in ".nursery-out" in
+    let status = input_line ch in
+    let status = int_of_string status in
+    exit status
 
 let with_sibling_exe opts prog args =
   let prog = System.get_toplevel_path prog in
@@ -42,6 +54,7 @@ type subcommand =
   | Tex
   | Makefile
   | Timelog2Html
+  | Nursery
 
 let subcommands = [
   ("compile", "Compile a Rocq source file", Compile);
@@ -63,6 +76,7 @@ let subcommands = [
   ("tex", "Process Rocq code in a Latex document", Tex);
   ("makefile", "Generate a Makefile to compile a Rocq project", Makefile);
   ("timelog2html", "Combine timing information and a Rocq source file", Timelog2Html);
+  ("nursery", "Experimental process nursery mode", Nursery);
 ]
 
 let print_usage fmt () =
@@ -103,6 +117,7 @@ let run_subcommand opts args = function
   | Tex -> Rocqtex.main ~prog:(Sys.argv.(0) ^ " tex") args
   | Makefile -> Rocqmakefile.main ~prog:[Sys.argv.(0); "makefile"] args
   | Timelog2Html -> with_worker_gen opts ~package:"rocq-devtools" "timelog2html" args
+  | Nursery -> with_worker ~ignore_nursery:true opts "nursery" args
 
 let () =
   if Array.length Sys.argv < 2 then error_usage ();

topbin/rocqworker.ml

@@ -8,38 +8,4 @@
 (*         *     (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: rocqworker --kind=[compile|repl|proof|query|tactic] $args@\ngot %s\n%!" s;
-  exit 1
-
-type kind =
-  | Worker of { init : unit -> unit; loop : unit -> unit }
-  | Compile
-  | Repl
-
-let start kind args = match kind with
-  | Worker { init; loop } -> WorkerLoop.start ~init ~loop args
-  | Compile -> Coqc.main args
-  | Repl -> Coqtop.(start_coq coqtop_toplevel 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=repl" -> Repl
-      | "--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 () = Worker_main.main (List.tl (Array.to_list Sys.argv))

toplevel/coqtop.ml

@@ -59,7 +59,7 @@ type ('a,'b) custom_toplevel =
 
 (** Main init routine *)
 let init_toplevel { parse_extra; init_extra; usage; initial_args } args =
-  Coqinit.init_ocaml ();
+  if not !Flags.nursery then Coqinit.init_ocaml ();
   let opts, customopts = Coqinit.parse_arguments ~parse_extra ~initial_args args in
   Stm.init_process (snd customopts);
   let () = Coqinit.init_runtime ~usage opts in

toplevel/dune

@@ -5,7 +5,7 @@
  (wrapped false)
  ; until ocaml/dune#4892 fixed
  ; (private_modules g_toplevel)
- (libraries rocq-runtime.stm
+ (libraries rocq-runtime.stm rocq-runtime.coqdeplib
   (select memtrace_init.ml from
    (memtrace -> memtrace_init.memtrace.ml)
    (!memtrace -> memtrace_init.default.ml))))

toplevel/nursery.ml

@@ -0,0 +1,144 @@
+(************************************************************************)
+(*         *      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 to_vo_path (x:Coqargs.vo_path) : Loadpath.vo_path = {
+  implicit = x.implicit;
+  unix_path = x.unix_path;
+  coq_path = Libnames.dirpath_of_string x.rocq_path;
+  recursive = true;
+  installed = false;
+  }
+
+let cache = ref Names.DirPath.Map.empty
+
+let fs_intern dp =
+  match Names.DirPath.Map.find_opt dp !cache with
+  | Some (v, prov) -> Ok v, prov
+  | None ->
+    Printf.eprintf "non cached require %s\n%!" (Names.DirPath.to_string dp);
+    Vernacinterp.base_fs_intern dp
+
+let cache_intern dp =
+  match Names.DirPath.Map.find_opt dp !cache with
+  | Some (v, _) -> Some v
+  | None ->
+    match Vernacinterp.base_fs_intern dp with
+    | exception e when CErrors.noncritical e -> None
+    | Ok v, prov ->
+      (* Printf.eprintf "nursery loaded %s\n%!" (Names.DirPath.to_string dp); *)
+      cache := Names.DirPath.Map.add dp (v,prov) !cache;
+      Some v
+    | Error _, _ -> None
+
+let rec rec_intern dp =
+  if Names.DirPath.Map.mem dp !cache then ()
+  else match cache_intern dp with
+    | None -> ()
+    | Some lib ->
+      Array.iter (fun (dp, _) -> rec_intern dp) (Library.library_deps lib)
+
+let intern_require_command from qids =
+  (* could also translate Coq-Stdlib but whatever *)
+  let root = match from with
+    | None -> None
+    | Some from ->
+      let (hd, tl) = Libnames.repr_qualid from in
+      Some (Libnames.add_dirpath_suffix hd tl)
+  in
+  let locate qid =
+    let open Loadpath in
+    match locate_qualified_library ?root qid with
+    | Ok (dir,_) -> Some dir
+    | Error _ -> None
+  in
+  let modrefl = List.filter_map locate qids in
+  List.iter rec_intern modrefl
+
+let rec intern_required lexbuf =
+  let open Coqdeplib.Lexer in
+  let qualid s = Libnames.qualid_of_string (String.concat "." s) in
+  match coq_action lexbuf with
+  | exception Fin_fichier -> ()
+  | Require (from, sl) ->
+    let from = Option.map qualid from in
+    let sl = List.map (fun (_, s) -> qualid s) sl in
+    intern_require_command from sl;
+    intern_required lexbuf
+  | Declare _ | Load _ | External _ ->
+    (* could try to look into Load but whatever *)
+    intern_required lexbuf
+
+let intern_required_injection = function
+  | Coqargs.RequireInjection { prefix; lib; } ->
+    intern_require_command (Option.map Libnames.qualid_of_string prefix)
+      [Libnames.qualid_of_string lib]
+  | _ -> ()
+
+let intern_required = function
+  | "--kind=compile" :: args ->
+    let () =
+      try
+        let opts, _ = Coqargs.parse_args ~init:Coqargs.default args in
+        List.iter intern_required_injection (Coqargs.injection_commands opts);
+        let f = List.find (fun a -> Filename.extension a = ".v") args in
+        let ch = open_in f in
+        let lexbuf = Lexing.from_channel ~with_positions:false ch in
+        intern_required lexbuf;
+        close_in ch
+      with e when CErrors.noncritical e -> ()
+    in
+    ()
+  | _ -> ()
+
+let rec loop self =
+  let ch_in = try open_in_bin ".nursery-in" with Sys.Break -> exit 0 in
+  match input_line ch_in with
+  | "Exit" -> ()
+  | "Run" ->
+    let args : string list = Marshal.from_channel ch_in in
+    (* don't keep ch_in open and instead reopen each loop
+       because I can't figure out how to wait for a new writer *)
+    close_in ch_in;
+    (* Printf.eprintf "nursery running %s\n%!" (String.concat " " args); *)
+    let () = intern_required args in
+    let pid = Unix.fork () in
+    if pid = 0 then
+      (* XXX redirect stdout/stderr to other process's fds? is that even possible?
+         (doesn't matter in rocq makefile operation
+         because it all goes to the make caller's stdout/stderr) *)
+      self args
+    else
+      let _, status = Unix.waitpid [] pid in
+      let status = match status with
+        | WEXITED i -> i
+        | WSIGNALED i -> i
+        | WSTOPPED _ -> assert false
+      in
+      let ch_out = open_out ".nursery-out" in
+      Printf.fprintf ch_out "%d\n%!" status;
+      close_out ch_out;
+      loop self
+  | s -> Printf.eprintf "Unknown nursery command %S.\n%!" s; exit 1
+
+let start self args =
+  let () = Exninfo.record_backtrace true in
+  let () = Flags.nursery := true in
+  let () = Vernacextend.static_linking_done () in
+  let () = Vernacinterp.set_fs_intern fs_intern in
+  let () = Coqinit.init_ocaml () in
+  let opts, _ = Coqargs.parse_args ~init:Coqargs.default args in
+  let boot_env = Boot.Env.maybe_init ~boot:opts.pre.boot ~coqlib:opts.config.coqlib
+      ~warn_ignored_coqlib:CWarnings.warn_ignored_coqlib
+  in
+  let () = Coqinit.init_load_paths boot_env opts in
+  (* nursery mode assumes vo_includes is constant *)
+  let () = List.iter (fun x -> Loadpath.add_vo_path @@ to_vo_path x) opts.pre.vo_includes in
+
+  loop self

toplevel/nursery.mli

@@ -0,0 +1,11 @@
+(************************************************************************)
+(*         *      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)         *)
+(************************************************************************)
+
+val start : (string list -> unit) -> string list -> unit

toplevel/worker_main.ml

@@ -0,0 +1,44 @@
+(************************************************************************)
+(*         *      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)         *)
+(************************************************************************)
+
+module WProof = AsyncTaskQueue.MakeWorker(Stm.ProofTask) ()
+module WQuery = AsyncTaskQueue.MakeWorker(Stm.QueryTask) ()
+module WTactic = AsyncTaskQueue.MakeWorker(Partac.TacTask) ()
+
+let error s () =
+  Format.eprintf "Usage: rocqworker --kind=[compile|repl|proof|query|tactic|nursery] $args@\ngot %s\n%!" s;
+  exit 1
+
+type kind =
+  | Worker of { init : unit -> unit; loop : unit -> unit }
+  | Compile
+  | Repl
+  | Nursery
+
+let start main kind args = match kind with
+  | Worker { init; loop } -> WorkerLoop.start ~init ~loop args
+  | Compile -> Coqc.main args
+  | Repl -> Coqtop.(start_coq coqtop_toplevel args)
+  | Nursery -> Nursery.start main args
+
+let rec main = function
+  | [] -> error "no argument" ()
+  | kind :: argv ->
+    let kind =
+      match kind with
+      | "--kind=compile" -> Compile
+      | "--kind=repl" -> Repl
+      | "--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 }
+      | "--kind=nursery" -> Nursery
+      | s -> error s ()
+    in
+    start main kind argv

toplevel/worker_main.mli

@@ -0,0 +1,11 @@
+(************************************************************************)
+(*         *      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)         *)
+(************************************************************************)
+
+val main : string list -> unit