From 0a2db0269809539ccc66f8ec73637c37fbd23580 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 17 Apr 2020 17:56:23 +0200 Subject: Support for coq 8.11.1. Update configure script. --- configure | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'configure') diff --git a/configure b/configure index 6bd7ed0e..ee0108ae 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.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.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.11.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.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" + echo "Error: CompCert requires one of the following Coq versions: 8.11.1, 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;; "") -- cgit From 5e29f8b5ba9582ecf2a1d0baeaef195873640607 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 8 Jun 2020 12:33:52 +0200 Subject: Compatibility with coq 8.11.2 Updated configure script to also allow coq version 8.11.2 --- configure | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'configure') diff --git a/configure b/configure index ee0108ae..d5264654 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.11.0|8.11.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|8.11.0|8.11.1|8.11.2) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" -- cgit From 5b8578daeed73483b130618c954abb24afa8ddb9 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 21 Jun 2020 19:19:49 +0200 Subject: Preliminary support for Coq 8.12 Based on testing with beta-1 release. The deprecation warning about the "omega" tactic is ignored while we decide when to switch to "lia" instead. --- configure | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'configure') diff --git a/configure b/configure index d5264654..b358f3cb 100755 --- a/configure +++ b/configure @@ -530,19 +530,19 @@ 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.11.1|8.11.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|8.11.1|8.11.2|8.12.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.11.1, 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" + echo "Error: CompCert requires a version of Coq between 8.8.0 and 8.12.0" missingtools=true fi;; "") echo "NOT FOUND" - echo "Error: make sure Coq version 8.9.1 is installed." + echo "Error: make sure Coq version 8.11.2 is installed." missingtools=true;; esac -- cgit From 3b1f3dd57d8c10c1c29f67f0f745e3263d9d3daf Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 7 Jul 2020 14:07:37 +0200 Subject: Revised detection of menhirLib directory (#248) Use `ocamlfind query menhirLib` in preference to `menhir --suggest-menhirLib`. Fixes: #363 --- configure | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'configure') diff --git a/configure b/configure index b358f3cb..432bacff 100755 --- a/configure +++ b/configure @@ -582,8 +582,12 @@ 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_dir=$(menhir --suggest-menhirLib | tr -d '\r' | tr '\\' '/') - if test -z "$menhir_dir"; then + menhir_dir=$(ocamlfind query menhirLib 2>/dev/null \ + | tr -d '\r' | tr '\\' '/') || \ + menhir_dir=$(menhir --suggest-menhirLib \ + | tr -d '\r' | tr '\\' '/') || \ + menhir_dir="" + if test ! -d "$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." -- cgit From 9af28924713d14d833dcaf95cd3338ef68fbfc97 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 7 Jul 2020 14:08:24 +0200 Subject: Bytecode-only build (#243) If ocamlopt (the native-code OCaml compiler) is not available, fall back to building with ocamlc (the bytecode OCaml compiler). Fixes: #359 --- configure | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) (limited to 'configure') diff --git a/configure b/configure index 432bacff..d38deeec 100755 --- a/configure +++ b/configure @@ -547,7 +547,7 @@ case "$coq_ver" in esac echo "Testing OCaml... " | tr -d '\n' -ocaml_ver=`ocamlopt -version 2>/dev/null` +ocaml_ver=`ocamlc -version 2>/dev/null` case "$ocaml_ver" in 4.00.*|4.01.*| 4.02.*|4.03.*|4.04.*) echo "version $ocaml_ver -- UNSUPPORTED" @@ -565,9 +565,19 @@ case "$ocaml_ver" in missingtools=true;; esac +echo "Testing OCaml native-code compiler..." | tr -d '\n' +ocamlopt_ver=`ocamlopt -version 2>/dev/null` +if test "$ocamlopt_ver" = "$ocaml_ver"; then + echo "yes" + ocaml_native_comp=true +else + echo "no, will build to bytecode only" + ocaml_native_comp=false +fi + echo "Testing OCaml .opt compilers... " | tr -d '\n' -ocaml_opt_ver=`ocamlopt.opt -version 2>/dev/null` -if test "$ocaml_opt_ver" = "$ocaml_ver"; then +ocamlopt_opt_ver=`ocamlopt.opt -version 2>/dev/null` +if test "$ocamlopt_opt_ver" = "$ocaml_ver"; then echo "yes" ocaml_opt_comp=true else @@ -680,6 +690,7 @@ LIBDIR=$libdir MANDIR=$sharedir/man SHAREDIR=$sharedir COQDEVDIR=$coqdevdir +OCAML_NATIVE_COMP=$ocaml_native_comp OCAML_OPT_COMP=$ocaml_opt_comp MENHIR_DIR=$menhir_dir COMPFLAGS=-bin-annot -- cgit From 13e0566dbdd8bf845d7c2a65ffefaaf460381e70 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 15 Jul 2020 09:49:40 +0200 Subject: Revised detection of menhirLib directory, continued (#365) This is a follow-up to commit 3b1f3dd5, which was wrong in that errors in a shell pipeline were not correctly detected. Fixes: #363 --- configure | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'configure') diff --git a/configure b/configure index d38deeec..0919f34e 100755 --- a/configure +++ b/configure @@ -592,11 +592,10 @@ 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_dir=$(ocamlfind query menhirLib 2>/dev/null \ - | tr -d '\r' | tr '\\' '/') || \ - menhir_dir=$(menhir --suggest-menhirLib \ - | tr -d '\r' | tr '\\' '/') || \ + menhir_dir=$(ocamlfind query menhirLib 2>/dev/null) || \ + menhir_dir=$(menhir --suggest-menhirLib) || \ menhir_dir="" + menhir_dir=$(echo "$menhir_dir" | tr -d '\r' | tr '\\' '/') if test ! -d "$menhir_dir"; then echo "Error: cannot determine the location of the Menhir API library." echo "This can be due to an incorrect Menhir package." @@ -852,6 +851,7 @@ CompCert configuration: Linker needs '-no-pie'........ $clinker_needs_no_pie Math library.................. $libmath Build command to use.......... $make + Menhir API library............ $menhir_dir Binaries installed in......... $bindirexp Runtime library provided...... $has_runtime_lib Library files installed in.... $libdirexp -- cgit From 338509aef7347fda5db4123d645bb52971fa8a91 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 29 Jul 2020 12:16:03 +0200 Subject: Remove support for x86-32 under macOS 32-bit executables cannot be built since XCode 10.0 (sep 2018). 32-bit executables cannot be executed since MacOS 10.15 (oct 2019). Better remove x86-32 support and fail at configuration time instead of at the end of the build. --- configure | 24 ------------------------ 1 file changed, 24 deletions(-) (limited to 'configure') diff --git a/configure b/configure index 0919f34e..a02e561f 100755 --- a/configure +++ b/configure @@ -48,7 +48,6 @@ Supported targets: armeb-hardfloat (ARM, EABI using hardware FP registers, big endian) x86_32-linux (x86 32 bits, Linux) x86_32-bsd (x86 32 bits, BSD) - x86_32-macosx (x86 32 bits, MacOS X) x86_32-cygwin (x86 32 bits, Cygwin environment under Windows) x86_64-linux (x86 64 bits, Linux) x86_64-bsd (x86 64 bits, BSD) @@ -328,29 +327,6 @@ if test "$arch" = "x86" -a "$bitsize" = "32"; then libmath="-lm" system="linux" ;; - macosx) - # kernel major versions count upwards from 4 for OSX 10.0 to 15 for OSX 10.11 - kernel_major=`uname -r | cut -d "." -f 1` - - abi="macosx" - casm="${toolprefix}gcc" - casm_options="-arch i386 -c" - cc="${toolprefix}gcc -arch i386" - clinker="${toolprefix}gcc" - clinker_needs_no_pie=false - cprepro="${toolprefix}gcc" - cprepro_options="-std=c99 -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -E" - libmath="" - system="macosx" - - if [[ $kernel_major -gt 11 ]]; then - # OSX >= 10.8 - clinker_options="-arch i386 -Wl,-no_pie" - else - # OSX <= 10.7 - clinker_options="-arch i386" - fi - ;; *) echo "Error: invalid eabi/system '$target' for architecture IA32/X86_32." 1>&2 echo "$usage" 1>&2 -- cgit From ab0d9476db875a82cf293623d18552b62f239d5c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 21 Sep 2020 14:15:57 +0200 Subject: Support the use of already-installed MenhirLib and Flocq libraries configure flags -use-external-Flocq and -use external-MenhirLib. --- configure | 86 ++++++++++++++++++++++++++++++++------------------------------- 1 file changed, 44 insertions(+), 42 deletions(-) (limited to 'configure') diff --git a/configure b/configure index a02e561f..a71901b8 100755 --- a/configure +++ b/configure @@ -27,6 +27,8 @@ clightgen=false install_coqdev=false responsefile="gnu" ignore_coq_version=false +library_Flocq=local +library_MenhirLib=local usage='Usage: ./configure [options] target For help on options and targets, do: ./configure -help @@ -84,6 +86,8 @@ Options: -libdir Install libraries in -coqdevdir Install Coq development (.vo files) in -toolprefix Prefix names of tools ("gcc", etc) with + -use-external-Flocq Use an already-installed Flocq library + -use-external-MenhirLib Use an already-installed MenhirLib library -no-runtime-lib Do not compile nor install the runtime support library -no-standard-headers Do not install nor use the standard .h headers -clightgen Also compile and install the clightgen tool @@ -124,6 +128,10 @@ while : ; do ignore_coq_version=true;; -install-coqdev|--install-coqdev|-install-coq-dev|--install-coq-dev) install_coqdev=true;; + -use-external-Flocq|--use-external-Flocq) + library_Flocq=external;; + -use-external-MenhirLib|--use-external-MenhirLib) + library_MenhirLib=external;; -help|--help) echo "$help"; exit 0;; -*) @@ -611,47 +619,6 @@ if $missingtools; then exit 2 fi -cat > .merlin < _CoqProject -case $arch in - x86) - echo "-R x86_${bitsize} compcert.x86_${bitsize}" >> _CoqProject - ;; -esac - # # Generate Makefile.config # @@ -694,6 +661,8 @@ LIBMATH=$libmath MODEL=$model SYSTEM=$system RESPONSEFILE=$responsefile +LIBRARY_FLOCQ=$library_Flocq +LIBRARY_MENHIRLIB=$library_MenhirLib EOF else cat >> Makefile.config <<'EOF' @@ -787,9 +756,41 @@ CLIGHTGEN=false # Whether the other tools support responsefiles in gnu syntax RESPONSEFILE="none" +# Whether to use the local copies of Flocq and MenhirLib +LIBRARY_FLOCQ=local # external +LIBRARY_MENHIRLIB=local # external EOF fi +# +# Generate Merlin and CoqProject files to simplify development +# +cat > .merlin < Date: Mon, 5 Oct 2020 15:52:58 +0200 Subject: Support Cygwin 64 bits - Add support for the Win64 ABI to the x86_64 port - Update vararg support to handle Win64 conventions - Configure support for x86_64-cygwin64 --- configure | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'configure') diff --git a/configure b/configure index a71901b8..fcdbe803 100755 --- a/configure +++ b/configure @@ -54,6 +54,7 @@ Supported targets: x86_64-linux (x86 64 bits, Linux) x86_64-bsd (x86 64 bits, BSD) x86_64-macosx (x86 64 bits, MacOS X) + x86_64-cygwin (x86 64 bits, Cygwin environment under Windows) rv32-linux (RISC-V 32 bits, Linux) rv64-linux (RISC-V 64 bits, Linux) aarch64-linux (AArch64, i.e. ARMv8 in 64-bit mode, Linux) @@ -387,6 +388,18 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then libmath="" system="macosx" ;; + cygwin) + abi="standard" + casm="${toolprefix}gcc" + casm_options="-m64 -c" + cc="${toolprefix}gcc -m64" + clinker="${toolprefix}gcc" + clinker_options="-m64" + cprepro="${toolprefix}gcc" + cprepro_options="-std=c99 -m64 -U__GNUC__ '-D__attribute__(x)=' -E" + libmath="-lm" + system="cygwin" + ;; *) echo "Error: invalid eabi/system '$target' for architecture X86_64." 1>&2 echo "$usage" 1>&2 -- cgit From e87f24575e79e7866b132f0a970cf6f82d115b88 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 14 Nov 2020 09:49:28 +0100 Subject: Support Coq 8.12.1 --- configure | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'configure') diff --git a/configure b/configure index fcdbe803..1620ad4b 100755 --- a/configure +++ b/configure @@ -527,14 +527,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.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.11.1|8.11.2|8.12.0) + 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.11.1|8.11.2|8.12.0|8.12.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 a version of Coq between 8.8.0 and 8.12.0" + echo "Error: CompCert requires a version of Coq between 8.8.0 and 8.12.1" missingtools=true fi;; "") -- cgit From 5b5682a4d4ebb102002616015adab46154597b10 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 16 Dec 2020 15:52:48 +0100 Subject: upgrade kvx backend to coq.8.12.2 --- configure | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'configure') diff --git a/configure b/configure index 415dbb03..e63ff928 100755 --- a/configure +++ b/configure @@ -565,7 +565,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.11.1|8.11.2|8.12.0|8.12.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|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" -- cgit