From 577474d16a9ac78de57e348e19b6ad8cbb59a8fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 22 Jul 2026 16:53:52 +0200 Subject: [PATCH 1/3] basic nursery --- lib/flags.ml | 2 ++ lib/flags.mli | 3 ++ sysinit/coqinit.ml | 9 ++++-- sysinit/coqinit.mli | 4 ++- tools/CoqMakefile.in | 12 ++++++++ topbin/rocq.ml | 19 ++++++++++-- topbin/rocqworker.ml | 36 +---------------------- toplevel/coqtop.ml | 2 +- toplevel/nursery.ml | 63 ++++++++++++++++++++++++++++++++++++++++ toplevel/nursery.mli | 11 +++++++ toplevel/worker_main.ml | 44 ++++++++++++++++++++++++++++ toplevel/worker_main.mli | 11 +++++++ vernac/loadpath.ml | 2 +- 13 files changed, 175 insertions(+), 43 deletions(-) create mode 100644 toplevel/nursery.ml create mode 100644 toplevel/nursery.mli create mode 100644 toplevel/worker_main.ml create mode 100644 toplevel/worker_main.mli diff --git a/lib/flags.ml b/lib/flags.ml index 910581decb57..47c482fc44c7 100644 --- a/lib/flags.ml +++ b/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 diff --git a/lib/flags.mli b/lib/flags.mli index 0141a327cab7..2bf0b5a3456c 100644 --- a/lib/flags.mli +++ b/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 diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml index d6f777fbb8de..4d28c7733eab 100644 --- a/sysinit/coqinit.ml +++ b/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; diff --git a/sysinit/coqinit.mli b/sysinit/coqinit.mli index 8666006e61bb..d8de17c7926a 100644 --- a/sysinit/coqinit.mli +++ b/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) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 87b5fb59418d..789fd50a5390 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -418,10 +418,22 @@ ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) $(VDFILE) # Compilation targets ######################################################### +ifdef ROCQ_NURSERY +all: + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all + rm -f .nursery-in .nursery-out + mkfifo .nursery-in .nursery-out + $(ROCQ) nursery $(COQLIBS) & \ + $(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 +else all: $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all +endif .PHONY: all all.timing.diff: diff --git a/topbin/rocq.ml b/topbin/rocq.ml index 45b389c8dde3..61502918df35 100644 --- a/topbin/rocq.ml +++ b/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 (); diff --git a/topbin/rocqworker.ml b/topbin/rocqworker.ml index b095d8e8b68a..f64603f5e590 100644 --- a/topbin/rocqworker.ml +++ b/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)) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 5a582134839f..a330bccd1102 100644 --- a/toplevel/coqtop.ml +++ b/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 diff --git a/toplevel/nursery.ml b/toplevel/nursery.ml new file mode 100644 index 000000000000..4f5b9cd8ef5f --- /dev/null +++ b/toplevel/nursery.ml @@ -0,0 +1,63 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* 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); *) + (* TODO unmarshal required files before fork + (need to parse args enough to find the file, then read it to find requires) *) + 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 () = 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 diff --git a/toplevel/nursery.mli b/toplevel/nursery.mli new file mode 100644 index 000000000000..7c6fa1941a5f --- /dev/null +++ b/toplevel/nursery.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* unit) -> string list -> unit diff --git a/toplevel/worker_main.ml b/toplevel/worker_main.ml new file mode 100644 index 000000000000..58c1a9ecfd9b --- /dev/null +++ b/toplevel/worker_main.ml @@ -0,0 +1,44 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* 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 diff --git a/toplevel/worker_main.mli b/toplevel/worker_main.mli new file mode 100644 index 000000000000..a1bc9634d32b --- /dev/null +++ b/toplevel/worker_main.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* unit diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml index 4b6ef278414c..6a4e184d5994 100644 --- a/vernac/loadpath.ml +++ b/vernac/loadpath.ml @@ -22,7 +22,7 @@ type t = { let load_vos_libraries = ref false -let load_paths = Summary.ref ([] : t list) ~stage:Summary.Stage.Synterp ~name:"LOADPATHS" +let load_paths = ref ([] : t list) let logical p = p.path_logical let physical p = p.path_physical From 87b26a99adc24b28e0d2cd68d1a72b33916033e5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 22 Jul 2026 17:39:16 +0200 Subject: [PATCH 2/3] nursery preload requires --- tools/coqdep/lib/args.ml | 2 +- toplevel/dune | 2 +- toplevel/nursery.ml | 85 +++++++++++++++++++++++++++++++++++++++- vernac/library.ml | 2 + vernac/library.mli | 2 + vernac/vernacinterp.ml | 8 +++- vernac/vernacinterp.mli | 4 ++ 7 files changed, 100 insertions(+), 5 deletions(-) diff --git a/tools/coqdep/lib/args.ml b/tools/coqdep/lib/args.ml index 31ebca9875cd..bddc1293f6dd 100644 --- a/tools/coqdep/lib/args.ml +++ b/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 () = diff --git a/toplevel/dune b/toplevel/dune index 61810cdf7cb1..b5275120a309 100644 --- a/toplevel/dune +++ b/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)))) diff --git a/toplevel/nursery.ml b/toplevel/nursery.ml index 4f5b9cd8ef5f..1795a3050452 100644 --- a/toplevel/nursery.ml +++ b/toplevel/nursery.ml @@ -16,6 +16,87 @@ let to_vo_path (x:Coqargs.vo_path) : Loadpath.vo_path = { 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 @@ -26,8 +107,7 @@ let rec loop self = 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); *) - (* TODO unmarshal required files before fork - (need to parse args enough to find the file, then read it to find requires) *) + 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? @@ -51,6 +131,7 @@ 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 diff --git a/vernac/library.ml b/vernac/library.ml index b8184f98e3cb..3040f2dcc398 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -105,6 +105,8 @@ type library_t = { library_vm : Vmlibrary.on_disk; } +let library_deps l = l.library_deps + (* This is a map from names to loaded libraries *) let libraries_table : library_t DirPath.Map.t ref = Summary.ref DirPath.Map.empty ~stage:Summary.Stage.Synterp ~name:"LIBRARY" diff --git a/vernac/library.mli b/vernac/library.mli index e3abc7e0a7b9..c6d25dc860ca 100644 --- a/vernac/library.mli +++ b/vernac/library.mli @@ -21,6 +21,8 @@ open Names (** Type of libraries loaded in memory *) type library_t +val library_deps : library_t -> (DirPath.t * Safe_typing.vodigest) array + (** {6 ... } Require = load in the environment *) val require_library_from_dirpath : library_t list -> unit diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 8e53d5be4e89..33b64d46b5a4 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -189,7 +189,13 @@ module Intern = struct Loadpath.Error.raise dp e end -let fs_intern = Intern.fs_intern +let base_fs_intern = Intern.fs_intern + +let fs_intern = ref Intern.fs_intern + +let set_fs_intern f = fs_intern := f + +let fs_intern dp = !fs_intern dp let interp_qed_delayed_proof ~proof ~st ~control (CAst.{loc; v = pe } as e) : Vernacstate.Interp.t = NewProfile.profile "interp-delayed-qed" (fun () -> diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index f8e47797fc2e..11dbd3d42f12 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -11,6 +11,10 @@ (** Regular intern using the filesystem *) val fs_intern : Library.Intern.t +val base_fs_intern : Library.Intern.t + +val set_fs_intern : Library.Intern.t -> unit + (** The main interpretation function of vernacular expressions *) val interp : intern:Library.Intern.t From 3fed6be7be1888797d17cbd3ead9a8140e92dc17 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 22 Jul 2026 17:47:07 +0200 Subject: [PATCH 3/3] force nursery mode in rocq makefile --- tools/CoqMakefile.in | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 789fd50a5390..efe4a40f41f7 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -418,22 +418,16 @@ ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) $(VDFILE) # Compilation targets ######################################################### -ifdef ROCQ_NURSERY all: $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-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 -else -all: - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all -endif .PHONY: all all.timing.diff: