From 6da277cf402055e1fe7d0eef01e3d682d3fc4f4d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 26 Nov 2024 11:02:58 +0100 Subject: [PATCH] Use `-deprecated-since-N.NN` warning options For finer control of deprecation warnings. --- Makefile | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/Makefile b/Makefile index 58b623581..20947e842 100644 --- a/Makefile +++ b/Makefile @@ -57,13 +57,25 @@ endif # deprecated-instance-without-locality: # warning introduced in 8.14 # triggered by Menhir-generated files, to be solved upstream in Menhir +# deprecated-since-8.19 +# deprecated-since-8.20 +# renamings performed in Coq's standard library; +# using the new names would break compatibility with earlier Coq versions. COQCOPTS ?= \ - -w -unused-pattern-matching-variable + -w -unused-pattern-matching-variable \ + -w -deprecated-since-8.19 \ + -w -deprecated-since-8.20 cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality MenhirLib/Interpreter.vo: COQCOPTS += -w -undeclared-scope +# Flocq and Menhirlib run into other renaming issues. +# These warnings can only be addressed upstream. + +flocq/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition +MenhirLib/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition + ifneq ($(INSTALL_COQDEV),true) # Disable costly generation of .cmx files, which are not used locally COQCOPTS += -w -deprecated-native-compiler-option -native-compiler no @@ -219,12 +231,6 @@ endif proof: $(FILES:.v=.vo) -# Turn off some warnings for Flocq and Menhirlib -# These warnings can only be addressed upstream - -flocq/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition -MenhirLib/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition - extraction: extraction/STAMP extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMachdep.v