#!/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 INRIA Non-Commercial License Agreement. #
# #
#######################################################################
prefix='/usr/local'
bindir='$(PREFIX)/bin'
libdir='$(PREFIX)/lib/compcert'
toolprefix=''
target=''
has_runtime_lib=true
has_standard_headers=true
clightgen=false
responsefile="gnu"
merlin=false
usage='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-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-macosx (x86 64 bits, MacOS X)
manual (edit configuration file by hand)
For x86 targets, the "x86_32-" prefix can also be written "ia32-".
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
armv7a- ARMv7-A + VFPv3-d16 (default for arm-)
armv7r- ARMv7-R + VFPv3-d16
armv7m- ARMv7-M + VFPv3-d16
armebv6- ARMv6 + 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
-toolprefix Prefix names of tools ("gcc", etc) with
-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 the clightgen tool
-merlin Generate .merlin file
'
#
# 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;;
-toolprefix|--toolprefix)
toolprefix="$2"; shift;;
-no-runtime-lib)
has_runtime_lib=false;;
-no-standard-headers)
has_standard_headers=false;;
-clightgen)
clightgen=true;;
-merlin)
merlin=true;;
*)
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;;
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;;
armebv7r-*)
arch="arm"; model="armv7r"; endianness="big"; bitsize=32;;
armebv7m-*)
arch="arm"; model="armv7m"; endianness="big"; bitsize=32;;
x86_32-*|ia32-*)
arch="x86"; model="32sse2"; endianness="little"; bitsize=32;;
x86_64-*)
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;;
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
asm_supports_cfi=""
casm_options=""
casmruntime=""
clinker_options=""
cprepro_options=""
struct_passing=""
struct_return=""
#
# 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
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"
struct_passing="ints"
struct_return="int1-4"
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)
struct_return="ref"
;;
*)
struct_return="int1-8"
;;
esac
case "$target" in
eabi-diab)
abi="eabi"
asm_supports_cfi=false
casm="${toolprefix}das"
casm_options="-Xalign-value"
cc="${toolprefix}dcc"
clinker="${toolprefix}dcc"
cprepro="${toolprefix}dcc"
cprepro_options="-E -D__GNUC__"
libmath="-lm"
struct_passing="ref-caller"
system="diab"
responsefile="diab"
;;
*)
abi="eabi"
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"
struct_passing="ref-caller"
system="linux"
;;
esac
fi
#
# x86 (32 bits) Target Configuration
#
if test "$arch" = "x86" -a "$bitsize" = "32"; then
case "$target" in
bsd)
abi="standard"
casm="${toolprefix}gcc"
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"
struct_passing="ints"
struct_return="int1248" # to check!
system="bsd"
;;
cygwin)
abi="standard"
casm="${toolprefix}gcc"
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"
struct_passing="ints"
struct_return="ref"
system="cygwin"
;;
linux)
abi="standard"
casm="${toolprefix}gcc"
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"
struct_passing="ints"
struct_return="ref"
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"
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=""
struct_passing="ints"
struct_return="int1248"
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
exit 2;;
esac
fi
#
# IA32 (64 bits) Target Configuration
#
if test "$arch" = "x86" -a "$bitsize" = "64"; then
case "$target" in
linux)
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__ -E"
libmath="-lm"
struct_passing="ref-callee" # wrong!
struct_return="ref" # to check!
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 x86_64 -c"
cc="${toolprefix}gcc -arch x86_64"
clinker="${toolprefix}gcc"
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=""
struct_passing="ref-callee" # wrong!
struct_return="ref" # to check!
system="macosx"
;;
*)
echo "Error: invalid eabi/system '$target' for architecture X86_64." 1>&2
echo "$usage" 1>&2
exit 2;;
esac
fi
#
# Finalize Target Configuration
#
if test -z "$casmruntime"; then casmruntime="$casm $casm_options"; fi
#
# 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'
f=/tmp/compcert-configure-$$.s
rm -f $f
cat >> $f </dev/null
then echo "yes"; asm_supports_cfi=true
else echo "no"; asm_supports_cfi=false
fi
rm -f $f
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.6)
echo "version $coq_ver -- good!";;
?.*)
echo "version $coq_ver -- UNSUPPORTED"
echo "Error: CompCert requires Coq version 8.6."
missingtools=true;;
*)
echo "NOT FOUND"
echo "Error: make sure Coq version 8.6 is installed."
missingtools=true;;
esac
echo "Testing OCaml... " | tr -d '\n'
ocaml_ver=`ocamlopt -version 2>/dev/null`
case "$ocaml_ver" in
4.00.*|4.01.*)
echo "version $ocaml_ver -- UNSUPPORTED"
echo "Error: CompCert requires OCaml version 4.02 or later."
missingtools=true;;
4.0*)
echo "version $ocaml_ver -- good!";;
?.*)
echo "version $ocaml_ver -- UNSUPPORTED"
echo "Error: CompCert requires OCaml version 4.02 or later."
missingtools=true;;
*)
echo "NOT FOUND"
echo "Error: make sure OCaml version 4.02 or later is installed."
missingtools=true;;
esac
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
echo "yes"
ocaml_opt_comp=true
else
echo "no, will do without"
ocaml_opt_comp=false
fi
MENHIR_REQUIRED=20160303
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_includes="-I `menhir --suggest-menhirLib`"
else
echo "version $menhir_ver -- UNSUPPORTED"
echo "Error: CompCert requires Menhir version $MENHIR_REQUIRED or later."
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
if $merlin; then
cat > .merlin < Makefile.config <> Makefile.config <> Makefile.config <> Makefile.config <<'EOF'
# Target architecture
# ARCH=powerpc
# ARCH=arm
# ARCH=x86
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=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=
# Target ABI
# ABI=eabi # for PowerPC / Linux and other SVR4 or EABI platforms
# ABI=eabi # for ARM
# ABI=hardfloat # for ARM
# ABI=standard # for x86
ABI=
# Target bit width
# BITSIZE=64 # for x86 in 64-bit mode
# BITSIZE=32 # otherwise
BITSIZE=
# Target endianness
# ENDIANNESS=big # for ARM or PowerPC
# ENDIANNESS=little # for ARM or x86
ENDIANNESS=
# Default calling conventions for passing structs and unions by value
# See options -fstruct-passing=