#!/bin/sh
#######################################################################
# #
# The Compcert verified compiler #
# #
# Xavier Leroy, INRIA Paris-Rocquencourt #
# #
# 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. #
# #
#######################################################################
prefix='/usr/local'
bindir='$(PREFIX)/bin'
libdir='$(PREFIX)/lib/compcert'
mandir='$(PREFIX)/share/man'
coqdevdir='$(PREFIX)/lib/compcert/coq'
toolprefix=''
target=''
has_runtime_lib=true
has_standard_headers=true
clightgen=false
install_coqdev=false
ignore_coq_version=false
library_Flocq=local
library_MenhirLib=local
usage='Usage: ./configure [options] target
For help on options and targets, do: ./configure -help
'
help='Usage: ./configure [options] target
Supported targets:
ppc-eabi (PowerPC, EABI with GNU/Unix tools)
ppc-eabi-diab (PowerPC, EABI with Diab tools)
ppc-linux (PowerPC, Linux)
arm-eabi (ARM, EABI, little endian)
arm-linux (ARM, EABI, little endian)
arm-eabihf (ARM, EABI using hardware FP registers, little endian)
arm-hardfloat (ARM, EABI using hardware FP registers, little endian)
armeb-eabi (ARM, EABI, big endian)
armeb-linux (ARM, EABI, big endian)
armeb-eabihf (ARM, EABI using hardware FP registers, big endian)
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-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-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)
manual (edit configuration file by hand)
For x86 targets, the "x86_32-" prefix can also be written "ia32-" or "i386-".
For x86 targets, the "x86_64-" prefix can also be written "amd64-".
For AArch64 targets, the "aarch64-" prefix can also be written "arm64-".
For PowerPC targets, the "ppc-" prefix can be refined into:
ppc64- PowerPC 64 bits
e5500- Freescale e5500 core (PowerPC 64 bit, EREF extensions)
For ARM targets, the "arm-" or "armeb-" prefix can be refined into:
armv6- ARMv6 + VFPv2 (Thumb mode not supported)
armv6t2- ARMv6T2 + VFPv2
armv7a- ARMv7-A + VFPv3-d16 (default for arm-)
armv7r- ARMv7-R + VFPv3-d16
armv7m- ARMv7-M + VFPv3-d16
armebv6- ARMv6 + VFPv2 (Thumb mode not supported)
armebv6t2- ARMv6T2 + VFPv2
armebv7a- ARMv7-A + VFPv3-d16 (default for armeb-)
armebv7r- ARMv7-R + VFPv3-d16
armebv7m- ARMv7-M + VFPv3-d16
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
-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
-install-coqdev Also install the Coq development (implied by -clightgen)
-ignore-coq-version Accept to use experimental or unsupported versions of Coq
'
#
# Remove Leftover Makefile.config (if any) (GPR#244)
#
rm -f Makefile.config
#
# Parse Command-Line Arguments
#
while : ; do
case "$1" in
"")
break;;
-prefix|--prefix)
prefix="$2"; shift;;
-bindir|--bindir)
bindir="$2"; shift;;
-libdir|--libdir)
libdir="$2"; shift;;
-mandir|--mandir)
mandir="$2"; shift;;
-coqdevdir|--coqdevdir)
coqdevdir="$2"; install_coqdev=true; shift;;
-toolprefix|--toolprefix)
toolprefix="$2"; shift;;
-no-runtime-lib)
has_runtime_lib=false;;
-no-standard-headers)
has_standard_headers=false;;
-clightgen)
clightgen=true
install_coqdev=true;;
-ignore-coq-version|--ignore-coq-version)
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;;
-*)
echo "Error: unknown option '$1'." 1>&2
echo "$usage" 1>&2
exit 2;;
*)
if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi
target="$1";;
esac
shift
done
#
# Extract Architecture, Model and Default Endianness
#
case "$target" in
arm-*|armv7a-*)
arch="arm"; model="armv7a"; endianness="little"; bitsize=32;;
armv6-*)
arch="arm"; model="armv6"; endianness="little"; bitsize=32;;
armv6t2-*)
arch="arm"; model="armv6t2"; endianness="little"; bitsize=32;;
armv7r-*)
arch="arm"; model="armv7r"; endianness="little"; bitsize=32;;
armv7m-*)
arch="arm"; model="armv7m"; endianness="little"; bitsize=32;;
armeb-*|armebv7a-*)
arch="arm"; model="armv7a"; endianness="big"; bitsize=32;;
armebv6-*)
arch="arm"; model="armv6"; endianness="big"; bitsize=32;;
armebv6t2-*)
arch="arm"; model="armv6t2"; endianness="big"; bitsize=32;;
armebv7r-*)
arch="arm"; model="armv7r"; endianness="big"; bitsize=32;;
armebv7m-*)
arch="arm"; model="armv7m"; endianness="big"; bitsize=32;;
x86_32-*|ia32-*|i386-*)
arch="x86"; model="32sse2"; endianness="little"; bitsize=32;;
x86_64-*|amd64-*)
arch="x86"; model="64"; endianness="little"; bitsize=64;;
powerpc-*|ppc-*)
arch="powerpc"; model="ppc32"; endianness="big"; bitsize=32;;
powerpc64-*|ppc64-*)
arch="powerpc"; model="ppc64"; endianness="big"; bitsize=32;;
e5500-*)
arch="powerpc"; model="e5500"; endianness="big"; bitsize=32;;
rv32-*)
arch="riscV"; model="32"; endianness="little"; bitsize=32;;
rv64-*)
arch="riscV"; model="64"; endianness="little"; bitsize=64;;
aarch64-*|arm64-*)
arch="aarch64"; model="default"; endianness="little"; bitsize=64;;
manual)
;;
"")
echo "Error: no target architecture specified." 1>&2
echo "$usage" 1>&2
exit 2
;;
*)
echo "Error: unknown target architecture: '$target'." 1>&2
echo "$usage" 1>&2
exit 2
;;
esac
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=""
cc="${toolprefix}gcc"
cc_options=""
casm="${toolprefix}gcc"
casm_options="-c"
casmruntime=""
clinker="${toolprefix}gcc"
clinker_options=""
clinker_needs_no_pie=true
cprepro="${toolprefix}gcc"
cprepro_options="-E"
archiver="${toolprefix}ar rcs"
libmath="-lm"
responsefile="gnu"
#
# ARM Target Configuration
#
if test "$arch" = "arm"; then
case "$target" in
eabi|linux)
abi="eabi"
;;
eabihf|hf|hardfloat)
abi="hardfloat"
;;
*)
echo "Error: invalid eabi/system '$target' for architecture ARM." 1>&2
echo "$usage" 1>&2
exit 2;;
esac
cprepro_options="-std=c99 -U__GNUC__ '-D__REDIRECT(name,proto,alias)=name proto' '-D__REDIRECT_NTH(name,proto,alias)=name proto' -E"
system="linux"
fi
#
# PowerPC Target Configuration
#
if test "$arch" = "powerpc"; then
case "$target" in
eabi|eabi-diab|linux)
;;
*)
echo "Error: invalid eabi/system '$target' for architecture PowerPC." 1>&2
echo "$usage" 1>&2
exit 2;;
esac
case "$target" in
linux)
abi="linux"
;;
*)
abi="eabi"
;;
esac
case "$target" in
eabi-diab)
asm_supports_cfi=false
casm="${toolprefix}das"
casm_options="-Xalign-value"
cc="${toolprefix}dcc"
clinker_needs_no_pie=false
clinker="${toolprefix}dcc"
cprepro="${toolprefix}dcc"
cprepro_options="-E -D__GNUC__"
archiver="${toolprefix}dar -q"
libmath="-lm"
system="diab"
responsefile="diab"
;;
*)
casmruntime="${toolprefix}gcc -c -Wa,-mregnames"
cprepro_options="-std=c99 -U__GNUC__ -E"
system="linux"
;;
esac
fi
#
# x86 (32 bits) Target Configuration
#
if test "$arch" = "x86" -a "$bitsize" = "32"; then
case "$target" in
bsd)
abi="standard"
cc_options="-m32"
casm_options="-m32 -c"
clinker_options="-m32"
cprepro_options="-std=c99 -m32 -U__GNUC__ -E"
system="bsd"
;;
cygwin)
abi="standard"
cc_options="-m32"
casm_options="-m32 -c"
clinker_options="-m32"
cprepro_options="-std=c99 -m32 -U__GNUC__ '-D__attribute__(x)=' -E"
system="cygwin"
;;
linux)
abi="standard"
cc_options="-m32"
casm_options="-m32 -c"
clinker_options="-m32"
cprepro_options="-std=c99 -m32 -U__GNUC__ -E"
system="linux"
;;
*)
echo "Error: invalid eabi/system '$target' for architecture IA32/X86_32." 1>&2
echo "$usage" 1>&2
exit 2;;
esac
fi
#
# x86 (64 bits) Target Configuration
#
if test "$arch" = "x86" -a "$bitsize" = "64"; then
case "$target" in
bsd)
abi="standard"
cc_options="-m64"
casm_options="-m64 -c"
clinker_options="-m64"
cprepro_options="-std=c99 -m64 -U__GNUC__ -E"
system="bsd"
;;
linux)
abi="standard"
cc_options="-m64"
casm_options="-m64 -c"
clinker_options="-m64"
cprepro_options="-std=c99 -m64 -U__GNUC__ -E"
system="linux"
;;
macosx)
abi="macosx"
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=' -E"
libmath=""
system="macosx"
;;
cygwin)
abi="standard"
cc_options="-m64"
casm_options="-m64 -c"
clinker_options="-m64"
cprepro_options="-std=c99 -m64 -U__GNUC__ '-D__attribute__(x)=' -E"
system="cygwin"
;;
*)
echo "Error: invalid eabi/system '$target' for architecture X86_64." 1>&2
echo "$usage" 1>&2
exit 2;;
esac
fi
#
# RISC-V Target Configuration
#
if test "$arch" = "riscV"; then
if test "$model" = "64"; then
model_options="-march=rv64imafd -mabi=lp64d"
else
model_options="-march=rv32imafd -mabi=ilp32d"
fi
abi="standard"
cc_options="$model_options"
casm_options="$model_options -c"
clinker_options="$model_options"
cprepro_options="$model_options -std=c99 -U__GNUC__ -E"
system="linux"
fi
#
# AArch64 (ARMv8 64 bits) Target Configuration
#
if test "$arch" = "aarch64"; then
case "$target" in
linux)
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
exit 2;;
esac
fi
#
# Finalize Target Configuration
#
if test -z "$casmruntime"; then casmruntime="$casm $casm_options"; fi
# Invoke a C compiler, e.g. to check for availability of command-line options
testcompiler () {
tmpsrc="${TMPDIR:-/tmp}/compcert-configure-$$.c"
rm -f "$tmpsrc"
tmpout="${TMPDIR:-/tmp}/compcert-configure-$$.out"
rm -f "$tmpout"
cat >> "$tmpsrc" <&1 >/dev/null)
retcode=$?
errcount=$(echo "${errout}" | grep -ciE "(unknown|unsupported|unrecognized).*(option|argument)")
rm -f "$tmpsrc" "$tmpout"
# Test failed or error is logged to stderr
if [ "${retcode}" != "0" ] || [ "${errcount}" != "0" ]; then return 1; fi
# OK and no error was logged
return 0
}
#
# Test Assembler Support for CFI Directives
#
if test "$target" != "manual" && test -z "$asm_supports_cfi"; then
echo "Testing assembler support for CFI directives... " | tr -d '\n'
tmpsrc="${TMPDIR:-/tmp}/compcert-configure-$$.s"
rm -f "$tmpsrc"
cat >> "$tmpsrc" </dev/null
then echo "yes"; asm_supports_cfi=true
else echo "no"; asm_supports_cfi=false
fi
rm -f "$tmpsrc"
fi
#
# Test Availability of Option '-no-pie' or '-nopie'
#
if ($clinker_needs_no_pie) then
echo "Testing linker support for '-no-pie' / '-nopie' option... " | tr -d '\n'
if testcompiler ${cc} -no-pie;
then echo "yes, '-no-pie'"; clinker_options="${clinker_options} -no-pie"
elif testcompiler ${cc} -nopie;
then echo "yes, '-nopie'"; clinker_options="${clinker_options} -nopie"
else echo "no"; clinker_needs_no_pie=false
fi
fi
#
# Test Availability of Required Tools
#
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)
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"
missingtools=true
fi;;
"")
echo "NOT FOUND"
echo "Error: make sure Coq version 8.11.2 is installed."
missingtools=true;;
esac
echo "Testing OCaml... " | tr -d '\n'
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"
echo "Error: CompCert requires OCaml version 4.05 or later."
missingtools=true;;
4.*)
echo "version $ocaml_ver -- good!";;
?.*)
echo "version $ocaml_ver -- UNSUPPORTED"
echo "Error: CompCert requires OCaml version 4.05 or later."
missingtools=true;;
*)
echo "NOT FOUND"
echo "Error: make sure OCaml version 4.05 or later is installed."
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'
ocamlopt_opt_ver=`ocamlopt.opt -version 2>/dev/null`
if test "$ocamlopt_opt_ver" = "$ocaml_ver"; then
echo "yes"
ocaml_opt_comp=true
else
echo "no, will do without"
ocaml_opt_comp=false
fi
MENHIR_REQUIRED=20190626
echo "Testing Menhir... " | tr -d '\n'
menhir_ver=`menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'`
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) || \
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."
echo "Consider using the OPAM package for Menhir."
missingtools=true
fi
else
echo "version $menhir_ver -- UNSUPPORTED"
echo "Error: CompCert requires a version greater or equal to $MENHIR_REQUIRED."
missingtools=true
fi;;
*)
echo "NOT FOUND"
echo "Error: make sure Menhir version $MENHIR_REQUIRED or later is installed."
missingtools=true;;
esac
echo "Testing GNU make... " | tr -d '\n'
make=''
for mk in make gmake gnumake; do
make_ver=`$mk -v 2>/dev/null | head -1 | sed -n -e 's/^GNU Make //p'`
case "$make_ver" in
3.8*|3.9*|[4-9].*)
echo "version $make_ver (command '$mk') -- good!"
make="$mk"
break;;
esac
done
if test -z "$make"; then
echo "NOT FOUND"
echo "Error: make sure GNU Make version 3.80 or later is installed."
missingtools=true
fi
if $missingtools; then
echo "One or several required tools are missing or too old. Aborting."
exit 2
fi
#
# Generate Makefile.config
#
sharedir="$(dirname "$bindir")"/share
rm -f Makefile.config
cat > Makefile.config <> Makefile.config <> Makefile.config <<'EOF'
# Target architecture
# ARCH=powerpc
# ARCH=arm
# ARCH=x86
# ARCH=riscV
# ARCH=aarch6
ARCH=
# Hardware variant
# MODEL=ppc32 # for plain PowerPC
# MODEL=ppc64 # for PowerPC with 64-bit instructions
# MODEL=e5500 # for Freescale e5500 PowerPC variant
# MODEL=armv6 # for ARM
# MODEL=armv6t2 # for ARM
# MODEL=armv7a # for ARM
# MODEL=armv7r # for ARM
# MODEL=armv7m # for ARM
# MODEL=32sse2 # for x86 in 32-bit mode
# MODEL=64 # for x86 in 64-bit mode
# MODEL=default # for others
MODEL=
# Target ABI
# ABI=eabi # for PowerPC / Linux and other SVR4 or EABI platforms
# ABI=eabi # for ARM
# ABI=hardfloat # for ARM
# ABI=standard # for others
ABI=
# Target bit width
# BITSIZE=64 # for x86 in 64-bit mode, RiscV in 64-bit mode, AArch64
# BITSIZE=32 # otherwise
BITSIZE=
# Target endianness
# ENDIANNESS=big # for ARM or PowerPC
# ENDIANNESS=little # for ARM or x86 or RiscV or AArch64
ENDIANNESS=
# Target operating system and development environment
#
# Possible choices for PowerPC:
# SYSTEM=linux
# SYSTEM=diab
#
# Possible choices for ARM, AArch64, RiscV:
# SYSTEM=linux
#
# Possible choices for x86:
# SYSTEM=linux
# SYSTEM=bsd
# SYSTEM=macosx
# SYSTEM=cygwin
SYSTEM=
# C compiler (for testing only)
CC=cc
# Assembler for assembling compiled files
CASM=cc
CASM_OPTIONS=-c
# Assembler for assembling runtime library files
CASMRUNTIME=$(CASM) $(CASM_OPTIONS)
# Linker
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
LIBMATH=-lm
# Turn on/off the installation and use of the runtime support library
HAS_RUNTIME_LIB=true
# Turn on/off the installation and use of the standard header files
HAS_STANDARD_HEADERS=true
# Whether the assembler $(CASM) supports .cfi debug directives
ASM_SUPPORTS_CFI=false
#ASM_SUPPORTS_CFI=true
# Turn on/off compilation of clightgen
CLIGHTGEN=false
# 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
LIBRARY_MENHIRLIB=local # external
EOF
fi
#
# Generate Merlin and CoqProject files to simplify development
#
cat > .merlin <