[coq] Correctly handle composed stdlib after coq lang 0.8

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)

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
 ;;

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)

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 <<EOF
   > (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 <<EOF
+  > (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:

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