diff options
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 197 |
1 files changed, 91 insertions, 106 deletions
@@ -8,16 +8,18 @@ # # # 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. # # # ####################################################################### prefix='/usr/local' bindir='$(PREFIX)/bin' libdir='$(PREFIX)/lib/compcert' +mandir='$(PREFIX)/share/man' coqdevdir='$(PREFIX)/lib/compcert/coq' toolprefix='' target='' @@ -25,7 +27,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,7 +54,7 @@ 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) verilog-linux (x86 64 bits, Linux) verilog-bsd (x86 64 bits, BSD) @@ -61,6 +62,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-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-". @@ -88,6 +90,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 @@ -117,6 +120,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) @@ -210,13 +215,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 @@ -236,13 +252,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 @@ -280,19 +290,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 @@ -307,38 +312,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" ;; *) @@ -356,53 +349,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=' '-D__DARWIN_OS_INLINE=static inline' -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" ;; *) @@ -472,14 +448,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 @@ -490,15 +462,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=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E" + libmath="" + system="macos" + ;; *) echo "Error: invalid eabi/system '$target' for architecture AArch64." 1>&2 echo "$usage" 1>&2 @@ -581,19 +558,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.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.12.1" + echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.13.2" 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 @@ -696,7 +673,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 @@ -714,12 +691,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 @@ -785,26 +763,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 - -# Preprocessor for .c files -CPREPRO=gcc -U__GNUC__ -E +# C compiler (for testing only) +CC=cc -# 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 -# Math library. Set to empty under MacOS X +# 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 LIBMATH=-lm # Turn on/off the installation and use of the runtime support library @@ -820,8 +804,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 @@ -856,7 +840,7 @@ B cparser B extraction EOF -make CoqProject +$make CoqProject # # Clean up target-dependent files to force their recompilation @@ -874,9 +858,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 @@ -886,28 +870,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 |