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, 0 insertions, 94 deletions
diff --git a/debian/patches/0001-Fix-Makefile-generation.patch b/debian/patches/0001-Fix-Makefile-generation.patch deleted file mode 100644 index bf654fe..0000000 --- a/debian/patches/0001-Fix-Makefile-generation.patch +++ /dev/null @@ -1,94 +0,0 @@ -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") --- |