From b6cf48c1f420690b10d1530356c34cbb1fdbd5ef Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 1 Dec 2023 12:15:24 +0100 Subject: [PATCH] [coq] Correctly handle composed stdlib after coq lang 0.8 Indeed the logic is a bit more complex than what we had. Current setup should work well now. Fixes #7909 , replaces #7942 This also reverts most of d92cb2e4fb8500aaaabd0d08b4959bf44eaa6157 Signed-off-by: Emilio Jesus Gallego Arias --- doc/changes/9347_fix_coq_boot_bug.md | 2 + src/dune_rules/coq/coq_rules.ml | 173 ++++++++++-------- .../test-cases/coq/coqdoc-with-boot.t/run.t | 6 +- .../test-cases/coq/failed-config.t/run.t | 34 +++- .../test-cases/coq/no-stdlib.t/run.t | 10 +- 5 files changed, 141 insertions(+), 84 deletions(-) create mode 100644 doc/changes/9347_fix_coq_boot_bug.md diff --git a/doc/changes/9347_fix_coq_boot_bug.md b/doc/changes/9347_fix_coq_boot_bug.md new file mode 100644 index 00000000000..7d8f468898b --- /dev/null +++ b/doc/changes/9347_fix_coq_boot_bug.md @@ -0,0 +1,2 @@ +- [coq] Fix bug in computation of flags when composed with boot theories. + (#9347, fixes #7909, @ejgallego) diff --git a/src/dune_rules/coq/coq_rules.ml b/src/dune_rules/coq/coq_rules.ml index 28e8b802f48..d197cc05a27 100644 --- a/src/dune_rules/coq/coq_rules.ml +++ b/src/dune_rules/coq/coq_rules.ml @@ -163,23 +163,94 @@ let theories_flags ~theories_deps = Command.Args.S (List.map ~f:theory_coqc_flag libs)) ;; -let boot_flags ~coq_lang_version t : _ Command.Args.t = - let boot_flag = if coq_lang_version >= (0, 8) then [ "-boot" ] else [] in - match t with - (* We are compiling the prelude itself - [should be replaced with (per_file ...) flags] *) - | `Bootstrap_prelude -> As ("-noinit" :: boot_flag) - (* No special case *) - | `No_boot | `Bootstrap _ -> As boot_flag -;; +module Bootstrap : sig + type t = + | Implicit (** Use implicit stdlib loading, for coq lang versions < 0.8 *) + | No_stdlib + (** We are in >= 0.8, however the user set stdlib = no + , or we are compiling the prelude *) + | Stdlib of Coq_lib.t (** Regular case in >= 0.8 (or in < 0.8 + (boot) was used *) -let coqc_file_flags - ~dir - ~theories_deps - ~wrapper_name - ~boot_type - ~ml_flags - ~coq_lang_version + val empty : t Memo.t + + val make + : dir:Path.Build.t + -> use_stdlib:bool + -> wrapper_name:string + -> coq_lang_version:Syntax.Version.t + -> Coq_module.t + -> t Memo.t + + val flags : t -> 'a Command.Args.t +end = struct + type t = + | Implicit (** Use implicit stdlib loading, for coq lang versions < 0.8 *) + | No_stdlib + (** We are in >= 0.8, however the user set stdlib = no + , or we are compiling the prelude *) + | Stdlib of Coq_lib.t (** Regular case in >= 0.8 (or in < 0.8 + (boot) was used *) + + (* For empty set of modules, we return Prelude which is kinda + conservative. *) + let empty = Memo.return No_stdlib + + (* Hack to know if a module is a prelude module *) + let check_init_module bootlib wrapper_name coq_module = + String.equal (Coq_lib_name.wrapper (Coq_lib.name bootlib)) wrapper_name + && Option.equal + String.equal + (List.hd_opt (Coq_module.prefix coq_module)) + (Some "Init") + ;; + + (* [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+ boot_lib = + Scope.coq_libs scope + >>= Coq_lib.DB.resolve_boot ~coq_lang_version + |> Resolve.Memo.read_memo + in + if use_stdlib + then ( + match boot_lib with + | None -> + if coq_lang_version >= (0, 8) + then + User_error.raise + [ Pp.text + "Couldn't find Coq standard library, and theory is not using (stdlib no)" + ] + else Implicit + | Some (_loc, boot_lib) -> + (* TODO: replace with per_file flags *) + let init = check_init_module boot_lib wrapper_name coq_module in + if init + then No_stdlib + else if coq_lang_version >= (0, 8) + then Stdlib boot_lib + else ( + (* Check if the boot library is in scope or not; note!! + This will change once we install dune-package files + for installed libs *) + match boot_lib with + | Legacy _ -> Implicit + | Dune _ -> Stdlib boot_lib)) + else No_stdlib + ;; + + let flags t : _ Command.Args.t = + match t with + | Implicit -> As [] + | Stdlib _ -> As [ "-boot" ] + | No_stdlib -> As [ "-noinit"; "-boot" ] + ;; +end + +let coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags : _ Command.Args.t list = let file_flags : _ Command.Args.t list = @@ -190,7 +261,7 @@ let coqc_file_flags ; A wrapper_name ] in - [ boot_flags ~coq_lang_version boot_type; S file_flags ] + [ Bootstrap.flags boot_type; S file_flags ] ;; let native_includes ~dir = @@ -349,38 +420,6 @@ let ml_flags_and_ml_pack_rule Resolve.Memo.map ~f:fst res, mlpack_rule ;; -(* the internal boot flag determines if the Coq "standard library" is being - built, in case we need to explicitly tell Coq where the build artifacts are - and add `Init.Prelude.vo` as a dependency; there is a further special case - when compiling the prelude, in this case we also need to tell Coq not to - try to load the prelude. *) -let boot_type ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module = - let* scope = Scope.DB.find_by_dir dir in - let+ boot_lib = - Scope.coq_libs scope - >>= Coq_lib.DB.resolve_boot ~coq_lang_version - |> Resolve.Memo.read_memo - in - if use_stdlib - then ( - match boot_lib with - | None -> - `No_boot - (* XXX: use_stdlib + no_boot is - actually a workspace error, cleanup *) - | Some (_loc, lib) -> - (* This is here as an optimization, TODO; replace with per_file flags *) - let init = - String.equal (Coq_lib_name.wrapper (Coq_lib.name lib)) wrapper_name - && Option.equal - String.equal - (List.hd_opt (Coq_module.prefix coq_module)) - (Some "Init") - in - if init then `Bootstrap_prelude else `Bootstrap lib) - else `Bootstrap_prelude -;; - let dep_theory_file ~dir ~wrapper_name = Path.Build.relative dir ("." ^ wrapper_name) |> Path.Build.set_extension ~ext:".theory.d" @@ -404,20 +443,14 @@ let setup_coqdep_for_theory_rule the more conservative path and pass -boot, we don't care here about -noinit as coqdep ignores it *) match coq_modules with - | [] -> Memo.return `Bootstrap_prelude - | m :: _ -> boot_type ~dir ~use_stdlib ~wrapper_name ~coq_lang_version m + | [] -> Bootstrap.empty + | m :: _ -> Bootstrap.make ~dir ~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 let file_flags = [ Command.Args.S - (coqc_file_flags - ~dir - ~theories_deps - ~wrapper_name - ~boot_type - ~ml_flags - ~coq_lang_version) + (coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags) ; As [ "-dyndep"; "opt"; "-vos" ] ; Deps sources ] @@ -524,8 +557,8 @@ let deps_of ~dir ~boot_type ~wrapper_name ~mode coq_module = let deps = let prelude = "Init/Prelude.vo" in match boot_type with - | `No_boot | `Bootstrap_prelude -> deps - | `Bootstrap lib -> Path.relative (Coq_lib.obj_root lib) prelude :: deps + | Bootstrap.No_stdlib | Bootstrap.Implicit -> deps + | Bootstrap.Stdlib lib -> Path.relative (Coq_lib.obj_root lib) prelude :: deps in Action_builder.paths deps ;; @@ -541,7 +574,6 @@ let generic_coq_args ~ml_flags ~theories_deps ~theory_dirs - ~coq_lang_version coq_module = let+ coq_stanza_flags = @@ -575,13 +607,7 @@ let generic_coq_args coqc_native_flags ~sctx ~dir ~theories_deps ~theory_dirs ~mode in let file_flags = - coqc_file_flags - ~dir - ~theories_deps - ~wrapper_name - ~boot_type - ~ml_flags - ~coq_lang_version + coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags in match coq_prog with | `Coqc -> @@ -611,7 +637,7 @@ let setup_coqc_rule = (* Process coqdep and generate rules *) let* boot_type = - boot_type ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module + Bootstrap.make ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module in let* coqc = coqc ~loc ~dir ~sctx in let obj_files = @@ -635,7 +661,6 @@ let setup_coqc_rule ~theories_deps ~theory_dirs ~mode - ~coq_lang_version ~coq_prog:`Coqc coq_module in @@ -900,7 +925,7 @@ let coqtop_args_theory ~sctx ~dir ~dir_contents (s : Coq_stanza.Theory.t) coq_mo let name = snd s.name in let use_stdlib = s.buildable.use_stdlib in let* boot_type = - boot_type ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module + Bootstrap.make ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module in let* coq_dir_contents = Dir_contents.coq dir_contents in let theory_dirs = @@ -917,7 +942,6 @@ let coqtop_args_theory ~sctx ~dir ~dir_contents (s : Coq_stanza.Theory.t) coq_mo ~ml_flags ~theories_deps ~theory_dirs - ~coq_lang_version coq_module ;; @@ -1100,7 +1124,7 @@ let coqtop_args_extraction ~sctx ~dir (s : Coq_stanza.Extraction.t) coq_module = in let wrapper_name = "DuneExtraction" in let* boot_type = - boot_type ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module + Bootstrap.make ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module in let* mode = select_native_mode ~sctx ~dir s.buildable in generic_coq_args @@ -1114,7 +1138,6 @@ let coqtop_args_extraction ~sctx ~dir (s : Coq_stanza.Extraction.t) coq_module = ~ml_flags ~theories_deps ~theory_dirs:Path.Build.Set.empty - ~coq_lang_version coq_module ;; @@ -1123,7 +1146,7 @@ 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 - (boot_type ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module) + (Bootstrap.make ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module) in deps_of ~dir ~boot_type ~wrapper_name ~mode coq_module ;; diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-with-boot.t/run.t b/test/blackbox-tests/test-cases/coq/coqdoc-with-boot.t/run.t index 8bf53d54888..e0cd2c19b92 100644 --- a/test/blackbox-tests/test-cases/coq/coqdoc-with-boot.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coqdoc-with-boot.t/run.t @@ -15,7 +15,7 @@ Testing coqdoc when composed with a boot library Dune should be passing '--coqlib' to coqdoc, but it doesn't. This is a bug. $ cat _build/log | sed 's/$ (cd .*coqc/coqc/' | sed 's/$ (cd .*coqdoc/coqdoc/' | sed '/# /d' | sed '/> /d' | sort - coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R Coq Coq Coq/mytheory.v) - coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -noinit -R Coq Coq -R A A A/a.v) - coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -noinit -R Coq Coq Coq/Init/Prelude.v) + coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -R Coq Coq Coq/mytheory.v) + coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -noinit -boot -R Coq Coq -R A A A/a.v) + coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -noinit -boot -R Coq Coq Coq/Init/Prelude.v) coqdoc -R ../Coq Coq -R . A --toc --html -d A.html a.v) diff --git a/test/blackbox-tests/test-cases/coq/failed-config.t/run.t b/test/blackbox-tests/test-cases/coq/failed-config.t/run.t index b64e0b23fd6..d3998760f80 100644 --- a/test/blackbox-tests/test-cases/coq/failed-config.t/run.t +++ b/test/blackbox-tests/test-cases/coq/failed-config.t/run.t @@ -32,7 +32,8 @@ These should fail. > coqc --config 2> /dev/null [1] -Now we create a simple project that uses this coqc wrapper. +Now we create a simple project that uses this coqc wrapper, should +fail when the stdlib cannot be determined $ cat > dune < (coq.theory @@ -47,11 +48,36 @@ Now we create a simple project that uses this coqc wrapper. > (write-file a.v ""))) > EOF +Should fail: first warning that installed theories are being skipped due to the +failure, then, as the library requires the stdlib, it fails: + $ FAIL_CONFIG=1 \ + > dune build + Warning: Skipping installed theories due to 'coqc --config' failure: + - $TESTCASE_ROOT/bin/coqc --config failed with exit code 1. + Hint: Try running 'coqc --config' manually to see the error. + Error: Couldn't find Coq standard library, and theory is not using (stdlib + no) + [1] + Here we build a simple Coq project. Neither a failing --config or --print-version should -block this. +block this as it doesn't depend on the stdlib. + + $ cat > dune < (coq.theory + > (flags -noinit) + > (name foo) + > (stdlib no)) + > + > (rule + > (deps + > (env_var FAIL_VERSION) + > (env_var FAIL_CONFIG)) + > (action + > (write-file a.v ""))) + > EOF -Should succeed, but should warn that installed theories are being skipped due to the -failure. +Should succeed, warning that installed theories are being skipped due to the +failure (c.f. #8958): $ FAIL_CONFIG=1 \ > dune build Warning: Skipping installed theories due to 'coqc --config' failure: diff --git a/test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t b/test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t index 48499436ab2..382f1c2152a 100644 --- a/test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t +++ b/test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t @@ -1,11 +1,17 @@ Test that when `(stdlib no)` is provided, the standard library is not bound to `Coq` -and the prelude is not imported +and the prelude is not imported; we expect the below two tests to fail. $ dune build --display=short foo.vo Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. coqdep .basic.theory.d - coqc foo.{glob,vo} + *** Warning: in file foo.v, library Prelude is required from root Coq and has not been found in the loadpath! + coqc foo.{glob,vo} (exit 1) + File "./foo.v", line 1, characters 0-32: + Error: Cannot find a physical path bound to logical path + Prelude with prefix Coq. + + [1] $ dune build --display=short bar.vo Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune