From d4513f41c54869c9b4ba96ab79d50933a1d5c25a Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 28 Dec 2020 15:53:36 +0100 Subject: Update Flocq to 3.4.0 (#383) --- Makefile | 1 + 1 file changed, 1 insertion(+) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 4b0b5761..73f8f172 100644 --- a/Makefile +++ b/Makefile @@ -57,6 +57,7 @@ GPATH=$(DIRS) ifeq ($(LIBRARY_FLOCQ),local) FLOCQ=\ + SpecFloatCompat.v \ Raux.v Zaux.v Defs.v Digits.v Float_prop.v FIX.v FLT.v FLX.v FTZ.v \ Generic_fmt.v Round_pred.v Round_NE.v Ulp.v Core.v \ Bracket.v Div.v Operations.v Round.v Sqrt.v \ -- cgit From aba0e740f25ffa5c338dfa76cab71144802cebc2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 21 Jun 2020 18:22:00 +0200 Subject: Replace `omega` tactic with `lia` Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 73f8f172..971b1394 100644 --- a/Makefile +++ b/Makefile @@ -41,7 +41,7 @@ DIRS += MenhirLib COQINCLUDES += -R MenhirLib MenhirLib endif -COQCOPTS ?= -w -undeclared-scope -w -omega-is-deprecated +COQCOPTS ?= -w -undeclared-scope COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) COQDOC="$(COQBIN)coqdoc" -- cgit From 25483cf1acce8695a438f4f2164b09fb1ecd9d2e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 21 Jan 2021 16:54:40 +0100 Subject: Silence some new warnings of Coq 8.13 Either because the code change that would silence the warning is not desirable, or because it would break compatibility with earlier versions of Coq. Explain the silenced warnings as comments in the Makefile. --- Makefile | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 971b1394..d0b0029a 100644 --- a/Makefile +++ b/Makefile @@ -41,7 +41,23 @@ DIRS += MenhirLib COQINCLUDES += -R MenhirLib MenhirLib endif -COQCOPTS ?= -w -undeclared-scope +# Notes on silenced Coq warnings: +# +# undeclared-scope: +# warning introduced in 8.12 +# suggested change (use `Declare Scope`) supported since 8.12 +# unused-pattern-matching-variable: +# warning introduced in 8.13 +# the code rewrite that avoids the warning is not desirable +# deprecated-ident-entry: +# warning introduced in 8.13 +# suggested change (use `name` instead of `ident`) supported since 8.13 + +COQCOPTS ?= \ + -w -undeclared-scope \ + -w -unused-pattern-matching-variable \ + -w -deprecated-ident-entry + COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) COQDOC="$(COQBIN)coqdoc" -- cgit From 5a632954c85e8b2b5afea124e4fc83f39c5d3598 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 1 Jun 2021 14:37:07 +0200 Subject: [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend/C2C.ml --- Makefile | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 25cb82e6..92cd37eb 100644 --- a/Makefile +++ b/Makefile @@ -6,10 +6,11 @@ # # # Copyright Institut National de Recherche en Informatique et en # # Automatique. All rights reserved. This file is distributed # -# under the terms of the GNU General Public License as published by # -# the Free Software Foundation, either version 2 of the License, or # -# (at your option) any later version. This file is also distributed # -# under the terms of the INRIA Non-Commercial License Agreement. # +# under the terms of the GNU Lesser General Public License as # +# published by the Free Software Foundation, either version 2.1 of # +# the License, or (at your option) any later version. # +# This file is also distributed under the terms of the # +# INRIA Non-Commercial License Agreement. # # # ####################################################################### -- cgit