From: Stephane Glondu <steph@glondu.net>
Date: Mon, 29 Nov 2010 23:52:39 +0100
Subject: [PATCH] Fix Makefile generation

 * add "#!" header to make_makefile
 * add "-R . AACTactics" option to coq_makefile, and adapt theory.ml
 * add custom rule for aac_tactics.cmxa
 * fix Makefile rule
 * fix build on bytecode/non-natdynlink architectures
 * workaround Coq bug #2444

Signed-off-by: Stephane Glondu <steph@glondu.net>
---
 magic.txt     |    1 +
 make_makefile |   22 ++++++++++++++++++----
 theory.ml     |    2 +-
 3 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/magic.txt b/magic.txt
index d0272c3..1b17df7 100644
--- a/magic.txt
+++ b/magic.txt
@@ -1,4 +1,5 @@
 -custom "mkdir -p doc; $(CAMLBIN)ocamldoc -html -rectypes -d doc -m A $(ZDEBUG) $(ZFLAGS) $^ && touch doc" "$(MLIFILES)" doc
 -custom "$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -linkall -o aac_tactics.cmxs $(CMXFILES)" "$(CMXFILES)" aac_tactics.cmxs 
 -custom "$(CAMLLINK) -g -a -o aac_tactics.cma $(CMOFILES)" "$(CMOFILES)" aac_tactics.cma
+-custom "$(CAMLOPTLINK) -g -a -o aac_tactics.cmxa $(CMXFILES)" "$(CMXFILES)" aac_tactics.cmxa
 -custom "$(CAMLBIN)ocamldep -slash $(OCAMLLIBS) $^ > .depend" "$(MLIFILES)" .depend
diff --git a/make_makefile b/make_makefile
index 3cfc096..44b47f1 100755
--- a/make_makefile
+++ b/make_makefile
@@ -1,3 +1,4 @@
+#!/bin/sh
 # - set variable MLIFILES so that it can be used in custom targets to
 #   build documentation and dependencies for .mli files
 # - remove useless ' -I . .../plugins/ ' lines so that we can read something in the compilation log
@@ -5,9 +6,22 @@
 # - patch the rule for cleaning doc
 # - include the .depend custom target, to take .mli dependencies into account
 
+set -e
+
+if [ -f `ocamlc -where`/dynlink.cmxa ]; then
+    BEST=opt
+    CMXA=aac_tactics.cmxa
+    CMXS=aac_tactics.cmxs
+else
+    BEST=byte
+    if which ocamlopt >/dev/null; then
+        CMXA=aac_tactics.cmxa
+    fi
+fi
+
 (
-coq_makefile -no-install -opt MLIFILES = '$(MLFILES:.ml=.mli)' $(cat files.txt) -f magic.txt \
-    | sed 's|.*/plugins/.*||g;s|Makefile:|\.dummy:|g;s|rm -f doc|rm -rf doc|g'
+coq_makefile -R . AACTactics -no-install -$BEST MLIFILES = '$(MLFILES:.ml=.mli)' $(cat files.txt) -f magic.txt \
+    | sed 's|.*/plugins/.*||g;s|Makefile:|\.dummy:|g;s|rm -f doc|rm -rf doc|g;s|\.opt||g'
 cat <<EOF
 
 # sanity checks
@@ -15,7 +29,7 @@ tests: Tests.vo
 
 # override inadequate coq_makefile auto-regeneration
 Makefile: make_makefile magic.txt files.txt
-	. make_makefile
+	./make_makefile
 
 # We want to keep the proofs only in the Tutorial
 tutorial: Tutorial.vo Tutorial.glob
@@ -28,7 +42,7 @@ world: \$(VOFILES) doc gallinahtml tutorial
 # ignores this dependency)
 # (one can safely select one of theses dependencies according to 
 #  coq' compilation mode--bytecode or native)
-AAC.vo: aac_tactics.cmxs aac_tactics.cma
+AAC.vo: $CMXA $CMXS aac_tactics.cma
 
 
 # .depend contains dependencies for .mli files
diff --git a/theory.ml b/theory.ml
index 45a76f1..f2041da 100644
--- a/theory.ml
+++ b/theory.ml
@@ -16,7 +16,7 @@
 
 open Term
 
-let ac_theory_path = ["AAC"]
+let ac_theory_path = ["AACTactics"; "AAC"]
 
 module Sigma = struct
   let sigma = lazy (Coq.init_constant ac_theory_path "sigma")
--