From c5f978cec752586dbfada83b177b7b9e16b5b2a2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 9 Dec 2023 10:51:30 +0100 Subject: [PATCH] [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 --- doc/changes/9439_coq_disable_08_warning.md | 1 + src/dune_rules/coq/coq_stanza.ml | 25 ++++++-- src/dune_rules/warning_emit.ml | 11 ++++ src/dune_rules/warning_emit.mli | 2 + .../test-cases/coq/base-unsound.t/run.t | 2 + .../test-cases/coq/base.t/run.t | 4 ++ .../coq/compose-boot-nodeps.t/run.t | 2 + .../coq/compose-boot-nodups.t/run.t | 2 + .../coq/compose-boot-nostdlib.t/run.t | 4 ++ .../coq/compose-boot-plugins.t/run.t | 2 + .../test-cases/coq/compose-cycle.t/run.t | 2 + .../coq/compose-installed-compat.t/run.t | 4 ++ .../test-cases/coq/compose-plugin.t/run.t | 2 + .../coq/compose-private-ambiguous.t/run.t | 4 ++ .../test-cases/coq/compose-private.t/run.t | 2 + .../coq/compose-projects-boot.t/run.t | 6 ++ .../coq/compose-projects-cycle.t/run.t | 6 ++ .../coq/compose-projects-missing.t/run.t | 2 + .../run.t | 8 +++ .../test-cases/coq/compose-projects.t/run.t | 2 + .../test-cases/coq/compose-self.t/run.t | 2 + .../test-cases/coq/compose-simple.t/run.t | 2 + .../test-cases/coq/compose-sub-theory.t/run.t | 2 + .../test-cases/coq/compose-two-scopes.t/run.t | 2 + .../test-cases/coq/coqdep-on-rebuild.t/run.t | 4 ++ .../coq/coqdoc-dir-target-clash.t/run.t | 2 + .../coq/coqdoc-multi-theory.t/run.t | 8 +++ .../test-cases/coq/coqdoc-with-boot.t/run.t | 2 + .../test-cases/coq/coqdoc.t/run.t | 6 ++ .../coq/coqtop/coqtop-flags.t/run.t | 4 ++ .../coq/coqtop/coqtop-nested.t/run.t | 8 +++ .../test-cases/coq/coqtop/coqtop-recomp.t | 8 +++ .../test-cases/coq/coqtop/coqtop-root.t/run.t | 2 + .../coq/deprecate-libraries.t/run.t | 4 ++ .../coq/deprecate-public_name.t/run.t | 4 ++ .../test-cases/coq/empty-modules.t/run.t | 2 + test/blackbox-tests/test-cases/coq/env.t | 64 +++++++++++++++++++ .../test-cases/coq/extraction/extract.t | 2 + .../coq/extraction/extraction-patch.t/run.t | 4 ++ test/blackbox-tests/test-cases/coq/flags.t | 18 ++++++ .../test-cases/coq/github5532.t | 2 + .../coq/lang_08_warning_disable/run.t | 37 +++++++++++ .../test-cases/coq/ml-lib.t/run.t | 2 + .../test-cases/coq/native-compose.t/run.t | 4 ++ .../test-cases/coq/native-single.t/run.t | 4 ++ .../test-cases/coq/no-stdlib.t/run.t | 4 ++ .../test-cases/coq/plugin-meta.t/run.t | 2 + .../test-cases/coq/plugin-private.t/run.t | 2 + .../coq/public-dep-on-private.t/run.t | 2 + .../test-cases/coq/rec-module.t/run.t | 4 ++ .../theory-stanza-duplicate-module.t/run.t | 2 + 51 files changed, 303 insertions(+), 5 deletions(-) create mode 100644 doc/changes/9439_coq_disable_08_warning.md create mode 100644 test/blackbox-tests/test-cases/coq/lang_08_warning_disable/run.t diff --git a/doc/changes/9439_coq_disable_08_warning.md b/doc/changes/9439_coq_disable_08_warning.md new file mode 100644 index 000000000000..30703eeb5221 --- /dev/null +++ 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 index 083a08935bee..b80fbe4608cf 100644 --- a/src/dune_rules/coq/coq_stanza.ml +++ b/src/dune_rules/coq/coq_stanza.ml @@ -18,16 +18,31 @@ let coq_syntax = let already_warned = ref false +let deprecated_coq_lang_lt_08 = + Warning.make + ~default:(fun _version -> `Enabled) + ~name:"deprecated_coq_lang_lt_08" + ~since:(3, 8) +;; + +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 + deprecated_coq_lang_lt_08 + project + deprecated_coq_lang_lt_08_msg); return version ;; diff --git a/src/dune_rules/warning_emit.ml b/src/dune_rules/warning_emit.ml index 99060a8e8a94..bcdcdaf3015a 100644 --- a/src/dune_rules/warning_emit.ml +++ b/src/dune_rules/warning_emit.ml @@ -55,6 +55,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 index 9cdc7ad18747..780cb08fb70a 100644 --- 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 index 029785d434f0..d18fc47294ac 100644 --- 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 index e4ac0c250bc9..0cb876900bbe 100644 --- a/test/blackbox-tests/test-cases/coq/base.t/run.t +++ b/test/blackbox-tests/test-cases/coq/base.t/run.t @@ -1,6 +1,8 @@ $ 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} @@ -8,6 +10,8 @@ $ 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 index 80792fd1bc99..dd88383d4fa3 100644 --- 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 index 9323097b87eb..fe9d705d6926 100644 --- 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 index 16a5f5158430..e8f58d46d3a3 100644 --- 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 index a29fa2406513..baf938624aed 100644 --- 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 index 5374d70d13a4..87ecbc2a5359 100644 --- 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 index 8033484073a9..a9aca2bc9fa7 100644 --- 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 index fabc761c6365..47b798a69b66 100644 --- 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 index 9fa9803d2a78..6bfc4042d14e 100644 --- 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,6 +5,8 @@ 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 @@ -12,6 +14,8 @@ 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 index ce9de2e0f58e..2666a2dd7d26 100644 --- 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 index fd656ab43aca..2ef8e18d612f 100644 --- 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 index 3fa34c031582..c664811aba0f 100644 --- 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 index c69835a565aa..2e67285a788a 100644 --- 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 index 3f7ead354a5d..73b8cfa52e3e 100644 --- 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 index 4ebbd1a4420b..63251790972a 100644 --- 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 index 0817a2a53dea..8b4ee745609e 100644 --- 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 index d42d195b738e..8cfaf8020584 100644 --- 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 index 45dd4d53ee21..bbc40d5eed30 100644 --- 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 index b5e8c884fb9b..2255e9c78417 100644 --- 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 index b06db944e972..db4155cb44d1 100644 --- 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} diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/run.t b/test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/run.t index 163f15b18655..0ea279133d48 100644 --- a/test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/run.t @@ -3,6 +3,8 @@ directory targets. Notice how the tex one fails before html one. $ dune build @check 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 "dune", line 9, characters 0-116: 9 | (rule 10 | (targets diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/run.t b/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/run.t index 3bc7da766d93..59c8da096b78 100644 --- a/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/run.t @@ -5,6 +5,8 @@ First we build the doc alias for the first theory $ dune build @A/doc 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) The first theory doc is built $ ls _build/default/A/A.html A.AA.aa.html @@ -22,6 +24,8 @@ Next we build the doc for the second theory $ dune build @B/doc 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) Check that the first theory doc is not built $ ls _build/default/A/ AA @@ -43,6 +47,8 @@ Next we test the LaTeX targets in the same manner $ dune build @A/doc-latex 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) The first theory doc is built $ ls _build/default/A/A.tex A.AA.aa.tex @@ -58,6 +64,8 @@ Next we build the doc for the second theory $ dune build @B/doc-latex 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) Check that the first theory doc is not built $ ls _build/default/A AA 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 e0cd2c19b929..c8b4c47dec27 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 @@ -3,6 +3,8 @@ Testing coqdoc when composed with a boot library $ dune build A/A.html 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) $ ls _build/default/A A.html diff --git a/test/blackbox-tests/test-cases/coq/coqdoc.t/run.t b/test/blackbox-tests/test-cases/coq/coqdoc.t/run.t index eb31d0afeac1..d7fcb041ccdf 100644 --- a/test/blackbox-tests/test-cases/coq/coqdoc.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coqdoc.t/run.t @@ -2,6 +2,8 @@ We build the coqdoc html target: $ dune build basic.html/ 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) Now we inspect it: $ ls _build/default/basic.html @@ -15,6 +17,8 @@ We build the coqdoc latex target: $ dune build basic.tex/ 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) Now we inspect it: $ ls _build/default/basic.tex @@ -27,6 +31,8 @@ Next from a clean build we make sure that @all does *not* build any doc targets: $ dune build @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) Note that this currently works due to a bug in @all detecting directory targets. $ ls _build/default META.base diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-flags.t/run.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-flags.t/run.t index e664348423e9..a2784b86b126 100644 --- a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-flags.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-flags.t/run.t @@ -4,6 +4,8 @@ The flags passed to coqc: $ dune build && tail -1 _build/log | ../../scrub_coq_args.sh 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) coqc -w -notation-overridden -w -deprecated-native-compiler-option -native-output-dir . @@ -39,6 +41,8 @@ The flags passed to coqtop: $ dune coq top --toplevel=echo Test.v | ../../scrub_coq_args.sh 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) -topfile $TESTCASE_ROOT/_build/default/Test.v -w -notation-overridden -w -deprecated-native-compiler-option -native-output-dir . diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-nested.t/run.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-nested.t/run.t index 5b9ef1f19a4d..16149a9320bf 100644 --- a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-nested.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-nested.t/run.t @@ -3,12 +3,18 @@ Checking that we compute the directory and file for dune coq top correctly $ dune build theories/c.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. + Hint: To disable this warning, add the following to your dune-project file + (warnings ...) section: (deprecated_coq_lang_lt_08 disabled) $ dune build theories/b/b.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. + Hint: To disable this warning, add the following to your dune-project file + (warnings ...) section: (deprecated_coq_lang_lt_08 disabled) $ dune coq top --toplevel=echo theories/c.v | ../../scrub_coq_args.sh 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) -topfile $TESTCASE_ROOT/_build/default/theories/c.v -w -deprecated-native-compiler-option -w -native-compiler-disabled @@ -40,6 +46,8 @@ Checking that we compute the directory and file for dune coq top correctly $ dune coq top --toplevel=echo theories/b/b.v | ../../scrub_coq_args.sh 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) -topfile $TESTCASE_ROOT/_build/default/theories/b/b.v -w -deprecated-native-compiler-option -w -native-compiler-disabled diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-recomp.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-recomp.t index efe6ffa11fc5..53689c109cbd 100644 --- a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-recomp.t +++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-recomp.t @@ -21,6 +21,8 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587). $ dune coq top --display short --toplevel echo dir/bar.v | ../scrub_coq_args.sh 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 dir/.basic.theory.d coqc dir/foo.{glob,vo} -topfile $TESTCASE_ROOT/_build/default/dir/bar.v @@ -53,6 +55,8 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587). $ dune coq top --display short --toplevel echo dir/bar.v | ../scrub_coq_args.sh 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) -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -w -deprecated-native-compiler-option -w -native-compiler-disabled @@ -85,6 +89,8 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587). Entering directory '..' 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 dir/.basic.theory.d coqc dir/foo.{glob,vo} Leaving directory '..' @@ -119,6 +125,8 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587). Entering directory '..' 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 '..' -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -w -deprecated-native-compiler-option diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t index 89fe2bc9f683..5dc6561a0ecd 100644 --- a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t @@ -3,6 +3,8 @@ All dune commands work when you run them in sub-directories, so this should be n $ dune coq top --toplevel=echo -- theories/foo.v | ../../scrub_coq_args.sh 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) -topfile $TESTCASE_ROOT/_build/default/theories/foo.v -w -deprecated-native-compiler-option -w -native-compiler-disabled diff --git a/test/blackbox-tests/test-cases/coq/deprecate-libraries.t/run.t b/test/blackbox-tests/test-cases/coq/deprecate-libraries.t/run.t index d02e625c891a..3ecd488de901 100644 --- a/test/blackbox-tests/test-cases/coq/deprecate-libraries.t/run.t +++ b/test/blackbox-tests/test-cases/coq/deprecate-libraries.t/run.t @@ -12,6 +12,8 @@ The libraries field is deprecated $ 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 "dune", line 7, characters 1-20: 7 | (libraries bar.foo)) ^^^^^^^^^^^^^^^^^^^ @@ -33,6 +35,8 @@ Having both a libraries and plugins field is an error $ 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 "dune", line 7, characters 1-20: 7 | (libraries bar.foo) ^^^^^^^^^^^^^^^^^^^ diff --git a/test/blackbox-tests/test-cases/coq/deprecate-public_name.t/run.t b/test/blackbox-tests/test-cases/coq/deprecate-public_name.t/run.t index 6e5a18e53b38..4561759b6656 100644 --- a/test/blackbox-tests/test-cases/coq/deprecate-public_name.t/run.t +++ b/test/blackbox-tests/test-cases/coq/deprecate-public_name.t/run.t @@ -13,6 +13,8 @@ public_name field is deprecated Please use 'package' instead. 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) both package and public_name field is an error $ cat > dune << EOF @@ -30,6 +32,8 @@ both package and public_name field is an error Please use 'package' instead. 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 "dune", line 3, characters 14-17: 3 | (public_name Foo) ^^^ diff --git a/test/blackbox-tests/test-cases/coq/empty-modules.t/run.t b/test/blackbox-tests/test-cases/coq/empty-modules.t/run.t index 721c30dfcf60..cf3582905b5c 100644 --- a/test/blackbox-tests/test-cases/coq/empty-modules.t/run.t +++ b/test/blackbox-tests/test-cases/coq/empty-modules.t/run.t @@ -11,3 +11,5 @@ Builds fine as expected. $ dune build 2>&1 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) diff --git a/test/blackbox-tests/test-cases/coq/env.t b/test/blackbox-tests/test-cases/coq/env.t index b8de7258433a..6ece7d6daf8e 100644 --- a/test/blackbox-tests/test-cases/coq/env.t +++ b/test/blackbox-tests/test-cases/coq/env.t @@ -48,6 +48,8 @@ Case A / A $ dune build @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) File "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -58,6 +60,8 @@ Case A / A $ dune build @all --profile unsound 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 "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -75,6 +79,8 @@ Case A / I $ dune build @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) File "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -85,6 +91,8 @@ Case A / I $ dune build @all --profile unsound 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 "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -102,6 +110,8 @@ Case A / N $ dune build @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) File "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -112,6 +122,8 @@ Case A / N $ dune build @all --profile unsound 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 "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -129,6 +141,8 @@ Case A / Y $ dune build @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) File "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -139,6 +153,8 @@ Case A / Y $ dune build @all --profile unsound 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) Cases for I @@ -157,6 +173,8 @@ Case I / A $ dune build @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) File "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -167,6 +185,8 @@ Case I / A $ dune build @all --profile unsound 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 "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -184,6 +204,8 @@ Case I / I $ dune build @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) File "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -194,6 +216,8 @@ Case I / I $ dune build @all --profile unsound 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 "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -211,6 +235,8 @@ Case I / N $ dune build @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) File "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -221,6 +247,8 @@ Case I / N $ dune build @all --profile unsound 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 "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -238,6 +266,8 @@ Case I / Y $ dune build @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) File "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -248,6 +278,8 @@ Case I / Y $ dune build @all --profile unsound 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) Cases for N @@ -266,6 +298,8 @@ Case N / A $ dune build @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) File "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -276,6 +310,8 @@ Case N / A $ dune build @all --profile unsound 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 "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -293,6 +329,8 @@ Case N / I $ dune build @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) File "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -303,6 +341,8 @@ Case N / I $ dune build @all --profile unsound 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 "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -320,6 +360,8 @@ Case N / N $ dune build @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) File "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -330,6 +372,8 @@ Case N / N $ dune build @all --profile unsound 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 "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -347,6 +391,8 @@ Case N / Y $ dune build @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) File "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -357,6 +403,8 @@ Case N / Y $ dune build @all --profile unsound 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 "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -380,6 +428,8 @@ Case Y / A $ dune build @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) File "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -390,6 +440,8 @@ Case Y / A $ dune build @all --profile unsound 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) Case Y / I @@ -401,6 +453,8 @@ Case Y / I $ dune build @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) File "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -411,6 +465,8 @@ Case Y / I $ dune build @all --profile unsound 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) Case Y / N @@ -422,6 +478,8 @@ Case Y / N $ dune build @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) File "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -432,6 +490,8 @@ Case Y / N $ dune build @all --profile unsound 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) Case Y / Y @@ -443,6 +503,8 @@ Case Y / Y $ dune build @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) File "./foo.v", line 3, characters 24-25: Error: The term "t" has type "Type" while it is expected to have type @@ -453,3 +515,5 @@ Case Y / Y $ dune build @all --profile unsound 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) diff --git a/test/blackbox-tests/test-cases/coq/extraction/extract.t b/test/blackbox-tests/test-cases/coq/extraction/extract.t index 04c3fe1b5280..7774b74308a6 100644 --- a/test/blackbox-tests/test-cases/coq/extraction/extract.t +++ b/test/blackbox-tests/test-cases/coq/extraction/extract.t @@ -36,6 +36,8 @@ $ dune exec ./foo.exe 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) false $ ls _build/default Datatypes.ml diff --git a/test/blackbox-tests/test-cases/coq/extraction/extraction-patch.t/run.t b/test/blackbox-tests/test-cases/coq/extraction/extraction-patch.t/run.t index 8a05aff80120..9b1b6f4d9d5e 100644 --- a/test/blackbox-tests/test-cases/coq/extraction/extraction-patch.t/run.t +++ b/test/blackbox-tests/test-cases/coq/extraction/extraction-patch.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) $ ls _build/default Datatypes.ml @@ -22,4 +24,6 @@ $ dune exec -- ./my_prog.exe 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) Result: false diff --git a/test/blackbox-tests/test-cases/coq/flags.t b/test/blackbox-tests/test-cases/coq/flags.t index ddf335746b89..b7919ebe0ffe 100644 --- a/test/blackbox-tests/test-cases/coq/flags.t +++ b/test/blackbox-tests/test-cases/coq/flags.t @@ -19,6 +19,8 @@ Test case: default flags $ dune build foo.vo && tail -n 1 _build/log | ./scrub_coq_args.sh 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) coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled @@ -60,6 +62,8 @@ TC: :standard $ dune build foo.vo && tail -n 1 _build/log | ./scrub_coq_args.sh 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) coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled @@ -100,6 +104,8 @@ TC: override :standard $ dune build foo.vo && tail -n 1 _build/log | ./scrub_coq_args.sh 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) coqc -w -deprecated-native-compiler-option -w -native-compiler-disabled @@ -140,6 +146,8 @@ TC: add to :standard $ dune build foo.vo && tail -n 1 _build/log | ./scrub_coq_args.sh 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) coqc -q -type-in-type -w -deprecated-native-compiler-option -w -native-compiler-disabled @@ -185,6 +193,8 @@ TC: extend in workspace + override standard $ dune build foo.vo && tail -n 1 _build/log | ./scrub_coq_args.sh 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) coqc -type-in-type -w -deprecated-native-compiler-option -w -native-compiler-disabled @@ -224,6 +234,8 @@ TC: extend in workspace + override standard $ dune build foo.vo && tail -n 1 _build/log | ./scrub_coq_args.sh 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) coqc -q -type-in-type -w -deprecated-native-compiler-option -w -native-compiler-disabled @@ -265,6 +277,8 @@ TC: extend in dune (env) + override standard $ dune build foo.vo && tail -n 1 _build/log | ./scrub_coq_args.sh 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) coqc -type-in-type -w -deprecated-native-compiler-option -w -native-compiler-disabled @@ -306,6 +320,8 @@ TC: extend in dune (env) + standard $ dune build foo.vo && tail -n 1 _build/log | ./scrub_coq_args.sh 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) coqc -q -type-in-type -type-in-type -w -deprecated-native-compiler-option -w -native-compiler-disabled @@ -352,6 +368,8 @@ TC: extend in dune (env) + workspace + standard $ dune build foo.vo && tail -n 1 _build/log | ./scrub_coq_args.sh 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) coqc -q -type-in-type -bt -w -deprecated-native-compiler-option -w -native-compiler-disabled diff --git a/test/blackbox-tests/test-cases/coq/github5532.t b/test/blackbox-tests/test-cases/coq/github5532.t index 9ffbf7297846..fb6fb07e354b 100644 --- a/test/blackbox-tests/test-cases/coq/github5532.t +++ b/test/blackbox-tests/test-cases/coq/github5532.t @@ -18,6 +18,8 @@ Reproducing test case for #5532. $ 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 "dune", line 1, characters 0-26: 1 | (coq.theory 2 | (name basic)) diff --git a/test/blackbox-tests/test-cases/coq/lang_08_warning_disable/run.t b/test/blackbox-tests/test-cases/coq/lang_08_warning_disable/run.t new file mode 100644 index 000000000000..4ce0b129ef59 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/lang_08_warning_disable/run.t @@ -0,0 +1,37 @@ +Test that the warning for coq lang 0.8 can be disabled + + $ cat > dune-project < (lang dune 3.12) + > (using coq 0.7) + > EOF + + $ cat > dune < (coq.theory + > (name Foo)) + > EOF + + $ cat > a.v < Definition a := Type. + > EOF + + $ 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 get the warning again, even on a zero-build: + + $ 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) + + $ cat > dune-project < (lang dune 3.12) + > (using coq 0.7) + > (warnings (deprecated_coq_lang_lt_08 disabled)) + > EOF + + $ dune build diff --git a/test/blackbox-tests/test-cases/coq/ml-lib.t/run.t b/test/blackbox-tests/test-cases/coq/ml-lib.t/run.t index 25d561eb4761..81dab774520e 100644 --- a/test/blackbox-tests/test-cases/coq/ml-lib.t/run.t +++ b/test/blackbox-tests/test-cases/coq/ml-lib.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/native-compose.t/run.t b/test/blackbox-tests/test-cases/coq/native-compose.t/run.t index 8a4c5d6bc5dc..5abe151e7ae0 100644 --- a/test/blackbox-tests/test-cases/coq/native-compose.t/run.t +++ b/test/blackbox-tests/test-cases/coq/native-compose.t/run.t @@ -1,6 +1,8 @@ $ dune build --profile=release --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) coqdep bar/.bar.theory.d coqdep foo/.foo.theory.d coqc foo/Nfoo_foo.{cmi,cmxs},foo/foo.{glob,vo} @@ -10,6 +12,8 @@ $ dune build --profile=release --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/native-single.t/run.t b/test/blackbox-tests/test-cases/coq/native-single.t/run.t index 09017fb41281..42b9bccfd234 100644 --- a/test/blackbox-tests/test-cases/coq/native-single.t/run.t +++ b/test/blackbox-tests/test-cases/coq/native-single.t/run.t @@ -1,6 +1,8 @@ $ dune build --profile=release --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) coqdep .basic.theory.d coqc Nbasic_foo.{cmi,cmxs},foo.{glob,vo} coqc Nbasic_bar.{cmi,cmxs},bar.{glob,vo} @@ -8,6 +10,8 @@ $ dune build --profile=release --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/no-stdlib.t/run.t b/test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t index 382f1c2152a3..d620356a3ae8 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 @@ -4,6 +4,8 @@ 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. + 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 *** 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) @@ -16,6 +18,8 @@ and the prelude is not imported; we expect the below two tests to fail. $ dune build --display=short bar.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. + Hint: To disable this warning, add the following to your dune-project file + (warnings ...) section: (deprecated_coq_lang_lt_08 disabled) coqc bar.{glob,vo} (exit 1) File "./bar.v", line 1, characters 20-23: Error: The reference nat was not found in the current environment. diff --git a/test/blackbox-tests/test-cases/coq/plugin-meta.t/run.t b/test/blackbox-tests/test-cases/coq/plugin-meta.t/run.t index 49e681c42c87..d86fc6ee6e16 100644 --- a/test/blackbox-tests/test-cases/coq/plugin-meta.t/run.t +++ b/test/blackbox-tests/test-cases/coq/plugin-meta.t/run.t @@ -12,6 +12,8 @@ The META file for plugins is built before calling coqdep $ dune build .bar.theory.d 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) $ ls _build/install/default/lib/bar META diff --git a/test/blackbox-tests/test-cases/coq/plugin-private.t/run.t b/test/blackbox-tests/test-cases/coq/plugin-private.t/run.t index 046ac0419db5..d09cc679a994 100644 --- a/test/blackbox-tests/test-cases/coq/plugin-private.t/run.t +++ b/test/blackbox-tests/test-cases/coq/plugin-private.t/run.t @@ -11,6 +11,8 @@ In Coq >= 0.6, depending on a private library as a plugin is an error. $ 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 "dune", line 6, characters 10-13: 6 | (plugins foo)) ^^^ diff --git a/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t b/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t index 61e8ec4a8c92..a1bd88bd3fd9 100644 --- a/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t +++ b/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t @@ -1,6 +1,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) File "public/dune", line 4, characters 11-18: 4 | (theories private)) ^^^^^^^ diff --git a/test/blackbox-tests/test-cases/coq/rec-module.t/run.t b/test/blackbox-tests/test-cases/coq/rec-module.t/run.t index 5b34c25e9dd3..eb56979dffbe 100644 --- a/test/blackbox-tests/test-cases/coq/rec-module.t/run.t +++ b/test/blackbox-tests/test-cases/coq/rec-module.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) coqdep .rec_module.theory.d coqc b/foo.{glob,vo} coqc c/ooo.{glob,vo} @@ -10,6 +12,8 @@ $ 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/rec/META" "_build/install/default/lib/rec/dune-package" diff --git a/test/blackbox-tests/test-cases/coq/theory-stanza-duplicate-module.t/run.t b/test/blackbox-tests/test-cases/coq/theory-stanza-duplicate-module.t/run.t index 85a1a2925156..9535c63e224b 100644 --- a/test/blackbox-tests/test-cases/coq/theory-stanza-duplicate-module.t/run.t +++ b/test/blackbox-tests/test-cases/coq/theory-stanza-duplicate-module.t/run.t @@ -9,6 +9,8 @@ Dune should warn about duplicate modules declared inside a coq.theory stanza $ 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 "dune", line 1, characters 0-47: 1 | (coq.theory 2 | (name foo)