coq: pass -boot only on 0.8

Signed-off-by: Ali Caglayan <alizter@gmail.com>

src/dune_rules/coq/coq_rules.ml

@@ -131,16 +131,17 @@ let theories_flags ~theories_deps =
     let+ libs = theories_deps in
     Command.Args.S (List.map ~f:theory_coqc_flag libs))
 
-let boot_flags t : _ Command.Args.t =
+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" ]
+  | `Bootstrap_prelude -> As ("-noinit" :: boot_flag)
   (* No special case *)
-  | `No_boot | `Bootstrap _ -> As []
+  | `No_boot | `Bootstrap _ -> As boot_flag
 
-let coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags :
-    _ Command.Args.t list =
+let coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags
+    ~coq_lang_version : _ Command.Args.t list =
   let file_flags : _ Command.Args.t list =
     [ Dyn (Resolve.Memo.read ml_flags)
     ; theories_flags ~theories_deps
@@ -149,7 +150,7 @@ let coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags :
     ; A wrapper_name
     ]
   in
-  [ A "-boot"; boot_flags boot_type; S file_flags ]
+  [ boot_flags ~coq_lang_version boot_type; S file_flags ]
 
 let native_includes ~dir =
   let* scope = Scope.DB.find_by_dir dir in
@@ -346,7 +347,8 @@ let setup_coqdep_for_theory_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name
   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)
+        (coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags
+           ~coq_lang_version)
     ; As [ "-dyndep"; "opt"; "-vos" ]
     ; Deps sources
     ]
@@ -431,7 +433,8 @@ let deps_of ~dir ~boot_type ~wrapper_name ~mode coq_module =
     Action_builder.paths deps
 
 let generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~mode ~coq_prog
-    ~stanza_flags ~ml_flags ~theories_deps ~theory_dirs coq_module =
+    ~stanza_flags ~ml_flags ~theories_deps ~theory_dirs ~coq_lang_version
+    coq_module =
   let+ coq_stanza_flags =
     let+ expander = Super_context.expander sctx ~dir in
     let coq_flags =
@@ -464,6 +467,7 @@ let generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~mode ~coq_prog
   in
   let file_flags =
     coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags
+      ~coq_lang_version
   in
   match coq_prog with
   | `Coqc ->
@@ -490,7 +494,8 @@ let setup_coqc_rule ~loc ~dir ~sctx ~coqc_dir ~file_targets ~stanza_flags
   let target_obj_files = Command.Args.Hidden_targets obj_files in
   let* args =
     generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~stanza_flags ~ml_flags
-      ~theories_deps ~theory_dirs ~mode ~coq_prog:`Coqc coq_module
+      ~theories_deps ~theory_dirs ~mode ~coq_lang_version ~coq_prog:`Coqc
+      coq_module
   in
   let deps_of = deps_of ~dir ~boot_type ~wrapper_name ~mode coq_module in
   let open Action_builder.With_targets.O in
@@ -730,7 +735,7 @@ let coqtop_args_theory ~sctx ~dir ~dir_contents (s : Coq_stanza.Theory.t)
   in
   generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~mode ~coq_prog:`Coqtop
     ~stanza_flags:s.buildable.flags ~ml_flags ~theories_deps ~theory_dirs
-    coq_module
+    ~coq_lang_version coq_module
 
 (******************************************************************************)
 (* Install rules *)
@@ -891,7 +896,7 @@ let coqtop_args_extraction ~sctx ~dir (s : Coq_stanza.Extraction.t) coq_module =
   let* mode = select_native_mode ~sctx ~dir s.buildable in
   generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~mode ~coq_prog:`Coqtop
     ~stanza_flags:s.buildable.flags ~ml_flags ~theories_deps
-    ~theory_dirs:Path.Build.Set.empty coq_module
+    ~theory_dirs:Path.Build.Set.empty ~coq_lang_version coq_module
 
 (* Version for export *)
 let deps_of ~dir ~use_stdlib ~wrapper_name ~mode ~coq_lang_version coq_module =

test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/A/a.v

@@ -1,4 +1,3 @@
-Print LoadPath.
 Fail Print Prelude.
 From Coq Require Import Prelude.
 Print Prelude.

test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/B/b.v

@@ -1,4 +1,3 @@
-Print LoadPath.
 Print Prelude.
 Require Import mytheory.
 Check Hello.

test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/run.t

@@ -4,13 +4,6 @@ importing ``stdlib`` enabled or disabled.
 Composing library A depending on Coq but having `(stdlib no)`:
 
   $ dune build A
-  Logical Path / Physical path:
-  A
-    $TESTCASE_ROOT/_build/default/A
-  Coq
-    $TESTCASE_ROOT/_build/default/Coq
-  Coq.Init
-    $TESTCASE_ROOT/_build/default/Coq/Init
   Module
   Prelude
   := Struct Inductive BootType : Set :=  boot : BootType | type : BootType. End
@@ -21,13 +14,6 @@ Composing library A depending on Coq but having `(stdlib no)`:
 Composing library B depending on Coq but having `(stdlib yes)`:
 
   $ dune build B
-  Logical Path / Physical path:
-  B
-    $TESTCASE_ROOT/_build/default/B
-  Coq
-    $TESTCASE_ROOT/_build/default/Coq
-  Coq.Init
-    $TESTCASE_ROOT/_build/default/Coq/Init
   Module
   Prelude
   := Struct Inductive BootType : Set :=  boot : BootType | type : BootType. End

test/blackbox-tests/test-cases/coq/compose-projects-boot.t/A/a.v

@@ -1,6 +1,5 @@
 
 
-Print LoadPath.
 Print Prelude.
 
 Require Import mytheory.

test/blackbox-tests/test-cases/coq/compose-projects-boot.t/run.t

@@ -8,13 +8,6 @@ When composing with a (boot) library, every library must have -boot passed to
 coqdep and coqc.
 
   $ dune build A
-  Logical Path / Physical path:
-  A
-    $TESTCASE_ROOT/_build/default/A
-  Coq
-    $TESTCASE_ROOT/_build/default/Coq
-  Coq.Init
-    $TESTCASE_ROOT/_build/default/Coq/Init
   Module
   Prelude
   := Struct Inductive BootType : Set :=  boot : BootType | type : BootType. End

test/blackbox-tests/test-cases/coq/coqdoc-with-boot.t/run.t

@@ -13,7 +13,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 -boot -R Coq Coq Coq/mytheory.v)
-  coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -noinit -R Coq Coq -R A A A/a.v)
-  coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -noinit -R Coq Coq Coq/Init/Prelude.v)
+  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)
   coqdoc -R ../Coq Coq -R . A --toc --html -d A.html a.v)

test/blackbox-tests/test-cases/coq/coqtop/coqtop-flags.t/run.t

@@ -8,7 +8,6 @@ The flags passed to coqc:
   -native-compiler on
   -nI lib/coq-core/kernel
   -nI .
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive
@@ -39,7 +38,6 @@ The flags passed to coqtop:
   -native-compiler on
   -nI lib/coq-core/kernel
   -nI $TESTCASE_ROOT/_build/default
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive

test/blackbox-tests/test-cases/coq/coqtop/coqtop-nested.t/run.t

@@ -7,7 +7,6 @@ Checking that we compute the directory and file for dune coq top correctly
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive
@@ -34,7 +33,6 @@ Checking that we compute the directory and file for dune coq top correctly
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive

test/blackbox-tests/test-cases/coq/coqtop/coqtop-recomp.t

@@ -25,7 +25,6 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587).
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive
@@ -51,7 +50,6 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587).
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive
@@ -82,7 +80,6 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587).
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive
@@ -110,7 +107,6 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587).
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive

test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t

@@ -5,7 +5,6 @@ All dune commands work when you run them in sub-directories, so this should be n
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive

test/blackbox-tests/test-cases/coq/flags.t

@@ -21,7 +21,6 @@ Test case: default flags
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive
@@ -58,7 +57,6 @@ TC: :standard
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive
@@ -94,7 +92,6 @@ TC: override :standard
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive
@@ -130,7 +127,6 @@ TC: add to :standard
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive
@@ -171,7 +167,6 @@ TC: extend in workspace + override standard
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive
@@ -206,7 +201,6 @@ TC: extend in workspace + override standard
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive
@@ -243,7 +237,6 @@ TC: extend in dune (env) + override standard
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive
@@ -280,7 +273,6 @@ TC: extend in dune (env) + standard
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive
@@ -322,7 +314,6 @@ TC: extend in dune (env) + workspace + standard
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -boot
   -I lib/coq/../coq-core/plugins/btauto
   -I lib/coq/../coq-core/plugins/cc
   -I lib/coq/../coq-core/plugins/derive

test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t

@@ -3,13 +3,7 @@ and the prelude is not imported
 
   $ dune build --display=short foo.vo
         coqdep .basic.theory.d
-  *** 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]
+          coqc foo.{glob,vo}
 
   $ dune build --display=short bar.vo
           coqc bar.{glob,vo} (exit 1)