From cb529a5fc2c760f57db3f2213570044442540992 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 29 Nov 2010 23:44:17 +0100
Subject: Initial packaging

---
 debian/patches/0001-Fix-Makefile-generation.patch | 94 +++++++++++++++++++++++
 debian/patches/series                             |  1 +
 2 files changed, 95 insertions(+)
 create mode 100644 debian/patches/0001-Fix-Makefile-generation.patch
 create mode 100644 debian/patches/series

(limited to 'debian/patches')

diff --git a/debian/patches/0001-Fix-Makefile-generation.patch b/debian/patches/0001-Fix-Makefile-generation.patch
new file mode 100644
index 0000000..bf654fe
--- /dev/null
+++ b/debian/patches/0001-Fix-Makefile-generation.patch
@@ -0,0 +1,94 @@
+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")
+-- 
diff --git a/debian/patches/series b/debian/patches/series
new file mode 100644
index 0000000..649ecb9
--- /dev/null
+++ b/debian/patches/series
@@ -0,0 +1 @@
+0001-Fix-Makefile-generation.patch
-- 
cgit v1.2.3