From 60eca4230e5abf5ed379fc927264b0389b93d653 Mon Sep 17 00:00:00 2001 From: Rudi Grinberg Date: Fri, 26 Jan 2024 16:31:47 -0700 Subject: [PATCH] fix(coq): delay boot type detection Signed-off-by: Rudi Grinberg --- src/dune_rules/coq/coq_rules.ml | 50 +++++++++++++++++++-------------- 1 file changed, 29 insertions(+), 21 deletions(-) diff --git a/src/dune_rules/coq/coq_rules.ml b/src/dune_rules/coq/coq_rules.ml index 47edce28fdfa..ceb637121d6e 100644 --- a/src/dune_rules/coq/coq_rules.ml +++ b/src/dune_rules/coq/coq_rules.ml @@ -200,15 +200,15 @@ module Bootstrap : sig | Stdlib of Coq_lib.t (** Regular case in >= 0.8 (or in < 0.8 (boot) was used *) - val empty : t Memo.t + val empty : t val make - : dir:Path.Build.t + : scope:Scope.t -> use_stdlib:bool -> wrapper_name:string -> coq_lang_version:Syntax.Version.t -> Coq_module.t - -> t Memo.t + -> t Resolve.Memo.t val flags : t -> 'a Command.Args.t end = struct @@ -222,7 +222,7 @@ end = struct (* For empty set of modules, we return Prelude which is kinda conservative. *) - let empty = Memo.return No_stdlib + let empty = No_stdlib (* Hack to know if a module is a prelude module *) let check_init_module bootlib wrapper_name coq_module = @@ -235,12 +235,12 @@ end = struct (* [Boostrap.t] determines, for a concrete Coq module, how the Coq "standard library" is being handled. See the main modes above. *) - let make ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module = - let* scope = Scope.DB.find_by_dir dir in + let make ~scope ~use_stdlib ~wrapper_name ~coq_lang_version coq_module = + let open Resolve.Memo.O in let+ boot_lib = Scope.coq_libs scope + |> Resolve.Memo.lift_memo >>= Coq_lib.DB.resolve_boot ~coq_lang_version - |> Resolve.Memo.read_memo in if use_stdlib then ( @@ -289,7 +289,8 @@ let coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags ; A wrapper_name ] in - [ Bootstrap.flags boot_type; S file_flags ] + let boot_flags = Resolve.Memo.read boot_type |> Action_builder.map ~f:Bootstrap.flags in + [ Dyn boot_flags; S file_flags ] ;; let native_includes ~dir = @@ -454,6 +455,7 @@ let dep_theory_file ~dir ~wrapper_name = ;; let setup_coqdep_for_theory_rule + ~scope ~sctx ~dir ~loc @@ -466,13 +468,13 @@ let setup_coqdep_for_theory_rule ~coq_lang_version coq_modules = - let* boot_type = + let boot_type = (* If coq_modules are empty it doesn't really matter, so we take the more conservative path and pass -boot, we don't care here about -noinit as coqdep ignores it *) match coq_modules with - | [] -> Bootstrap.empty - | m :: _ -> Bootstrap.make ~dir ~use_stdlib ~wrapper_name ~coq_lang_version m + | [] -> Resolve.Memo.return Bootstrap.empty + | m :: _ -> Bootstrap.make ~scope ~use_stdlib ~wrapper_name ~coq_lang_version m in (* coqdep needs the full source + plugin's mlpack to be present :( *) let sources = List.rev_map ~f:Coq_module.source coq_modules in @@ -574,6 +576,7 @@ let deps_of ~dir ~boot_type ~wrapper_name ~mode coq_module = Path.set_extension ~ext (Coq_module.source coq_module) in let* dep_map = get_dep_map ~dir ~wrapper_name in + let* boot_type = Resolve.Memo.read boot_type in match Dep_map.find dep_map vo_target with | None -> Code_error.raise @@ -649,6 +652,7 @@ let generic_coq_args ;; let setup_coqc_rule + ~scope ~loc ~dir ~sctx @@ -665,8 +669,8 @@ let setup_coqc_rule coq_module = (* Process coqdep and generate rules *) - let* boot_type = - Bootstrap.make ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module + let boot_type = + Bootstrap.make ~scope ~use_stdlib ~wrapper_name ~coq_lang_version coq_module in let* coqc = coqc ~loc ~dir ~sctx in let obj_files = @@ -910,6 +914,7 @@ let setup_theory_rules ~sctx ~dir ~dir_contents (s : Coq_stanza.Theory.t) = let* mode = select_native_mode ~sctx ~dir s.buildable in (* First we setup the rule calling coqdep *) setup_coqdep_for_theory_rule + ~scope ~sctx ~dir ~loc @@ -925,6 +930,7 @@ let setup_theory_rules ~sctx ~dir ~dir_contents (s : Coq_stanza.Theory.t) = coq_modules ~f: (setup_coqc_rule + ~scope ~loc ~dir ~sctx @@ -954,8 +960,8 @@ let coqtop_args_theory ~sctx ~dir ~dir_contents (s : Coq_stanza.Theory.t) coq_mo let* mode = select_native_mode ~sctx ~dir s.buildable in let name = snd s.name in let use_stdlib = s.buildable.use_stdlib in - let* boot_type = - Bootstrap.make ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module + let boot_type = + Bootstrap.make ~scope ~use_stdlib ~wrapper_name ~coq_lang_version coq_module in let* coq_dir_contents = Dir_contents.coq dir_contents in let theory_dirs = @@ -1117,6 +1123,7 @@ let setup_extraction_rules ~sctx ~dir ~dir_contents (s : Coq_stanza.Extraction.t in let* mode = select_native_mode ~sctx ~dir s.buildable in setup_coqdep_for_theory_rule + ~scope ~sctx ~dir ~loc @@ -1129,6 +1136,7 @@ let setup_extraction_rules ~sctx ~dir ~dir_contents (s : Coq_stanza.Extraction.t ~coq_lang_version [ coq_module ] >>> setup_coqc_rule + ~scope ~file_targets ~stanza_flags:s.buildable.flags ~sctx @@ -1154,8 +1162,8 @@ let coqtop_args_extraction ~sctx ~dir (s : Coq_stanza.Extraction.t) coq_module = extraction_context ~context ~scope ~coq_lang_version s.buildable in let wrapper_name = "DuneExtraction" in - let* boot_type = - Bootstrap.make ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module + let boot_type = + Bootstrap.make ~scope ~use_stdlib ~wrapper_name ~coq_lang_version coq_module in let* mode = select_native_mode ~sctx ~dir s.buildable in generic_coq_args @@ -1174,10 +1182,10 @@ let coqtop_args_extraction ~sctx ~dir (s : Coq_stanza.Extraction.t) coq_module = (* Version for export *) let deps_of ~dir ~use_stdlib ~wrapper_name ~mode ~coq_lang_version coq_module = - let open Action_builder.O in - let* boot_type = - Action_builder.of_memo - (Bootstrap.make ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module) + let boot_type = + let open Memo.O in + let* scope = Scope.DB.find_by_dir dir in + Bootstrap.make ~scope ~use_stdlib ~wrapper_name ~coq_lang_version coq_module in deps_of ~dir ~boot_type ~wrapper_name ~mode coq_module ;;