Reorganized the development, modularizing away machine-dependent parts.

Started to merge the ARM code generator.
Started to add support for PowerPC/EABI.
Use ocamlbuild to construct executable from Caml files.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 91 insertions, 6 deletions

diff --git a/configure b/configure
index bd1b7bb..0d71d27 100755
--- a/configure
+++ b/configure
@@ -16,6 +16,22 @@ cildistrib=cil-1.3.5.tar.gz
 prefix=/usr/local
 bindir='$(PREFIX)/bin'
 libdir='$(PREFIX)/lib/compcert'
+target=''
+
+usage='Usage: ./configure [options] <target>
+
+Supported targets:
+  macosx           (PowerPC, MacOS X)
+  ppc-linux        (PowerPC, Linux)
+  ppc-linux-cross  (PowerPC, Linux, cross-compilation)
+  arm-linux        (ARM, Linux)
+  arm-linux-cross  (ARM, Linux, cross-compilation)
+
+Options:
+  -prefix <dir>    Install in <dir>/bin and <dir>/lib/compcert
+  -bindir <dir>    Install binaries in <dir>
+  -libdir <dir>    Install libraries in <dir>
+'
 
 # Parse command-line arguments
 
@@ -28,11 +44,64 @@ while : ; do
         bindir=$2; shift;;
     -libdir|--libdir)
         libdir=$2; shift;;
-    *) echo "Unknown option \"$1\"." 1>&2; exit 2;;
+    *)
+        if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi
+        target="$1";;
   esac
   shift
 done
 
+if test -z "$target"; then echo "$usage" 1>&2; exit 2; fi
+
+# Per-target configuration
+
+case "$target" in
+  macosx)
+    arch="powerpc"
+    variant="macosx"
+    cc="gcc -arch ppc"
+    cprepro="gcc -arch ppc -U__GNUC__ -E"
+    casm="gcc -arch ppc -c"
+    clinker="gcc -arch ppc"
+    libmath="";;
+  ppc-linux)
+    arch="powerpc"
+    variant="eabi"
+    cc="gcc"
+    cprepro="gcc -U__GNUC__ -E"
+    casm="gcc -c"
+    clinker="gcc"
+    libmath="-lm";;
+  ppc-linux-cross)
+    arch="powerpc"
+    variant="eabi"
+    cc="ppc-linux-gcc"
+    cprepro="ppc-linux-gcc -U__GNUC__ -E"
+    casm="ppc-linux-gcc -c"
+    clinker="ppc-linux-gcc"
+    libmath="-lm";;
+  arm-linux)
+    arch="arm"
+    variant="linux"
+    cc="gcc"
+    cprepro="gcc -U__GNUC__ -E"
+    casm="gcc -c"
+    clinker="gcc"
+    libmath="-lm";;
+  arm-linux-cross)
+    arch="arm"
+    variant="linux"
+    cc="arm-linux-gcc"
+    cprepro="arm-linux-gcc -U__GNUC__ -E"
+    casm="arm-linux-gcc -c"
+    clinker="arm-linux-gcc"
+    libmath="-lm";;
+  *)
+    echo "Unsupported configuration '$target'" 1>&2
+    echo "$usage" 1>&2
+    exit 2;;
+esac
+
 # Generate Makefile.config
 
 rm -f Makefile.config
@@ -40,11 +109,13 @@ cat > Makefile.config <<EOF
 PREFIX=$prefix
 BINDIR=$bindir
 LIBDIR=$libdir
-CC=gcc -arch ppc
-CPREPRO=gcc -arch ppc -U__GNUC__ -E
-CASM=gcc -arch ppc -c
-CLINKER=gcc -arch ppc
-LIBMATH=
+ARCH=$arch
+VARIANT=$variant
+CC=$cc
+CPREPRO=$cprepro
+CASM=$casm
+CLINKER=$clinker
+LIBMATH=$libmath
 EOF
 
 # Extract and configure Cil
@@ -57,3 +128,17 @@ for i in cil.patch/*; do patch -p1 < $i; done
 # Extract 'ARCHOS' info from Cil configuration
 
 grep '^ARCHOS=' cil/config.log >> Makefile.config
+
+# Summarize configuration
+
+cat <<EOF
+
+CompCert configuration:
+    Target architecture........... $arch ($variant)
+    C compiler.................... $cc
+    C preprocessor................ $cprepro
+    Assembler..................... $casm
+    Linker........................ $clinker
+    Math library.................. $libmath
+
+EOF
\ No newline at end of file