diff options
-rw-r--r-- | .gitignore | 1 | ||||
-rw-r--r-- | debian/changelog | 5 | ||||
-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 | ||||
-rw-r--r-- | debian/patches/0001-Fix-Makefile-generation.patch | 94 | ||||
-rw-r--r-- | debian/patches/series | 1 | ||||
-rwxr-xr-x | debian/rules | 25 | ||||
-rw-r--r-- | debian/source/format | 1 | ||||
-rw-r--r-- | debian/source/local-options | 2 | ||||
-rw-r--r-- | debian/watch | 2 |
18 files changed, 246 insertions, 0 deletions
@@ -1,2 +1,3 @@ doc html +.pc diff --git a/debian/changelog b/debian/changelog new file mode 100644 index 0000000..6359894 --- /dev/null +++ b/debian/changelog @@ -0,0 +1,5 @@ +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..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 |