configure

#!/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'
coqdevdir='$(PREFIX)/lib/compcert/coq'
toolprefix=''
target=''
has_runtime_lib=true
has_standard_headers=true
clightgen=false
install_coqdev=false
responsefile="gnu"
ignore_coq_version=false

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-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-bsd           (x86 64 bits, BSD)
  x86_64-macosx        (x86 64 bits, MacOS X)
  rv32-linux           (RISC-V 32 bits, Linux)
  rv64-linux           (RISC-V 64 bits, Linux)
  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 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 <dir>        Install in <dir>/bin and <dir>/lib/compcert
  -bindir <dir>        Install binaries in <dir>
  -libdir <dir>        Install libraries in <dir>
  -coqdevdir <dir>     Install Coq development (.vo files) in <dir>
  -toolprefix <pref>   Prefix names of tools ("gcc", etc) with <pref>
  -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;;
    -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;;
    -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;;
  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_needs_no_pie=true
clinker_options=""
cprepro_options=""


#
# 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"
  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__"
        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
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"
        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__ '-D__attribute__(x)=' -E"
        libmath="-lm"
        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"
        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"
        clinker_needs_no_pie=false
        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=""
        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

#
# x86 (64 bits) Target Configuration
#
if test "$arch" = "x86" -a "$bitsize" = "64"; then

  case "$target" in
    bsd)
        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"
        system="bsd"
        ;;
    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"
        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"
        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"
        ;;
    *)
        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"
  casm="${toolprefix}gcc"
  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


#
# 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" <<EOF
int main (void)
{
   return 0;
}
EOF
    errout=$("$@" -o "$tmpout" "$tmpsrc" 2>&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" <<EOF
testfun:
  .file 1 "testfun.c"
  .loc 1 1
  .cfi_startproc
  .cfi_adjust_cfa_offset 16
  .cfi_endproc
EOF
  if $casm $casm_options -o /dev/null "$tmpsrc" 2>/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.6.1|8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.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 one of the following Coq versions: 8.9.0, 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0, 8.6.1"
            missingtools=true
        fi;;
  "")
        echo "NOT FOUND"
        echo "Error: make sure Coq version 8.9.0 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.02.*|4.03.*|4.04.*)
      echo "version $ocaml_ver -- good!"
      echo "WARNING: some Intel processors of the Skylake and Kaby Lake generations"
      echo "have a hardware bug that can be triggered by this version of OCaml."
      echo "To avoid this risk, it is recommended to use OCaml 4.05 or later.";;
  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=20161201
MENHIR_NEW_API=20180530
menhir_flags=''
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`"
          if test "$menhir_ver" -ge $MENHIR_NEW_API; then
              menhir_flags="--coq-lib-path compcert.cparser.MenhirLib"
          fi
      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

cat > .merlin <<EOF
S lib
S common
S $arch
S backend
S cfrontend
S driver
S debug
S exportclight
S cparser
S extraction

B lib
B common
B $arch
B backend
B cfrontend
B driver
B debug
B exportclight
B cparser
B extraction

EOF

echo "-R lib compcert.lib \
-R common compcert.common \
-R ${arch} compcert.${arch} \
-R backend compcert.backend \
-R cfrontend compcert.cfrontend \
-R driver compcert.driver \
-R flocq compcert.flocq \
-R exportclight compcert.exportclight \
-R cparser compcert.cparser" > _CoqProject
case $arch in
    x86)
        echo "-R x86_${bitsize} compcert.x86_${bitsize}" >> _CoqProject
        ;;
esac

#
# Generate Makefile.config
#
sharedir="$(dirname "$bindir")"/share

rm -f Makefile.config
cat > Makefile.config <<EOF
PREFIX=$prefix
BINDIR=$bindir
LIBDIR=$libdir
MANDIR=$sharedir/man
SHAREDIR=$sharedir
COQDEVDIR=$coqdevdir
OCAML_OPT_COMP=$ocaml_opt_comp
MENHIR_INCLUDES=$menhir_includes
MENHIR_FLAGS=$menhir_flags
COMPFLAGS=-bin-annot
EOF

if test "$target" != "manual"; then
cat >> Makefile.config <<EOF
ABI=$abi
ARCH=$arch
ASM_SUPPORTS_CFI=$asm_supports_cfi
BITSIZE=$bitsize
CASM=$casm
CASM_OPTIONS=$casm_options
CASMRUNTIME=$casmruntime
CC=$cc
CLIGHTGEN=$clightgen
CLINKER=$clinker
CLINKER_OPTIONS=$clinker_options
CPREPRO=$cprepro
CPREPRO_OPTIONS=$cprepro_options
ENDIANNESS=$endianness
HAS_RUNTIME_LIB=$has_runtime_lib
HAS_STANDARD_HEADERS=$has_standard_headers
INSTALL_COQDEV=$install_coqdev
LIBMATH=$libmath
MODEL=$model
SYSTEM=$system
RESPONSEFILE=$responsefile
EOF
else
cat >> 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=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=

# 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=

# Target operating system and development environment
#
# Possible choices for PowerPC:
# SYSTEM=linux
# SYSTEM=diab
#
# Possible choices for ARM:
# SYSTEM=linux
#
# Possible choices for x86:
# SYSTEM=linux
# SYSTEM=bsd
# SYSTEM=macosx
# SYSTEM=cygwin
SYSTEM=

# C compiler for compiling runtime library files and some tests
CC=gcc

# Preprocessor for .c files
CPREPRO=gcc -U__GNUC__ -E

# Assembler for assembling .s files
CASM=gcc -c

# Assembler for assembling runtime library files
CASMRUNTIME=gcc -c

# Linker
CLINKER=gcc

# Math library. Set to empty under MacOS X
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
RESPONSEFILE="none"

EOF
fi

#
# Clean up target-dependent files to force their recompilation
#
rm -f .depend $arch/Archi.vo ${arch}_${bitsize}/Archi.vo runtime/*.o

#
# Summarize Configuration
#
if test "$target" = "manual"; then
cat <<EOF

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|"`

cat <<EOF

CompCert configuration:
    Target architecture........... $arch
    Hardware model................ $model
    Application binary interface.. $abi
    Endianness.................... $endianness
    OS and development env........ $system
    C compiler.................... $cc
    C preprocessor................ $cprepro
    Assembler..................... $casm
    Assembler supports CFI........ $asm_supports_cfi
    Assembler for runtime lib..... $casmruntime
    Linker........................ $clinker
    Linker needs '-no-pie'........ $clinker_needs_no_pie
    Math library.................. $libmath
    Build command to use.......... $make
    Binaries installed in......... $bindirexp
    Runtime library provided...... $has_runtime_lib
    Library files installed in.... $libdirexp
    Standard headers provided..... $has_standard_headers
    Standard headers installed in. $libdirexp/include
EOF

if $install_coqdev; then
cat <<EOF
    Coq development installed in.. $coqdevdirexp
EOF
else
cat <<EOF
    Coq development will not be installed
EOF
fi

fi