From ca2ebae012d6cdcc19d0a01f54f3dad614de8e68 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 24 Dec 2020 16:28:01 +0100 Subject: Configure the correct archiver to build runtime/libcompcert.a - Use `${toolprefix}ar` instead of `ar` so as to match the choice of C compiler (as proposed by Michael Soegtrop in PR #380) - Use the Diab archiver `dar` if configured for powerpc-eabi-diab Closes: #380 --- configure | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'configure') diff --git a/configure b/configure index 1620ad4b..a4b257fc 100755 --- a/configure +++ b/configure @@ -211,7 +211,7 @@ casmruntime="" clinker_needs_no_pie=true clinker_options="" cprepro_options="" - +archiver="${toolprefix}ar rcs" # # ARM Target Configuration @@ -275,6 +275,7 @@ if test "$arch" = "powerpc"; then clinker="${toolprefix}dcc" cprepro="${toolprefix}dcc" cprepro_options="-E -D__GNUC__" + archiver="${toolprefix}dar -q" libmath="-lm" system="diab" responsefile="diab" @@ -666,6 +667,7 @@ CLINKER=$clinker CLINKER_OPTIONS=$clinker_options CPREPRO=$cprepro CPREPRO_OPTIONS=$cprepro_options +ARCHIVER=$archiver ENDIANNESS=$endianness HAS_RUNTIME_LIB=$has_runtime_lib HAS_STANDARD_HEADERS=$has_standard_headers @@ -750,6 +752,9 @@ CASMRUNTIME=gcc -c # Linker CLINKER=gcc +# Archiver to build .a libraries +ARCHIVER=ar rcs + # Math library. Set to empty under MacOS X LIBMATH=-lm @@ -839,6 +844,7 @@ CompCert configuration: Assembler for runtime lib..... $casmruntime Linker........................ $clinker Linker needs '-no-pie'........ $clinker_needs_no_pie + Archiver...................... $archiver Math library.................. $libmath Build command to use.......... $make Menhir API library............ $menhir_dir -- cgit From 06956421b4307054af221c118c5f59593c0e67b9 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 24 Dec 2020 16:59:04 +0100 Subject: configure: support Coq 8.12.2 --- configure | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'configure') diff --git a/configure b/configure index a4b257fc..67fb175e 100755 --- a/configure +++ b/configure @@ -528,14 +528,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.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" 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.1" + echo "Error: CompCert requires a version of Coq between 8.8.0 and 8.12.2" missingtools=true fi;; "") -- cgit From 2a9a34bc137b1ba81ab4f6e90a447ae9d64e344b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 24 Dec 2020 16:29:39 +0100 Subject: configure script revised and simplified Start from reasonable defaults before updating them per-target. Print more details in the final configuration summary. Update the "manual" mode. --- configure | 126 +++++++++++++++++++++----------------------------------------- 1 file changed, 43 insertions(+), 83 deletions(-) (limited to 'configure') diff --git a/configure b/configure index 67fb175e..c5afabd8 100755 --- a/configure +++ b/configure @@ -25,7 +25,6 @@ has_runtime_lib=true has_standard_headers=true clightgen=false install_coqdev=false -responsefile="gnu" ignore_coq_version=false library_Flocq=local library_MenhirLib=local @@ -205,13 +204,24 @@ target=${target#[a-zA-Z0-9]*-} # Per-target configuration +# We start with reasonable defaults, +# then redefine the required parameters for each target, +# then check for missing parameters and derive values for them. + asm_supports_cfi="" -casm_options="" +cc="${toolprefix}gcc" +cc_options="" +casm="${toolprefix}gcc" +casm_options="-c" casmruntime="" -clinker_needs_no_pie=true +clinker="${toolprefix}gcc" clinker_options="" -cprepro_options="" +clinker_needs_no_pie=true +cprepro="${toolprefix}gcc" +cprepro_options="-E" archiver="${toolprefix}ar rcs" +libmath="-lm" +responsefile="gnu" # # ARM Target Configuration @@ -231,13 +241,7 @@ if test "$arch" = "arm"; then exit 2;; esac - casm="${toolprefix}gcc" - casm_options="-c" - cc="${toolprefix}gcc" - clinker="${toolprefix}gcc" - cprepro="${toolprefix}gcc" cprepro_options="-std=c99 -U__GNUC__ '-D__REDIRECT(name,proto,alias)=name proto' '-D__REDIRECT_NTH(name,proto,alias)=name proto' -E" - libmath="-lm" system="linux" fi @@ -281,14 +285,8 @@ if test "$arch" = "powerpc"; then responsefile="diab" ;; *) - casm="${toolprefix}gcc" - casm_options="-c" casmruntime="${toolprefix}gcc -c -Wa,-mregnames" - cc="${toolprefix}gcc" - clinker="${toolprefix}gcc" - cprepro="${toolprefix}gcc" cprepro_options="-std=c99 -U__GNUC__ -E" - libmath="-lm" system="linux" ;; esac @@ -303,38 +301,26 @@ if test "$arch" = "x86" -a "$bitsize" = "32"; then case "$target" in bsd) abi="standard" - casm="${toolprefix}gcc" + cc_options="-m32" casm_options="-m32 -c" - cc="${toolprefix}gcc -m32" - clinker="${toolprefix}gcc" clinker_options="-m32" - cprepro="${toolprefix}gcc" cprepro_options="-std=c99 -m32 -U__GNUC__ -E" - libmath="-lm" system="bsd" ;; cygwin) abi="standard" - casm="${toolprefix}gcc" + cc_options="-m32" casm_options="-m32 -c" - cc="${toolprefix}gcc -m32" - clinker="${toolprefix}gcc" clinker_options="-m32" - cprepro="${toolprefix}gcc" cprepro_options="-std=c99 -m32 -U__GNUC__ '-D__attribute__(x)=' -E" - libmath="-lm" system="cygwin" ;; linux) abi="standard" - casm="${toolprefix}gcc" + cc_options="-m32" casm_options="-m32 -c" - cc="${toolprefix}gcc -m32" - clinker="${toolprefix}gcc" clinker_options="-m32" - cprepro="${toolprefix}gcc" cprepro_options="-std=c99 -m32 -U__GNUC__ -E" - libmath="-lm" system="linux" ;; *) @@ -352,53 +338,36 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then case "$target" in bsd) abi="standard" - casm="${toolprefix}gcc" + cc_options="-m64" casm_options="-m64 -c" - cc="${toolprefix}gcc -m64" - clinker="${toolprefix}gcc" clinker_options="-m64" - cprepro="${toolprefix}gcc" cprepro_options="-std=c99 -m64 -U__GNUC__ -E" - libmath="-lm" system="bsd" ;; linux) abi="standard" - casm="${toolprefix}gcc" + cc_options="-m64" casm_options="-m64 -c" - cc="${toolprefix}gcc -m64" - clinker="${toolprefix}gcc" clinker_options="-m64" - cprepro="${toolprefix}gcc" cprepro_options="-std=c99 -m64 -U__GNUC__ -E" - 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" + cc_options="-arch x86_64" casm_options="-arch x86_64 -c" - cc="${toolprefix}gcc -arch x86_64" - clinker="${toolprefix}gcc" + clinker_options="-arch x86_64" clinker_needs_no_pie=false - cprepro="${toolprefix}gcc" cprepro_options="-std=c99 -arch x86_64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -E" libmath="" system="macosx" ;; cygwin) abi="standard" - casm="${toolprefix}gcc" + cc_options="-m64" 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" ;; *) @@ -419,14 +388,10 @@ if test "$arch" = "riscV"; then model_options="-march=rv32imafd -mabi=ilp32d" fi abi="standard" - casm="${toolprefix}gcc" + cc_options="$model_options" casm_options="$model_options -c" - cc="${toolprefix}gcc $model_options" - clinker="${toolprefix}gcc" clinker_options="$model_options" - cprepro="${toolprefix}gcc" cprepro_options="$model_options -std=c99 -U__GNUC__ -E" - libmath="-lm" system="linux" fi @@ -437,14 +402,7 @@ if test "$arch" = "aarch64"; then case "$target" in linux) abi="standard" - casm="${toolprefix}gcc" - casm_options="-c" - cc="${toolprefix}gcc" - clinker="${toolprefix}gcc" - clinker_options="" - cprepro="${toolprefix}gcc" cprepro_options="-std=c99 -U__GNUC__ -E" - libmath="-lm" system="linux";; *) echo "Error: invalid eabi/system '$target' for architecture AArch64." 1>&2 @@ -661,7 +619,7 @@ BITSIZE=$bitsize CASM=$casm CASM_OPTIONS=$casm_options CASMRUNTIME=$casmruntime -CC=$cc +CC=$cc $cc_options CLIGHTGEN=$clightgen CLINKER=$clinker CLINKER_OPTIONS=$clinker_options @@ -737,25 +695,28 @@ ENDIANNESS= # SYSTEM=cygwin SYSTEM= -# C compiler for compiling runtime library files and some tests -CC=gcc +# C compiler (for testing only) +CC=cc -# Preprocessor for .c files -CPREPRO=gcc -U__GNUC__ -E - -# Assembler for assembling .s files -CASM=gcc -c +# Assembler for assembling compiled files +CASM=cc +CASM_OPTIONS=-c # Assembler for assembling runtime library files -CASMRUNTIME=gcc -c +CASMRUNTIME=$(CASM) $(CASM_OPTIONS) # Linker -CLINKER=gcc +CLINKER=cc +CLINKER_OPTIONS=-no-pie + +# Preprocessor for .c files +CPREPRO=cc +CPREPRO_OPTIONS=-std c99 -U__GNUC__ -E # Archiver to build .a libraries ARCHIVER=ar rcs -# Math library. Set to empty under MacOS X +# Math library. Set to empty under macOS LIBMATH=-lm # Turn on/off the installation and use of the runtime support library @@ -771,8 +732,8 @@ ASM_SUPPORTS_CFI=false # Turn on/off compilation of clightgen CLIGHTGEN=false -# Whether the other tools support responsefiles in gnu syntax -RESPONSEFILE="none" +# Whether the other tools support responsefiles in GNU syntax or Diab syntax +RESPONSEFILE=gnu # diab # Whether to use the local copies of Flocq and MenhirLib LIBRARY_FLOCQ=local # external @@ -837,13 +798,12 @@ CompCert configuration: Application binary interface.. $abi Endianness.................... $endianness OS and development env........ $system - C compiler.................... $cc - C preprocessor................ $cprepro - Assembler..................... $casm + C compiler.................... $cc $cc_options + C preprocessor................ $cprepro $cprepro_options + Assembler..................... $casm $casm_options Assembler supports CFI........ $asm_supports_cfi Assembler for runtime lib..... $casmruntime - Linker........................ $clinker - Linker needs '-no-pie'........ $clinker_needs_no_pie + Linker........................ $clinker $clinker_options Archiver...................... $archiver Math library.................. $libmath Build command to use.......... $make -- cgit From a138b43ccb391be63bed2fea26cd36dab96b091f Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 25 Dec 2020 15:39:42 +0100 Subject: configure: use `$make` instead of `make` To make sure it works if `gmake` is required. Fixes: #381 --- configure | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'configure') diff --git a/configure b/configure index c5afabd8..0ca893d2 100755 --- a/configure +++ b/configure @@ -768,7 +768,7 @@ B cparser B extraction EOF -make CoqProject +$make CoqProject # # Clean up target-dependent files to force their recompilation -- cgit From c50680bb86564fe61db61e6140a418ccc7d36677 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 23 Dec 2020 15:54:51 +0100 Subject: AArch64: macOS port This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors. --- configure | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'configure') diff --git a/configure b/configure index 0ca893d2..7cbb9d7d 100755 --- a/configure +++ b/configure @@ -57,6 +57,7 @@ Supported targets: 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) + aarch64-macosx (AArch64, i.e. Apple silicon, MacOS) manual (edit configuration file by hand) For x86 targets, the "x86_32-" prefix can also be written "ia32-" or "i386-". @@ -404,6 +405,18 @@ if test "$arch" = "aarch64"; then abi="standard" cprepro_options="-std=c99 -U__GNUC__ -E" system="linux";; + macosx) + abi="apple" + casm="${toolprefix}cc" + casm_options="-c -arch arm64" + cc="${toolprefix}cc -arch arm64" + clinker="${toolprefix}cc" + clinker_needs_no_pie=false + cprepro="${toolprefix}cc" + cprepro_options="-std=c99 -arch arm64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -E" + libmath="" + system="macosx" + ;; *) echo "Error: invalid eabi/system '$target' for architecture AArch64." 1>&2 echo "$usage" 1>&2 -- cgit From ebcece704b34a276fae56a546133a15f75086cdd Mon Sep 17 00:00:00 2001 From: Daniel Dickman Date: Mon, 28 Dec 2020 09:40:09 -0500 Subject: configure: add -mandir option (#382) To control where man pages are installed. The default `/usr/local/share/man` is good for Linux but BSD prefers `/usr/local/man`. --- configure | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'configure') diff --git a/configure b/configure index 7cbb9d7d..b0d57823 100755 --- a/configure +++ b/configure @@ -18,6 +18,7 @@ prefix='/usr/local' bindir='$(PREFIX)/bin' libdir='$(PREFIX)/lib/compcert' +mandir='$(PREFIX)/share/man' coqdevdir='$(PREFIX)/lib/compcert/coq' toolprefix='' target='' @@ -85,6 +86,7 @@ Options: -prefix Install in /bin and /lib/compcert -bindir Install binaries in -libdir Install libraries in + -mandir Install man pages 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 @@ -114,6 +116,8 @@ while : ; do bindir="$2"; shift;; -libdir|--libdir) libdir="$2"; shift;; + -mandir|--mandir) + mandir="$2"; shift;; -coqdevdir|--coqdevdir) coqdevdir="$2"; install_coqdev=true; shift;; -toolprefix|--toolprefix) @@ -614,7 +618,7 @@ cat > Makefile.config < Date: Mon, 28 Dec 2020 15:48:35 +0100 Subject: configure: simplify the final printing of the configuration Factor out the substitution of `$prefix` for `\$(PREFIX)` using a shell function `expandprefix`. --- configure | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) (limited to 'configure') diff --git a/configure b/configure index b0d57823..ac41ab56 100755 --- a/configure +++ b/configure @@ -803,10 +803,9 @@ Please finish the configuration by editing file ./Makefile.config. EOF else -bindirexp=`echo "$bindir" | sed -e "s|\\\$(PREFIX)|$prefix|"` -libdirexp=`echo "$libdir" | sed -e "s|\\\$(PREFIX)|$prefix|"` -mandirexp=`echo "$mandir" | sed -e "s|\\\$(PREFIX)|$prefix|"` -coqdevdirexp=`echo "$coqdevdir" | sed -e "s|\\\$(PREFIX)|$prefix|"` +expandprefix() { + echo "$1" | sed -e "s|\\\$(PREFIX)|$prefix|" +} cat < Date: Thu, 14 Jan 2021 19:11:38 +0100 Subject: Coq 8.13.0 is supported However it produces new warnings that should be investigated later. --- configure | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'configure') diff --git a/configure b/configure index ac41ab56..5fe1e2bf 100755 --- a/configure +++ b/configure @@ -503,19 +503,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.12.0|8.12.1|8.12.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|8.12.1|8.12.2|8.13.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 a version of Coq between 8.8.0 and 8.12.2" + echo "Error: CompCert requires a version of Coq between 8.8.0 and 8.13.0" missingtools=true fi;; "") echo "NOT FOUND" - echo "Error: make sure Coq version 8.11.2 is installed." + echo "Error: make sure Coq version 8.12.2 is installed." missingtools=true;; esac -- cgit From 0a39cdab7f7ad8dc73339d17563a85d6f57f1710 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 18 Jan 2021 19:00:47 +0100 Subject: macOS: turn #warning off The standard includes print irrelevant warnings using `#warning`. The warnings can be restored by passing `-W#warning` to `ccomp`. --- configure | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'configure') diff --git a/configure b/configure index 5fe1e2bf..a6cf84f7 100755 --- a/configure +++ b/configure @@ -363,7 +363,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then casm_options="-arch x86_64 -c" clinker_options="-arch x86_64" clinker_needs_no_pie=false - cprepro_options="-std=c99 -arch x86_64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -E" + cprepro_options="-std=c99 -arch x86_64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -Wno-\\#warnings -E" libmath="" system="macosx" ;; @@ -417,7 +417,7 @@ if test "$arch" = "aarch64"; then clinker="${toolprefix}cc" clinker_needs_no_pie=false cprepro="${toolprefix}cc" - cprepro_options="-std=c99 -arch arm64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -E" + cprepro_options="-std=c99 -arch arm64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -Wno-\\#warnings -E" libmath="" system="macosx" ;; -- cgit From ab62e1bed37d2efe4d2a9e0139839bae21b1cdd9 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 18 Jan 2021 19:56:44 +0100 Subject: "macosx" is now called "macos" The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos". --- configure | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'configure') diff --git a/configure b/configure index a6cf84f7..4b75509e 100755 --- a/configure +++ b/configure @@ -53,12 +53,12 @@ Supported targets: x86_32-cygwin (x86 32 bits, Cygwin environment under Windows) x86_64-linux (x86 64 bits, Linux) x86_64-bsd (x86 64 bits, BSD) - x86_64-macosx (x86 64 bits, MacOS X) + x86_64-macos (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) - aarch64-macosx (AArch64, i.e. Apple silicon, MacOS) + aarch64-macos (AArch64, i.e. Apple silicon, MacOS) manual (edit configuration file by hand) For x86 targets, the "x86_32-" prefix can also be written "ia32-" or "i386-". @@ -357,15 +357,15 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then cprepro_options="-std=c99 -m64 -U__GNUC__ -E" system="linux" ;; - macosx) - abi="macosx" + macos|macosx) + abi="macos" cc_options="-arch x86_64" casm_options="-arch x86_64 -c" clinker_options="-arch x86_64" clinker_needs_no_pie=false cprepro_options="-std=c99 -arch x86_64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -Wno-\\#warnings -E" libmath="" - system="macosx" + system="macos" ;; cygwin) abi="standard" @@ -409,7 +409,7 @@ if test "$arch" = "aarch64"; then abi="standard" cprepro_options="-std=c99 -U__GNUC__ -E" system="linux";; - macosx) + macos|macosx) abi="apple" casm="${toolprefix}cc" casm_options="-c -arch arm64" @@ -419,7 +419,7 @@ if test "$arch" = "aarch64"; then cprepro="${toolprefix}cc" cprepro_options="-std=c99 -arch arm64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -Wno-\\#warnings -E" libmath="" - system="macosx" + system="macos" ;; *) echo "Error: invalid eabi/system '$target' for architecture AArch64." 1>&2 @@ -708,7 +708,7 @@ ENDIANNESS= # Possible choices for x86: # SYSTEM=linux # SYSTEM=bsd -# SYSTEM=macosx +# SYSTEM=macos # SYSTEM=cygwin SYSTEM= -- cgit From 6bf310dd678285dc193798e89fc2c441d8430892 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 9 Mar 2021 10:39:33 +0100 Subject: Coq 8.13.1 is supported Closes: #389 --- configure | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'configure') diff --git a/configure b/configure index 4b75509e..a3444de8 100755 --- a/configure +++ b/configure @@ -503,14 +503,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.12.1|8.12.2|8.13.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|8.12.2|8.13.0|8.13.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.13.0" + echo "Error: CompCert requires a version of Coq between 8.8.0 and 8.13.1" missingtools=true fi;; "") -- 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 --- configure | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'configure') diff --git a/configure b/configure index 720ac511..469edd65 100755 --- a/configure +++ b/configure @@ -8,10 +8,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. # # # ####################################################################### @@ -367,7 +368,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then casm_options="-arch x86_64 -c" clinker_options="-arch x86_64" clinker_needs_no_pie=false - cprepro_options="-std=c99 -arch x86_64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -Wno-\\#warnings -E" + cprepro_options="-std=c99 -arch x86_64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E" libmath="" system="macos" ;; @@ -455,7 +456,7 @@ if test "$arch" = "aarch64"; then clinker="${toolprefix}cc" clinker_needs_no_pie=false cprepro="${toolprefix}cc" - cprepro_options="-std=c99 -arch arm64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -Wno-\\#warnings -E" + cprepro_options="-std=c99 -arch arm64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E" libmath="" system="macos" ;; @@ -541,14 +542,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.12.1|8.12.2|8.13.0|8.13.1) + 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|8.13.0|8.13.1|8.13.2) 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.13.1" + echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.13.2" missingtools=true fi;; "") -- cgit From d41bc9d9eecb7febc7ad48cb7d3a35768b73ee54 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 1 Jun 2021 15:54:47 +0200 Subject: Add target ELF --- configure | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'configure') diff --git a/configure b/configure index acc72e91..7467e80a 100755 --- a/configure +++ b/configure @@ -58,8 +58,9 @@ Supported targets: x86_64-cygwin (x86 64 bits, Cygwin environment under Windows) rv32-linux (RISC-V 32 bits, Linux) rv64-linux (RISC-V 64 bits, Linux) - kvx-mbr (Kalray KVX, bare runtime) - kvx-cos (Kalray KVX, ClusterOS) + kvx-mbr (Kalray KV3, bare runtime) + kvx-elf (Kalray KV3, ELF) + kvx-cos (Kalray KV3, ClusterOS) aarch64-linux (AArch64, i.e. ARMv8 in 64-bit mode, Linux) aarch64-macos (AArch64, i.e. Apple silicon, MacOS) manual (edit configuration file by hand) -- cgit From 3181fe5407ed0221714830e2bd1e19850eac5461 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 1 Jun 2021 18:28:11 +0200 Subject: Remove install path bricolage for kvx --- configure | 2 -- 1 file changed, 2 deletions(-) (limited to 'configure') diff --git a/configure b/configure index 7467e80a..ae3a7c00 100755 --- a/configure +++ b/configure @@ -431,8 +431,6 @@ if test "$arch" = "kvx"; then casm_options="$model_options" cc="$k1base-gcc $model_options" clinker="$k1base-gcc" - bindir="$HOME/.usr/bin" - libdir="$HOME/.usr/lib" clinker_options="$model_options -L$libdir -Wl,-rpath=$libdir" cprepro="$k1base-gcc" cprepro_options="$model_options -D __KVX_${osupper}__ -std=c99 -E -include ccomp_kvx_fixes.h" -- cgit