From e3f2f81e6ad70c082dbf3dc5f938e8474c46657d Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Sun, 13 Oct 2019 21:05:56 +0200 Subject: Fix configure for coq 8.10.0 --- configure | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'configure') diff --git a/configure b/configure index dccf6d14..bf4172f9 100755 --- a/configure +++ b/configure @@ -530,14 +530,14 @@ missingtools=false echo "Testing Coq... " | tr -d '\n' coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') case "$coq_ver" in - 8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10) + 8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" if $ignore_coq_version; then echo "Warning: this version of Coq is unsupported, proceed at your own risks." else - echo "Error: CompCert requires one of the following Coq versions: 8.10, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0" + echo "Error: CompCert requires one of the following Coq versions: 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0" missingtools=true fi;; "") -- cgit From 1c1a4d86a22dd04fc92e61d4bd5c35e047c8b772 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 28 Oct 2019 16:22:53 +0100 Subject: Add support for Coq 8.10.1 --- configure | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'configure') diff --git a/configure b/configure index bf4172f9..cb2747be 100755 --- a/configure +++ b/configure @@ -530,14 +530,14 @@ missingtools=false echo "Testing Coq... " | tr -d '\n' coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') case "$coq_ver" in - 8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0) + 8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" if $ignore_coq_version; then echo "Warning: this version of Coq is unsupported, proceed at your own risks." else - echo "Error: CompCert requires one of the following Coq versions: 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0" + echo "Error: CompCert requires one of the following Coq versions: 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0" missingtools=true fi;; "") -- cgit From 029329c8adc955d9ebe9030074cce0df9dcfa5f7 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 31 Oct 2019 11:49:42 +0100 Subject: Raise minimal required versions for OCaml and Coq (#203) At least OCaml 4.05 is now required as well as Coq 8.8. --- configure | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) (limited to 'configure') diff --git a/configure b/configure index cb2747be..8604a1d9 100755 --- a/configure +++ b/configure @@ -530,14 +530,14 @@ missingtools=false echo "Testing Coq... " | tr -d '\n' coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') case "$coq_ver" in - 8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1) + 8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" if $ignore_coq_version; then echo "Warning: this version of Coq is unsupported, proceed at your own risks." else - echo "Error: CompCert requires one of the following Coq versions: 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0" + echo "Error: CompCert requires one of the following Coq versions: 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0" missingtools=true fi;; "") @@ -549,15 +549,10 @@ esac echo "Testing OCaml... " | tr -d '\n' ocaml_ver=`ocamlopt -version 2>/dev/null` case "$ocaml_ver" in - 4.00.*|4.01.*) + 4.00.*|4.01.*| 4.02.*|4.03.*|4.04.*) echo "version $ocaml_ver -- UNSUPPORTED" - echo "Error: CompCert requires OCaml version 4.02 or later." + echo "Error: CompCert requires OCaml version 4.05 or later." missingtools=true;; - 4.02.*|4.03.*|4.04.*) - echo "version $ocaml_ver -- good!" - echo "WARNING: some Intel processors of the Skylake and Kaby Lake generations" - echo "have a hardware bug that can be triggered by this version of OCaml." - echo "To avoid this risk, it is recommended to use OCaml 4.05 or later.";; 4.0*) echo "version $ocaml_ver -- good!";; ?.*) -- cgit From ec49c7b8bd4502c380b88c78baa674000db109fd Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 3 Dec 2019 13:01:51 +0100 Subject: Allow Coq 8.10.2. --- configure | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'configure') diff --git a/configure b/configure index 8604a1d9..b964c124 100755 --- a/configure +++ b/configure @@ -530,7 +530,7 @@ missingtools=false echo "Testing Coq... " | tr -d '\n' coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') case "$coq_ver" in - 8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1) + 8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" -- cgit From aa042a1654698d7bfd1e3cd8cf7abacd528e7133 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 3 Feb 2020 17:45:02 +0100 Subject: Using k1-elf-as instead of k1-cos-gcc for assembling --- configure | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'configure') diff --git a/configure b/configure index b8555973..716e5e81 100755 --- a/configure +++ b/configure @@ -457,8 +457,8 @@ if test "$arch" = "mppa_k1c"; then fi osupper=`echo $os|tr a-z A-Z` k1base="k1-$os" - casm="$k1base-gcc" - casm_options="$model_options -c" + casm="k1-elf-as" + casm_options="$model_options" cc="$k1base-gcc $model_options" clinker="$k1base-gcc" bindir="$HOME/.usr/bin" -- cgit From b0fdbb0e88d6decd068709ea673dbe51fd6727b0 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 5 Feb 2020 18:33:13 +0100 Subject: Support Coq 8.11.0 (#212) Update configure. Ignore and clean up .vok and .vos files, which Coq 8.11.0 generates. --- configure | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'configure') diff --git a/configure b/configure index b964c124..d91bfebf 100755 --- a/configure +++ b/configure @@ -530,7 +530,7 @@ missingtools=false echo "Testing Coq... " | tr -d '\n' coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') case "$coq_ver" in - 8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2) + 8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" -- cgit From 6950ac8fb096768cb3811ae7f89d0db080bf965a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 5 Feb 2020 18:36:08 +0100 Subject: Revised menhirLib autoconfiguration (#331) Since Menhir version 20200123, we need to link with menhirLib.cmxa instead of menhirLib.cmx. This commit chooses automatically the file to link with: menhirLib.cmxa if it exists in the menhirLib installation directory, menhirLib.cmx otherwise. To reliably find the installation directory, configure was changed to record the menhirLib directory in Makefile.config, variable MENHIR_DIR, instead of a pre-cooked command-line option MENHIR_INCLUDES. Makefile.extr was adapted accordingly. Fixes: #329 Closes: #330 --- configure | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'configure') diff --git a/configure b/configure index d91bfebf..a8efb551 100755 --- a/configure +++ b/configure @@ -582,8 +582,8 @@ case "$menhir_ver" in 20[0-9][0-9][0-9][0-9][0-9][0-9]) if test "$menhir_ver" -ge $MENHIR_REQUIRED; then echo "version $menhir_ver -- good!" - menhir_include_dir=$(menhir --suggest-menhirLib | tr -d '\r' | tr '\\' '/') - if test -z "$menhir_include_dir"; then + menhir_dir=$(menhir --suggest-menhirLib | tr -d '\r' | tr '\\' '/') + if test -z "$menhir_dir"; then echo "Error: cannot determine the location of the Menhir API library." echo "This can be due to an incorrect Menhir package." echo "Consider using the OPAM package for Menhir." @@ -677,7 +677,7 @@ MANDIR=$sharedir/man SHAREDIR=$sharedir COQDEVDIR=$coqdevdir OCAML_OPT_COMP=$ocaml_opt_comp -MENHIR_INCLUDES=-I "$menhir_include_dir" +MENHIR_DIR=$menhir_dir COMPFLAGS=-bin-annot EOF -- cgit From d5435a34169d92a96f1436128f3e90df7f4f9e9a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 6 Feb 2020 17:27:05 +0100 Subject: Compatibility with OCaml 4.10 (#214) debug/DwarfPrinter.mli: unused functor parameter trigger warning 69, replace by non-dependent functor type. Makefile.extr: turn warning 69 (unused functor parameter) off for extracted code configure: accept OCaml versions above 4.09 configure: update messages for unsupported versions of OCaml and Coq --- configure | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'configure') diff --git a/configure b/configure index a8efb551..6bd7ed0e 100755 --- a/configure +++ b/configure @@ -537,7 +537,7 @@ case "$coq_ver" in if $ignore_coq_version; then echo "Warning: this version of Coq is unsupported, proceed at your own risks." else - echo "Error: CompCert requires one of the following Coq versions: 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0" + echo "Error: CompCert requires one of the following Coq versions: 8.11.0, 8.10.2, 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0" missingtools=true fi;; "") @@ -553,15 +553,15 @@ case "$ocaml_ver" in echo "version $ocaml_ver -- UNSUPPORTED" echo "Error: CompCert requires OCaml version 4.05 or later." missingtools=true;; - 4.0*) + 4.*) echo "version $ocaml_ver -- good!";; ?.*) echo "version $ocaml_ver -- UNSUPPORTED" - echo "Error: CompCert requires OCaml version 4.02 or later." + echo "Error: CompCert requires OCaml version 4.05 or later." missingtools=true;; *) echo "NOT FOUND" - echo "Error: make sure OCaml version 4.02 or later is installed." + echo "Error: make sure OCaml version 4.05 or later is installed." missingtools=true;; esac -- cgit From b748b38c8b3a998f018477d7375ae16997318769 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 10 Feb 2020 18:30:07 +0100 Subject: Removing from Asmblockgenproof0 architecture specific definitions --- configure | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'configure') diff --git a/configure b/configure index 9d5bfcf9..f13d1af3 100755 --- a/configure +++ b/configure @@ -845,7 +845,7 @@ EXECUTE=k1-cluster --syscall=libstd_scalls.so -- CFLAGS= -D __K1C_COS__ SIMU=k1-cluster -- BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\ - Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v\\ + Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\ AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\ -- cgit From c974b25682251da237dbbe8ef3af218c6d175ae2 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 1 Apr 2020 10:34:57 +0200 Subject: Removing 8.8.* versions of coq in configure --- configure | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'configure') diff --git a/configure b/configure index f13d1af3..f790281c 100755 --- a/configure +++ b/configure @@ -568,7 +568,7 @@ missingtools=false echo "Testing Coq... " | tr -d '\n' coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') case "$coq_ver" in - 8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0) + 8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" -- cgit