[coq] Allow to disable Coq language deprecation warning.

I had to adapt the warnings infra a little bit, IMHO that is fine, tho it would be nice to see if we can recover the vendor behavior. I also corrected the hint message a little bit, as it was a bit confusing IMHO, but will place that in the next commit as to keep diffs tidy. Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
ocaml · Dec 9, 2023 · 1edfd00 · 1edfd00
1 parent b7dadc5
commit 1edfd00
Show file tree

Hide file tree

Showing 53 changed files with 315 additions and 14 deletions.
diff --git a/doc/changes/9439_coq_disable_08_warning.md b/doc/changes/9439_coq_disable_08_warning.md
@@ -0,0 +1 @@
+- Allow to disable Coq 0.8 deprecation warning (#9439, @ejgallego)
diff --git a/src/dune_rules/coq/coq_stanza.ml b/src/dune_rules/coq/coq_stanza.ml
@@ -18,16 +18,24 @@ let coq_syntax =
 
 let already_warned = ref false
 
+let deprecated_coq_lang_lt_08_msg =
+  User_message.make
+    [ Pp.text
+        "Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will \
+         be removed in an upcoming Dune version."
+    ]
+;;
+
 let get_coq_syntax () =
   let* version = Dune_lang.Syntax.get_exn coq_syntax in
+  let* project = Dune_project.get_exn () in
   if version < (0, 8) && not !already_warned
   then (
     already_warned := true;
-    User_warning.emit
-      [ Pp.text
-          "Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and \
-           will be removed in an upcoming Dune version."
-      ]);
+    Warning_emit.emit_project
+      Warning.deprecated_coq_lang_lt_08
+      project
+      deprecated_coq_lang_lt_08_msg);
   return version
 ;;
 

diff --git a/src/dune_rules/warning.ml b/src/dune_rules/warning.ml
@@ -95,3 +95,10 @@ let escaping_paths_in_install_stanza =
 ;;
 
 let no_keep_locs = create ~default:(fun _ -> `Enabled) ~name:"no_keep_locs" ~since:(3, 11)
+
+let deprecated_coq_lang_lt_08 =
+  create
+    ~default:(fun _version -> `Enabled)
+    ~name:"deprecated_coq_lang_lt_08"
+    ~since:(3, 8)
+;;
diff --git a/src/dune_rules/warning.mli b/src/dune_rules/warning.mli
@@ -23,3 +23,4 @@ val missing_project_name : t
 
 val escaping_paths_in_install_stanza : t
 val no_keep_locs : t
+val deprecated_coq_lang_lt_08 : t
diff --git a/src/dune_rules/warning_emit.ml b/src/dune_rules/warning_emit.ml
@@ -16,20 +16,22 @@ let check_project warning project =
   Warning.Settings.active warnings warning version
 ;;
 
+let emit_hint warning =
+  [ Pp.concat
+      ~sep:Pp.space
+      [ Pp.text
+          "To disable this warning, add the following to your dune-project file:"
+      ; Pp.verbatim (sprintf "(%s disabled)" (Warning.name warning))
+      ]
+  ]
+;;
+
 let maybe_emit warning f = function
   | `Disabled -> Memo.return ()
   | `Enabled ->
     let+ message =
       let+ message = f () in
-      let hints =
-        [ Pp.concat
-            ~sep:Pp.space
-            [ Pp.text
-                "To disable this warning, add the following to your dune-project file:"
-            ; Pp.verbatim (sprintf "(%s disabled)" (Warning.name warning))
-            ]
-        ]
-      in
+      let hints = emit_hint warning in
       { message with User_message.hints }
     in
     User_warning.emit_message message
@@ -54,6 +56,17 @@ let emit t context f =
   >>= maybe_emit t f
 ;;
 
+let emit_project warning project message =
+  match check_project warning project with
+  | `Disabled -> ()
+  | `Enabled ->
+    let message =
+      let hints = emit_hint warning in
+      { message with User_message.hints }
+    in
+    User_warning.emit_message message
+;;
+
 module Bag = struct
   type decode =
     { active : Config.Toggle.t

diff --git a/src/dune_rules/warning_emit.mli b/src/dune_rules/warning_emit.mli
@@ -15,6 +15,8 @@ end
     generate the warning corresponding to [w] *)
 val emit : Warning.t -> Context.t -> (unit -> User_message.t Memo.t) -> unit Memo.t
 
+val emit_project : Warning.t -> Dune_project.t -> User_message.t -> unit
+
 module Bag : sig
   (** A set of warnings collected while parsing the dune language *)
   type t

diff --git a/test/blackbox-tests/test-cases/coq/base-unsound.t/run.t b/test/blackbox-tests/test-cases/coq/base-unsound.t/run.t
@@ -1,6 +1,8 @@
   $ dune build --display short --profile unsound --debug-dependency-path @all
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
         coqdep .basic.theory.d
           coqc foo.{glob,vo}
           coqc bar.{glob,vo}
diff --git a/test/blackbox-tests/test-cases/coq/base.t/run.t b/test/blackbox-tests/test-cases/coq/base.t/run.t
@@ -1,13 +1,17 @@
   $ dune build --display short --debug-dependency-path @all --always-show-command-line
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
         coqdep .basic.theory.d
           coqc foo.{glob,vo}
           coqc bar.{glob,vo}
 
   $ dune build --debug-dependency-path @default
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   lib: [
     "_build/install/default/lib/base/META"
     "_build/install/default/lib/base/dune-package"

diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/run.t b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/run.t
@@ -3,6 +3,8 @@ Testing composition with two boot libraries
   $ dune build
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   File "A/dune", line 4, characters 11-12:
   4 |  (theories B)
                  ^

diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodups.t/run.t b/test/blackbox-tests/test-cases/coq/compose-boot-nodups.t/run.t
@@ -3,6 +3,8 @@ Testing composition with two boot libraries
   $ dune build
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   Error: Cannot have more than one boot theory in scope:
   - B at B/dune:1
   - A at A/dune:1

diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/run.t b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/run.t
@@ -6,6 +6,8 @@ Composing library A depending on Coq but having `(stdlib no)`:
   $ dune build A
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   Module
   Prelude
   := Struct Inductive BootType : Set :=  boot : BootType | type : BootType. End
@@ -18,6 +20,8 @@ Composing library B depending on Coq but having `(stdlib yes)`:
   $ dune build B
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   Module
   Prelude
   := Struct Inductive BootType : Set :=  boot : BootType | type : BootType. End

diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/run.t b/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/run.t
@@ -3,5 +3,7 @@ Testing composition with a boot library with plugins
   $ dune build
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   plugin loaded
   plugin loaded
diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t b/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t
@@ -2,6 +2,8 @@ We check cycles are detected
   $ dune build
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   Error: Dependency cycle between:
      theory A in A/dune:2
   -> theory B in B/dune:2

diff --git a/test/blackbox-tests/test-cases/coq/compose-installed-compat.t/run.t b/test/blackbox-tests/test-cases/coq/compose-installed-compat.t/run.t
@@ -32,10 +32,14 @@ so this also tests that it won't be a problem.
   Entering directory 'B'
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   Leaving directory 'B'
   $ dune install --root B --prefix=$PWD --display=short
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   Installing $TESTCASE_ROOT/lib/B/META
   Installing $TESTCASE_ROOT/lib/B/dune-package
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmi

diff --git a/test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t b/test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t
@@ -1,6 +1,8 @@
   $ dune build --display short --debug-dependency-path @all
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
         ocamlc src_b/.ml_plugin_b.objs/byte/ml_plugin_b.{cmi,cmo,cmt}
       ocamldep src_b/.ml_plugin_b.objs/ml_plugin_b__Simple_b.impl.d
         ocamlc src_a/.ml_plugin_a.objs/byte/ml_plugin_a.{cmi,cmo,cmt}

diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/run.t b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/run.t
@@ -5,13 +5,17 @@ B will pick up the private one:
   $ dune build B
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   message = "I am the the private A "
        : string
 
 C picks up the private one too:
   $ dune build C
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   File "C/dune", line 4, characters 11-12:
   4 |  (theories A))
                  ^

diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/run.t b/test/blackbox-tests/test-cases/coq/compose-private.t/run.t
@@ -5,6 +5,8 @@ because a public theory cannot depend on a private theory.
   $ dune build
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   Hello
        : Set
   File "C/dune", line 4, characters 11-12:

diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/run.t
@@ -10,6 +10,8 @@ coqdep and coqc.
   $ dune build A
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   Module
   Prelude
   := Struct Inductive BootType : Set :=  boot : BootType | type : BootType. End
@@ -30,6 +32,8 @@ private boot library will be loaded implicitly.
   $ dune build B
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   private_boot
        : PrivateBootType
 
@@ -51,6 +55,8 @@ to fix this currently.
   $ dune build B
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   Error: Cannot have more than one boot theory in scope:
   - Coq at Coq/dune:1
   - Coq at B/Coq/dune:2

diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t
@@ -4,6 +4,8 @@ dependencies.
   $ dune build A
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   Error: Dependency cycle between:
      theory A in A/dune:2
   -> theory B in B/dune:2
@@ -17,6 +19,8 @@ dependencies.
   $ dune build B
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   Error: Dependency cycle between:
      theory B in B/dune:2
   -> theory C in C/dune:2
@@ -30,6 +34,8 @@ dependencies.
   $ dune build C
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   Error: Dependency cycle between:
      theory C in C/dune:2
   -> theory A in A/dune:2

diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t
@@ -4,6 +4,8 @@ dependency.
   $ dune build C
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   File "B/dune", line 4, characters 11-12:
   4 |  (theories A))
                  ^

diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-private-ambiguous.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects-private-ambiguous.t/run.t
@@ -11,6 +11,8 @@ which complains.
   $ dune build B
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   *** Warning: in file b.v, library a is required from root A and has not been found in the loadpath!
   File "./B/b.v", line 2, characters 0-24:
   Error: Cannot find a physical path bound to logical path a with prefix A.
@@ -20,6 +22,8 @@ which complains.
   $ dune build C
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   *** Warning: in file c.v, library a is required from root A and has not been found in the loadpath!
   *** Warning: in file a.v, library A is required from root C and has not been found in the loadpath!
   File "./C/c.v", line 2, characters 0-24:
@@ -41,10 +45,14 @@ which complains.
   $ dune build A
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
 
   $ dune build C/A_vendored
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   File "C/A_vendored/dune", line 1, characters 0-36:
   1 | (coq.theory
   2 |  (name A)

diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects.t/run.t
@@ -2,6 +2,8 @@ Testing composition of theories across a dune workspace
   $ dune build B
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   Hello
        : Set
 

diff --git a/test/blackbox-tests/test-cases/coq/compose-self.t/run.t b/test/blackbox-tests/test-cases/coq/compose-self.t/run.t
@@ -2,6 +2,8 @@ Composing a theory with itself should cause a cycle
   $ dune build
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   Error: Dependency cycle between:
      theory A in A/dune:2
   -> required by _build/default/A/.A.theory.d

diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t b/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t
@@ -4,6 +4,8 @@ depends on A.
   $ dune build
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
 
 We inspect the contents of the build directory.
 

diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t
@@ -4,6 +4,8 @@ defined as Foo.A. This changes the install layout of A.
   $ dune build
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
 
 Inspecting the build and install directory
   $ ls _build/install/default/lib/coq/user-contrib/Foo/A/a.vo

diff --git a/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/run.t b/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/run.t
@@ -2,6 +2,8 @@
   $ dune build
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
   lib: [
     "_build/install/default/lib/cvendor/META"
     "_build/install/default/lib/cvendor/dune-package"

diff --git a/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t
@@ -16,6 +16,8 @@
   $ dune build --display short --debug-dependency-path
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
         coqdep a/.a.theory.d
         coqdep b/.b.theory.d
           coqc a/Na_a.{cmi,cmxs},a/a.{glob,vo}
@@ -29,5 +31,7 @@
   $ dune build --display short --debug-dependency-path
   Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
   3.8 and will be removed in an upcoming Dune version.
+  Hint: To disable this warning, add the following to your dune-project file
+  (warnings ...) section: (deprecated_coq_lang_lt_08 disabled)
         coqdep b/.b.theory.d
           coqc b/Nb_b.{cmi,cmxs},b/b.{glob,vo}
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		- Allow to disable Coq 0.8 deprecation warning (#9439, @ejgallego)
Original file line number	Diff line number	Diff line change
Expand Up		@@ -23,3 +23,4 @@ val missing_project_name : t

		val escaping_paths_in_install_stanza : t
		val no_keep_locs : t
		val deprecated_coq_lang_lt_08 : t