diff options
Diffstat (limited to 'debian/patches/0001-Fix-Makefile-generation.patch')
| -rw-r--r-- | debian/patches/0001-Fix-Makefile-generation.patch | 94 |
1 files changed, 94 insertions, 0 deletions
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") +-- |