Initial packaging

18 files changed, 246 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..845ca06
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+.pc
diff --git a/debian/changelog b/debian/changelog
new file mode 100644
index 0000000..05bdfa9
--- /dev/null
+++ b/debian/changelog
@@ -0,0 +1,5 @@
+aac-tactics (0.1-r13244-1) UNRELEASED; urgency=low
+
+  * Initial release
+
+ -- Stéphane Glondu <glondu@debian.org>  Mon, 29 Nov 2010 23:32:43 +0100
diff --git a/debian/compat b/debian/compat
new file mode 100644
index 0000000..45a4fb7
--- /dev/null
+++ b/debian/compat
@@ -0,0 +1 @@
+8
diff --git a/debian/control b/debian/control
new file mode 100644
index 0000000..bca697c
--- /dev/null
+++ b/debian/control
@@ -0,0 +1,59 @@
+Source: aac-tactics
+Section: math
+Priority: optional
+Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
+Uploaders: Stéphane Glondu <glondu@debian.org>
+Build-Depends:
+ debhelper (>= 8),
+ dh-ocaml (>= 0.9~),
+ ocaml-nox (>= 3.11.1-3~),
+ coq (>= 8.3),
+ libcoq-ocaml-dev
+Standards-Version: 3.9.1
+Homepage: http://sardes.inrialpes.fr/~braibant/aac_tactics/
+Vcs-Browser: http://git.debian.org/?p=pkg-ocaml-maint/packages/coq-aactactics.git
+Vcs-Git: git://git.debian.org/git/pkg-ocaml-maint/packages/coq-aactactics.git
+
+Package: libaac-tactics-ocaml
+Section: ocaml
+Architecture: any
+Depends:
+ ${ocaml:Depends},
+ ${shlibs:Depends},
+ ${misc:Depends}
+Recommends: libaac-tactics-coq
+Enhances: coq
+Provides: ${ocaml:Provides}
+Description: Coq tactics for reasoning modulo AC (plugin)
+ This Coq plugin provides tactics for rewriting universally quantified
+ equations, modulo associative (and possibly commutative) operators.
+ .
+ This package provides the plugin itself.
+
+Package: libaac-tactics-ocaml-dev
+Section: ocaml
+Architecture: any
+Depends:
+ ${ocaml:Depends},
+ ${shlibs:Depends},
+ ${misc:Depends}
+Provides: ${ocaml:Provides}
+Description: Coq tactics for reasoning modulo AC (devt files)
+ This Coq plugin provides tactics for rewriting universally quantified
+ equations, modulo associative (and possibly commutative) operators.
+ .
+ This package provides the static native-code library, needed to build
+ custom toplevels, and the compiled interfaces.
+
+Package: libaac-tactics-coq
+Architecture: all
+Depends:
+ libaac-tactics-ocaml (>= ${source:Version}),
+ coq-${F:CoqABI},
+ ${misc:Depends}
+Provides: aac-tactics
+Description: Coq tactics for reasoning modulo AC (theories)
+ This Coq plugin provides tactics for rewriting universally quantified
+ equations, modulo associative (and possibly commutative) operators.
+ .
+ This package provides the Coq support library.
diff --git a/debian/copyright b/debian/copyright
new file mode 100644
index 0000000..daeda79
--- /dev/null
+++ b/debian/copyright
@@ -0,0 +1,26 @@
+Packaged-By: Stéphane Glondu <glondu@debian.org>
+Packaged-Date: Mon, 29 Nov 2010 23:40:57 +0100
+Upstream-Author: Thomas Braibant, Damien Pous
+Original-Source-Location: http://sardes.inrialpes.fr/~braibant/aac_tactics/
+
+Files: *
+Copyright: © 2009-2010 Thomas Braibant, Damien Pous
+License: LGPL-3+
+
+  The aac_tactics plugin library is free software: you can
+  redistribute it and/or modify it under the terms of the GNU Lesser
+  General Public License as published by the Free Software Foundation,
+  either version 3 of the License, or (at your option) any later
+  version.
+
+  This library is distributed in the hope that it will be useful, but
+  WITHOUT ANY WARRANTY; without even the implied warranty of
+  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+  Lesser General Public License for more details.
+
+  On Debian systems, the complete text of the GNU Lesser General
+  Public License can be found in `/usr/share/common-licenses/LGPL-3'.
+
+Files: debian/*
+Copyright: © 2010 Stéphane Glondu <steph@glondu.net>
+License: LGPL-3+
diff --git a/debian/gbp.conf b/debian/gbp.conf
new file mode 100644
index 0000000..cec628c
--- /dev/null
+++ b/debian/gbp.conf
@@ -0,0 +1,2 @@
+[DEFAULT]
+pristine-tar = True
diff --git a/debian/libaac-tactics-coq.doc-base.api b/debian/libaac-tactics-coq.doc-base.api
new file mode 100644
index 0000000..97c229f
--- /dev/null
+++ b/debian/libaac-tactics-coq.doc-base.api
@@ -0,0 +1,8 @@
+Document: aac-tactics-api-reference
+Title: aac_tactics API Reference
+Abstract: API reference for aac_tactics (generated from ML sources via OCamldoc)
+Section: Programming/OCaml
+
+Format: HTML
+Index: /usr/share/doc/libaac-tactics-coq/api/index.html
+Files: /usr/share/doc/libaac-tactics-coq/api/*
diff --git a/debian/libaac-tactics-coq.doc-base.theories b/debian/libaac-tactics-coq.doc-base.theories
new file mode 100644
index 0000000..de3a8e5
--- /dev/null
+++ b/debian/libaac-tactics-coq.doc-base.theories
@@ -0,0 +1,8 @@
+Document: aac-tactics-theories
+Title: aac_tactics theories
+Abstract: Theories for aac_tactics (generated from .v sources via coqdoc)
+Section: Science/Mathematics
+
+Format: HTML
+Index: /usr/share/doc/libaac-tactics-coq/theories/index.html
+Files: /usr/share/doc/libaac-tactics-coq/theories/*
diff --git a/debian/libaac-tactics-coq.docs b/debian/libaac-tactics-coq.docs
new file mode 100644
index 0000000..71dfd5b
--- /dev/null
+++ b/debian/libaac-tactics-coq.docs
@@ -0,0 +1 @@
+README.txt
diff --git a/debian/libaac-tactics-coq.install.in b/debian/libaac-tactics-coq.install.in
new file mode 100644
index 0000000..4302629
--- /dev/null
+++ b/debian/libaac-tactics-coq.install.in
@@ -0,0 +1,3 @@
+*.vo                      /usr/lib/coq/user-contrib/AACTactics/
+doc/*                     /usr/share/doc/libaac-tactics-coq/api
+html/*                    /usr/share/doc/libaac-tactics-coq/theories
diff --git a/debian/libaac-tactics-ocaml-dev.install.in b/debian/libaac-tactics-ocaml-dev.install.in
new file mode 100644
index 0000000..d360db0
--- /dev/null
+++ b/debian/libaac-tactics-ocaml-dev.install.in
@@ -0,0 +1,5 @@
+*.cmi                     /usr/lib/coq/user-contrib/AACTactics/
+*.mli                     /usr/lib/coq/user-contrib/AACTactics/
+OPT: *.cmx                /usr/lib/coq/user-contrib/AACTactics/
+OPT: *.cmxa               /usr/lib/coq/user-contrib/AACTactics/
+OPT: *.a                  /usr/lib/coq/user-contrib/AACTactics/
diff --git a/debian/libaac-tactics-ocaml.install.in b/debian/libaac-tactics-ocaml.install.in
new file mode 100644
index 0000000..55dd22c
--- /dev/null
+++ b/debian/libaac-tactics-ocaml.install.in
@@ -0,0 +1,2 @@
+aac_tactics.cma           /usr/lib/coq/user-contrib/AACTactics/
+DYN: aac_tactics.cmxs     /usr/lib/coq/user-contrib/AACTactics/
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
diff --git a/debian/rules b/debian/rules
new file mode 100755
index 0000000..446d604
--- /dev/null
+++ b/debian/rules
@@ -0,0 +1,25 @@
+#!/usr/bin/make -f
+# -*- makefile -*-
+
+include /usr/share/coq/coqvars.mk
+
+%:
+	dh $@ --with ocaml
+
+.PHONY: override_dh_auto_configure
+override_dh_auto_configure:
+	./make_makefile
+# workaround bug on fs mounted without relatime
+	touch make_makefile theory.ml
+
+.PHONY: override_dh_auto_build
+override_dh_auto_build:
+	$(MAKE) world
+
+.PHONY: override_dh_gencontrol
+override_dh_gencontrol:
+	dh_gencontrol -- -VF:CoqABI="$(COQ_ABI)"
+
+.PHONY: override_dh_auto_clean
+override_dh_auto_clean:
+	rm -Rf Makefile .depend *.glob *.d *.*o *.*a *.cm* doc html
diff --git a/debian/source/format b/debian/source/format
new file mode 100644
index 0000000..163aaf8
--- /dev/null
+++ b/debian/source/format
@@ -0,0 +1 @@
+3.0 (quilt)
diff --git a/debian/source/local-options b/debian/source/local-options
new file mode 100644
index 0000000..c4cf480
--- /dev/null
+++ b/debian/source/local-options
@@ -0,0 +1,2 @@
+abort-on-upstream-changes
+unapply-patches
diff --git a/debian/watch b/debian/watch
new file mode 100644
index 0000000..6ea59f3
--- /dev/null
+++ b/debian/watch
@@ -0,0 +1,2 @@
+version=3
+http://sardes.inrialpes.fr/~braibant/aac_tactics/ aac_tactics.(.*)\.tgz