From 547d8ecb50541db1e80bb23d065e55046a27452e Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 4 Apr 2012 13:59:24 +0000
Subject: Configuration, build and install for cchecklink.  Clean-ups in
 myocamlbuild.ml.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1874 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 Makefile        |  8 +++++++-
 configure       | 21 +++++++++++++++++++--
 myocamlbuild.ml |  2 +-
 3 files changed, 27 insertions(+), 4 deletions(-)

diff --git a/Makefile b/Makefile
index 00f8571..2c2825c 100644
--- a/Makefile
+++ b/Makefile
@@ -133,6 +133,9 @@ all:
 	$(MAKE) extraction
 	$(MAKE) ccomp
 	$(MAKE) runtime
+ifeq ($(CCHECKLINK),true)
+	$(MAKE) cchecklink
+endif
 
 documentation: doc/coq2html $(FILES)
 	mkdir -p doc/html
@@ -186,11 +189,14 @@ depend: $(FILES)
 install:
 	install -d $(BINDIR)
 	install ./ccomp $(BINDIR)
+ifeq ($(CCHECKLINK),true)
+	install ./cchecklink $(BINDIR)
+endif
 	$(MAKE) -C runtime install
 
 clean:
 	rm -f $(patsubst %, %/*.vo, $(DIRS))
-	rm -f ccomp ccomp.byte
+	rm -f ccomp ccomp.byte cchecklink cchecklink.byte
 	rm -rf _build
 	rm -rf doc/html doc/*.glob
 	rm -f doc/coq2html.ml doc/coq2html
diff --git a/configure b/configure
index 73dbd03..455f58b 100755
--- a/configure
+++ b/configure
@@ -61,6 +61,8 @@ done
 
 # Per-target configuration
 
+cchecklink=false
+
 case "$target" in
   powerpc-macosx|ppc-macosx)
     arch="powerpc"
@@ -81,7 +83,8 @@ case "$target" in
     casm="${toolprefix}gcc -c"
     clinker="${toolprefix}gcc"
     libmath="-lm"
-    need_stdlib_wrapper="false";;
+    need_stdlib_wrapper="false"
+    cchecklink=true;;
   powerpc-eabi-diab|ppc-eabi-diab)
     arch="powerpc"
     variant="eabi"
@@ -91,7 +94,8 @@ case "$target" in
     casm="${toolprefix}das"
     clinker="${toolprefix}dcc"
     libmath="-lm"
-    need_stdlib_wrapper="false";;
+    need_stdlib_wrapper="false"
+    cchecklink=true;;
   arm-linux)
     arch="arm"
     variant="linux"
@@ -154,6 +158,17 @@ case "$target" in
     exit 2;;
 esac
 
+# Additional packages needed for cchecklink
+
+if $cchecklink; then
+  if ocamlfind query bitstring > /dev/null
+  then :
+  else 
+    echo "ocamlfind or ocaml-bitstring missing, cchecklink will not be built"
+    cchecklink=false
+  fi
+fi
+
 # Generate Makefile.config
 
 rm -f Makefile.config
@@ -174,6 +189,7 @@ CASM=$casm
 CLINKER=$clinker
 LIBMATH=$libmath
 NEED_STDLIB_WRAPPER=$need_stdlib_wrapper
+CCHECKLINK=$cchecklink
 EOF
 else
 cat >> Makefile.config <<'EOF'
@@ -256,6 +272,7 @@ CompCert configuration:
     Needs wrapper around stdlib... $need_stdlib_wrapper
     Binaries installed in......... $bindirexp
     Library files installed in.... $libdirexp
+    cchecklink tool supported..... $cchecklink
 
 If anything above looks wrong, please edit file ./Makefile.config to correct.
 
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index c1b3ca8..0e51489 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -16,7 +16,7 @@ dispatch begin function
     (* ocamlfind libraries *)
     flag ["ocaml"; "link"; "pkg_unix"] & S[A"-package"; A "unix"];
     flag ["ocaml"; "link"; "pkg_str"] & S[A"-package"; A "str"];
-    flag ["ocaml"; "compile";  "pkg_bitstring"] & S[A"-package"; A"bitstring,bitstring.syntax"; A"-syntax"; A"bitstring.syntax"; A"-syntax"; A"camlp4o"];
+    flag ["ocaml"; "compile";  "pkg_bitstring"] & S[A"-package"; A"bitstring,bitstring.syntax"; A"-syntax"; A"bitstring.syntax,camlp4o"];
     flag ["ocaml"; "ocamldep";  "pkg_bitstring"] & S[A"-package"; A"bitstring,bitstring.syntax"; A"-syntax"; A"bitstring.syntax,camlp4o"];
     flag ["ocaml"; "link";  "pkg_bitstring"] & S[A"-package"; A"bitstring"]
 
-- 
cgit v1.2.3