diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-23 19:12:19 +0100 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-23 19:12:19 +0100 |
commit | dcb523736e82d72b03fa8d055bf74472dba7345c (patch) | |
tree | 71e797c92d45dca509527043d233c51b2ed8fc86 /configure | |
parent | 3e953ef41f736ed5b7db699b1adf21d46cb5b8db (diff) | |
parent | 6bf310dd678285dc193798e89fc2c441d8430892 (diff) | |
download | compcert-kvx-dcb523736e82d72b03fa8d055bf74472dba7345c.tar.gz compcert-kvx-dcb523736e82d72b03fa8d055bf74472dba7345c.zip |
Merge branch 'master' into merge_master_8.13.1
PARTIAL MERGE (PARTLY BROKEN).
See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE
WARNING:
interface of va_args and assembly sections have changed
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 188 |
1 files changed, 86 insertions, 102 deletions
@@ -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='' @@ -25,7 +26,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 @@ -53,13 +53,14 @@ 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) kvx-mbr (Kalray KVX, bare runtime) kvx-cos (Kalray KVX, 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) For x86 targets, the "x86_32-" prefix can also be written "ia32-" or "i386-". @@ -87,6 +88,7 @@ Options: -prefix <dir> Install in <dir>/bin and <dir>/lib/compcert -bindir <dir> Install binaries in <dir> -libdir <dir> Install libraries in <dir> + -mandir <dir> Install man pages in <dir> -coqdevdir <dir> Install Coq development (.vo files) in <dir> -toolprefix <pref> Prefix names of tools ("gcc", etc) with <pref> -use-external-Flocq Use an already-installed Flocq library @@ -116,6 +118,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) @@ -209,13 +213,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 @@ -235,13 +250,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 @@ -279,19 +288,14 @@ 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" ;; *) - 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 @@ -306,38 +310,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" ;; *) @@ -355,53 +347,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" + macos|macosx) + abi="macos" + 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" + 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" - 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" ;; *) @@ -422,14 +397,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 @@ -474,15 +445,20 @@ 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";; + macos|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=' -Wno-\\#warnings -E" + libmath="" + system="macos" + ;; *) echo "Error: invalid eabi/system '$target' for architecture AArch64." 1>&2 echo "$usage" 1>&2 @@ -565,19 +541,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|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.12.1" + echo "Error: CompCert requires a version of Coq between 8.8.0 and 8.13.1" 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 @@ -680,7 +656,7 @@ cat > Makefile.config <<EOF PREFIX=$prefix BINDIR=$bindir LIBDIR=$libdir -MANDIR=$sharedir/man +MANDIR=$mandir SHAREDIR=$sharedir COQDEVDIR=$coqdevdir OCAML_NATIVE_COMP=$ocaml_native_comp @@ -698,12 +674,13 @@ BITSIZE=$bitsize CASM=$casm CASM_OPTIONS=$casm_options CASMRUNTIME=$casmruntime -CC=$cc +CC=$cc $cc_options CLIGHTGEN=$clightgen 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 @@ -769,26 +746,32 @@ ENDIANNESS= # Possible choices for x86: # SYSTEM=linux # SYSTEM=bsd -# SYSTEM=macosx +# SYSTEM=macos # 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 @@ -804,8 +787,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 @@ -876,7 +859,7 @@ B cparser B extraction EOF -make CoqProject +$make CoqProject # # Clean up target-dependent files to force their recompilation @@ -894,9 +877,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|"` -coqdevdirexp=`echo "$coqdevdir" | sed -e "s|\\\$(PREFIX)|$prefix|"` +expandprefix() { + echo "$1" | sed -e "s|\\\$(PREFIX)|$prefix|" +} cat <<EOF @@ -906,28 +889,29 @@ 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 Menhir API library............ $menhir_dir The Flocq library............. $library_Flocq The MenhirLib library......... $library_MenhirLib - Binaries installed in......... $bindirexp + Binaries installed in......... $(expandprefix $bindir) Runtime library provided...... $has_runtime_lib - Library files installed in.... $libdirexp + Library files installed in.... $(expandprefix $libdir) + Man pages installed in........ $(expandprefix $mandir) Standard headers provided..... $has_standard_headers - Standard headers installed in. $libdirexp/include + Standard headers installed in. $(expandprefix $libdir)/include EOF if $install_coqdev; then cat <<EOF - Coq development installed in.. $coqdevdirexp + Coq development installed in.. $(expandprefix $coqdevdir) EOF else cat <<EOF |