diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | debian/changelog | 12 | ||||
| -rw-r--r-- | debian/compat | 1 | ||||
| -rw-r--r-- | debian/control | 59 | ||||
| -rw-r--r-- | debian/copyright | 26 | ||||
| -rw-r--r-- | debian/gbp.conf | 2 | ||||
| -rw-r--r-- | debian/libaac-tactics-coq.doc-base.api | 8 | ||||
| -rw-r--r-- | debian/libaac-tactics-coq.doc-base.theories | 8 | ||||
| -rw-r--r-- | debian/libaac-tactics-coq.docs | 1 | ||||
| -rw-r--r-- | debian/libaac-tactics-coq.install.in | 3 | ||||
| -rw-r--r-- | debian/libaac-tactics-ocaml-dev.install.in | 5 | ||||
| -rw-r--r-- | debian/libaac-tactics-ocaml.install.in | 2 | ||||
| -rwxr-xr-x | debian/rules | 27 | ||||
| -rw-r--r-- | debian/source/format | 1 | ||||
| -rw-r--r-- | debian/source/local-options | 2 | ||||
| -rw-r--r-- | debian/watch | 3 |
16 files changed, 161 insertions, 0 deletions
@@ -1,2 +1,3 @@ doc html +.pc diff --git a/debian/changelog b/debian/changelog new file mode 100644 index 0000000..06d08a9 --- /dev/null +++ b/debian/changelog @@ -0,0 +1,12 @@ +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) + + -- Stéphane Glondu <glondu@debian.org> Tue, 30 Nov 2010 16:24:53 +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..42cf10a --- /dev/null +++ b/debian/libaac-tactics-coq.install.in @@ -0,0 +1,3 @@ +*.vo /usr/lib/coq/user-contrib/AAC_tactics/ +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..74548b3 --- /dev/null +++ b/debian/libaac-tactics-ocaml-dev.install.in @@ -0,0 +1,5 @@ +*.cmi /usr/lib/coq/user-contrib/AAC_tactics/ +*.mli /usr/lib/coq/user-contrib/AAC_tactics/ +OPT: *.cmx /usr/lib/coq/user-contrib/AAC_tactics/ +OPT: *.cmxa /usr/lib/coq/user-contrib/AAC_tactics/ +OPT: *.a /usr/lib/coq/user-contrib/AAC_tactics/ diff --git a/debian/libaac-tactics-ocaml.install.in b/debian/libaac-tactics-ocaml.install.in new file mode 100644 index 0000000..2ede221 --- /dev/null +++ b/debian/libaac-tactics-ocaml.install.in @@ -0,0 +1,2 @@ +aac_tactics.cma /usr/lib/coq/user-contrib/AAC_tactics/ +DYN: aac_tactics.cmxs /usr/lib/coq/user-contrib/AAC_tactics/ diff --git a/debian/rules b/debian/rules new file mode 100755 index 0000000..a2e1bcb --- /dev/null +++ b/debian/rules @@ -0,0 +1,27 @@ +#!/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 + +.PHONY: override_dh_auto_build +override_dh_auto_build: + $(MAKE) world + +.PHONY: override_dh_auto_install +override_dh_auto_install: +# install rule as generated by coq_makefile is buggy + +.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..2e63b76 --- /dev/null +++ b/debian/watch @@ -0,0 +1,3 @@ +version=3 +opts="uversionmangle=s/-pl/.pl/" \ +http://sardes.inrialpes.fr/~braibant/aac_tactics/ aac_tactics.(.*)\.tgz |