From cb529a5fc2c760f57db3f2213570044442540992 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 29 Nov 2010 23:44:17 +0100 Subject: Initial packaging --- .gitignore | 1 + debian/changelog | 5 ++ debian/compat | 1 + debian/control | 59 ++++++++++++++ debian/copyright | 26 +++++++ debian/gbp.conf | 2 + debian/libaac-tactics-coq.doc-base.api | 8 ++ debian/libaac-tactics-coq.doc-base.theories | 8 ++ debian/libaac-tactics-coq.docs | 1 + debian/libaac-tactics-coq.install.in | 3 + debian/libaac-tactics-ocaml-dev.install.in | 5 ++ debian/libaac-tactics-ocaml.install.in | 2 + debian/patches/0001-Fix-Makefile-generation.patch | 94 +++++++++++++++++++++++ debian/patches/series | 1 + debian/rules | 25 ++++++ debian/source/format | 1 + debian/source/local-options | 2 + debian/watch | 2 + 18 files changed, 246 insertions(+) create mode 100644 .gitignore create mode 100644 debian/changelog create mode 100644 debian/compat create mode 100644 debian/control create mode 100644 debian/copyright create mode 100644 debian/gbp.conf create mode 100644 debian/libaac-tactics-coq.doc-base.api create mode 100644 debian/libaac-tactics-coq.doc-base.theories create mode 100644 debian/libaac-tactics-coq.docs create mode 100644 debian/libaac-tactics-coq.install.in create mode 100644 debian/libaac-tactics-ocaml-dev.install.in create mode 100644 debian/libaac-tactics-ocaml.install.in create mode 100644 debian/patches/0001-Fix-Makefile-generation.patch create mode 100644 debian/patches/series create mode 100755 debian/rules create mode 100644 debian/source/format create mode 100644 debian/source/local-options create mode 100644 debian/watch 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 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 +Uploaders: Stéphane Glondu +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 +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 +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 +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 +--- + 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 <