diff options
author | Stephane Glondu <steph@glondu.net> | 2010-12-01 11:26:53 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-12-01 13:36:59 +0100 |
commit | ca297726cd05e93f49e69ec798140b2ee77304b3 (patch) | |
tree | 84145dfc90f7bf619a15e17bf6fca3fb9da6f3e3 | |
parent | aa51449cb692a9a1d183b2663679645aba16b036 (diff) |
New upstream release
-rw-r--r-- | debian/changelog | 7 | ||||
-rw-r--r-- | debian/patches/0001-Fix-Makefile-generation.patch | 94 | ||||
-rw-r--r-- | debian/patches/series | 1 |
3 files changed, 7 insertions, 95 deletions
diff --git a/debian/changelog b/debian/changelog index 6359894..06d08a9 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,10 @@ +aac-tactics (0.2.1-1) UNRELEASED; urgency=low + + * New upstream release + - remove patch (applied upstream) + + -- Stéphane Glondu <glondu@debian.org> Wed, 01 Dec 2010 13:36:22 +0100 + aac-tactics (0.1-r13244-1) experimental; urgency=low * Initial release (Closes: #605487) 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") --- diff --git a/debian/patches/series b/debian/patches/series deleted file mode 100644 index 649ecb9..0000000 --- a/debian/patches/series +++ /dev/null @@ -1 +0,0 @@ -0001-Fix-Makefile-generation.patch |