path: root/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 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=''
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-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 KV3, bare runtime)
  kvx-elf              (Kalray KV3, ELF)
  kvx-cos              (Kalray KV3, 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-".
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 <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
  -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;;
  kvx-*)
      arch="kvx"; 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__ -U__SIZEOF_INT128__ -E"
        system="bsd"
        ;;
    linux)
        abi="standard"
        cc_options="-m64"
        casm_options="-m64 -c"
        clinker_options="-m64"
        cprepro_options="-std=c99 -m64 -U__GNUC__ -U__SIZEOF_INT128__ -E"
        system="linux"
        ;;
    macos|macosx)
        abi="macos"
        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__SIZEOF_INT128__ -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"
        ;;
    cygwin)
        abi="standard"
        cc_options="-m64"
        casm_options="-m64 -c"
        clinker_options="-m64"
        cprepro_options="-std=c99 -m64 -U__GNUC__ -U__SIZEOF_INT128__ '-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

#
# KVX Target Configuration
#
if test "$arch" = "kvx"; then
  #model_options="-march=rv64imafd -mabi=lp64d"
  # FIXME - maybe later add it for NodeOS & cie
  #model_options=-m64
  model_options=
  abi="standard"
  if test "$target" = "mbr";
  then os="mbr";
  elif test "$target" = "cos";
  then os="cos";
  elif test "$target" = "elf";
  then os="elf";
  else
      echo "Unknown KVX backend"
      exit 1
  fi
  osupper=`echo $os|tr a-z A-Z`
  k1base="kvx-$os"
  casm="$k1base-as"
  casm_options="$model_options"
  cc="$k1base-gcc $model_options"
  clinker="$k1base-gcc"
  clinker_options="$model_options -L$libdir -Wl,-rpath=$libdir"
  cprepro="$k1base-gcc"
  cprepro_options="$model_options -D __KVX_${osupper}__ -std=c99 -E -include ccomp_kvx_fixes.h"
  libmath="-lm"
  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";;
    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
        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" <<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.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|8.14.0|8.14.1|8.15.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 a version of Coq between 8.9.0 and 8.15.0"
            missingtools=true
        fi;;
  "")
        echo "NOT FOUND"
        echo "Error: make sure Coq version 8.13.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.*|4.05.*)
        echo "version $ocaml_ver -- UNSUPPORTED"
        echo "Error: CompCert requires OCaml version 4.06 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 <<EOF
PREFIX=$prefix
BINDIR=$bindir
LIBDIR=$libdir
MANDIR=$mandir
SHAREDIR=$sharedir
COQDEVDIR=$coqdevdir
OCAML_NATIVE_COMP=$ocaml_native_comp
OCAML_OPT_COMP=$ocaml_opt_comp
OCAML_LM_PROF=false
MENHIR_DIR=$menhir_dir
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 $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
INSTALL_COQDEV=$install_coqdev
LIBMATH=$libmath
MODEL=$model
OS=${os:-unspecified}
SYSTEM=$system
RESPONSEFILE=$responsefile
LIBRARY_FLOCQ=$library_Flocq
LIBRARY_MENHIRLIB=$library_MenhirLib
EOF
else
cat >> 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=macos
# 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

if [ "$arch" = "aarch64" ]; then # for aarch64 scheduling
cat >> Makefile.config <<EOF
ARCHDIRS=$arch scheduling/abstractbb scheduling/postpass_lib
BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v IterList.v \\
    Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asm.v Asmblockprops.v\\
    ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
    Asmblockdeps.v\\
    AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\
    ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v
    # TODO: UPDATE THIS
    # DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v
EXTRA_EXTRACTION=   Asmgen.Asmgen_expand.loadimm32 Asmgen.Asmgen_expand.addimm64 Asmgen.Asmgen_expand.storeptr
EOF
fi

if [ "$arch" = "kvx" ]; then
cat >> Makefile.config <<EOF
ARCHDIRS=$arch scheduling/abstractbb scheduling/postpass_lib
EXECUTE=kvx-cluster --syscall=libstd_scalls.so --
CFLAGS= -D __KVX_COS__
SIMU=kvx-cluster -- 
BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\
    Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\
    FPExtra.v \\
    ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
    Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v\\
    FPDivision32.v FPDivision64.v ExtValues.v ExtFloats.v\\
    AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v
EOF
fi

if [ "$arch" = "riscV" ] ; then
cat >> Makefile.config <<EOF
EXTRA_EXTRACTION=Asm.ireg_eq Asm.ireg0_eq
BACKENDLIB=Asmgenproof0.v Asmgenproof1.v ExtValues.v
EOF
fi

#
# Generate Merlin and CoqProject files to simplify development
#
cat > .merlin <<EOF
S lib
S common
S $arch
S backend
S cfrontend
S driver
S debug
S export
S cparser
S extraction

B lib
B common
B $arch
B backend
B cfrontend
B driver
B debug
B export
B cparser
B extraction
EOF

$make CoqProject

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

expandprefix() {
  echo "$1" | 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 $cc_options
    C preprocessor................ $cprepro $cprepro_options
    Assembler..................... $casm $casm_options
    Assembler supports CFI........ $asm_supports_cfi
    Assembler for runtime lib..... $casmruntime
    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......... $(expandprefix $bindir)
    Runtime library provided...... $has_runtime_lib
    Library files installed in.... $(expandprefix $libdir)
    Man pages installed in........ $(expandprefix $mandir)
    Standard headers provided..... $has_standard_headers
    Standard headers installed in. $(expandprefix $libdir)/include
EOF

if $install_coqdev; then
cat <<EOF
    Coq development installed in.. $(expandprefix $coqdevdir)
EOF
else
cat <<EOF
    Coq development will not be installed
EOF
fi
fi