[Pkg-ocaml-maint-commits] [mathcomp] 05/13: Produce the ssreflect packages
Nicolas Braud-Santoni
nicolas at braud-santoni.eu
Sun Jul 24 02:32:28 UTC 2016
This is an automated email from the git hooks/post-receive script.
nicoo-guest pushed a commit to branch v1.6/master
in repository mathcomp.
commit d1f7e6efe138e2f30d68e0cc1ad9c5eb09b26187
Author: Nicolas Braud-Santoni <nicolas at braud-santoni.eu>
Date: Wed Jul 6 15:43:27 2016 +0200
Produce the ssreflect packages
---
debian/control | 73 ++++++++++++++++++++--
debian/libmathcomp-coq.docs | 1 +
debian/libmathcomp-coq.install | 8 ++-
debian/libssreflect-coq.README.Debian | 11 ++++
debian/libssreflect-coq.doc-base | 9 +++
debian/libssreflect-coq.docs | 2 +
debian/libssreflect-coq.examples | 1 +
debian/libssreflect-coq.install | 1 +
debian/libssreflect-ocaml-dev.install | 1 +
debian/libssreflect-ocaml.install | 2 +
...0001-Build-docs-outside-of-a-Git-worktree.patch | 51 +++++++++++++++
debian/patches/series | 1 +
debian/rules | 11 ++--
13 files changed, 160 insertions(+), 12 deletions(-)
diff --git a/debian/control b/debian/control
index 55f3461..8accf41 100644
--- a/debian/control
+++ b/debian/control
@@ -1,11 +1,17 @@
Source: mathcomp
Priority: optional
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint at lists.debian.org>
-Uploaders: Enrico Tassi <gareuselesinge at debian.org>
+Uploaders: Enrico Tassi <gareuselesinge at debian.org>,
+ Stéphane Glondu <glondu at debian.org>
Build-Depends:
debhelper (>= 8),
- coq (>= 8.4),
- libssreflect-coq (>= 1.5)
+ coq (>= 8.5),
+ libcoq-ocaml-dev (>= 8.4),
+ dh-ocaml (>= 0.9~),
+ camlp5 (>= 5.12-2~),
+ lua5.1,
+ ocaml-best-compilers,
+ ocaml-nox (>= 4)
Standards-Version: 3.9.5
Section: math
Homepage: https://math-comp.github.io/math-comp/
@@ -15,10 +21,69 @@ Vcs-Git: https://alioth.debian.org/anonscm/git/pkg-ocaml-maint/packages/mathcomp
Package: libmathcomp-coq
Architecture: all
Depends:
- libssreflect-coq (>= 1.5), libssreflect-coq (<< 1.6),
+ libssreflect-coq (>= 1.6),
coq-${F:CoqABI},
${misc:Depends}
Description: Mathematical Components library for Coq (theories)
The Mathematical Components library is an extensive library of
formalized mathematics built using the Ssreflect extension for
the Coq system.
+
+Package: libssreflect-ocaml
+Section: ocaml
+Architecture: any
+Depends:
+ ${ocaml:Depends},
+ ${shlibs:Depends},
+ ${misc:Depends}
+Enhances: coq
+Provides: ${ocaml:Provides}
+Description: small scale reflection extension for Coq (plugin)
+ This package is part of Ssreflect, the small scale reflection
+ extension for Coq. It provides a new tactic language, which promotes
+ more structured, concise and robust proof scripts, and is in fact
+ independent from the "reflection" proof style. It is implemented as a
+ linkable extension to the Coq system.
+
+Package: libssreflect-ocaml-dev
+Section: ocaml
+Architecture: any
+Depends:
+ ${ocaml:Depends},
+ ${shlibs:Depends},
+ ${misc:Depends}
+Replaces: libssreflect-ocaml (<< 1.2+dfsg-3~)
+Breaks: libssreflect-ocaml (<< 1.2+dfsg-3~)
+Provides: ${ocaml:Provides}
+Description: small scale reflection extension for Coq (devt files)
+ This package is part of Ssreflect, the small scale reflection
+ extension for Coq. It provides the static native-code library, needed
+ to build custom toplevels, and the compiled interface.
+
+Package: libssreflect-coq
+Architecture: all
+Depends:
+ libssreflect-ocaml (>= ${source:Version}),
+ coq-${F:CoqABI},
+ ${misc:Depends}
+Provides: ssreflect
+Description: small scale reflection library for Coq (theories)
+ The name Ssreflect stands for "small scale reflection", a style of
+ proof that evolved from the computer-checked proof of the Four Colour
+ Theorem and which leverages the higher-order nature of Coq's
+ underlying logic to provide effective automation for many small,
+ clerical proof steps. This is often accomplished by restating
+ ("reflecting") problems in a more concrete form, hence the name. For
+ example, in the Ssreflect library, arithmetic comparison is not an
+ abstract predicate, but a function computing a boolean.
+ .
+ The Ssreflect distribution comprises two parts:
+ * A new tactic language, which promotes more structured, concise and
+ robust proof scripts, and is in fact independent from the "reflection"
+ proof style. It is implemented as a linkable extension to the Coq
+ system.
+ * A set of Coq libraries that provide core "reflection-oriented"
+ theories for basic combinatorics (roughly: arithmetic, lists, and
+ finite sets).
+ .
+ This package installs the full Ssreflect distribution.
diff --git a/debian/libmathcomp-coq.docs b/debian/libmathcomp-coq.docs
new file mode 120000
index 0000000..71e9d16
--- /dev/null
+++ b/debian/libmathcomp-coq.docs
@@ -0,0 +1 @@
+libssreflect-coq.docs
\ No newline at end of file
diff --git a/debian/libmathcomp-coq.install b/debian/libmathcomp-coq.install
index a04983f..64757be 100644
--- a/debian/libmathcomp-coq.install
+++ b/debian/libmathcomp-coq.install
@@ -1,2 +1,6 @@
- usr/lib/coq/user-contrib/MathComp/*.vo
-html usr/share/doc/libmathcomp-coq
+ usr/lib/coq/user-contrib/mathcomp/algebra/*.vo
+ usr/lib/coq/user-contrib/mathcomp/character/*.vo
+ usr/lib/coq/user-contrib/mathcomp/field/*.vo
+ usr/lib/coq/user-contrib/mathcomp/fingroup/*.vo
+ usr/lib/coq/user-contrib/mathcomp/solvable/*.vo
+htmldoc usr/share/doc/libmathcomp-coq
diff --git a/debian/libssreflect-coq.README.Debian b/debian/libssreflect-coq.README.Debian
new file mode 100644
index 0000000..224010c
--- /dev/null
+++ b/debian/libssreflect-coq.README.Debian
@@ -0,0 +1,11 @@
+Ssreflect for Debian
+====================
+
+This package doesn't provide the ssrcoq binary as built originally by
+upstream (but relies on dynamic linking instead), nor the PDF
+documentation (which is available online, see README).
+
+You can use Ssreflect directly with the regular Coq tools. For
+compatibility, a symlink to coqtop named "ssrcoq" is provided.
+
+ -- Stéphane Glondu <glondu at debian.org>, Tue, 1 Sep 2009 15:08:28 +0200
diff --git a/debian/libssreflect-coq.doc-base b/debian/libssreflect-coq.doc-base
new file mode 100644
index 0000000..6c49640
--- /dev/null
+++ b/debian/libssreflect-coq.doc-base
@@ -0,0 +1,9 @@
+Document: ssreflect-library
+Title: The Ssreflect Library
+Author: The Ssreflect Development Team
+Abstract: This is the coqdoc-generated documentation for Ssreflect
+Section: Science/Mathematics
+
+Format: HTML
+Index: /usr/share/doc/libssreflect-coq/html/index.html
+Files: /usr/share/doc/libssreflect-coq/html/*.html
diff --git a/debian/libssreflect-coq.docs b/debian/libssreflect-coq.docs
new file mode 100644
index 0000000..7cdad11
--- /dev/null
+++ b/debian/libssreflect-coq.docs
@@ -0,0 +1,2 @@
+etc/ANNOUNCE-1.6.md
+README
diff --git a/debian/libssreflect-coq.examples b/debian/libssreflect-coq.examples
new file mode 100644
index 0000000..6b59762
--- /dev/null
+++ b/debian/libssreflect-coq.examples
@@ -0,0 +1 @@
+mathcomp/ssreflect/pg-ssr.el
diff --git a/debian/libssreflect-coq.install b/debian/libssreflect-coq.install
new file mode 100644
index 0000000..2b68c39
--- /dev/null
+++ b/debian/libssreflect-coq.install
@@ -0,0 +1 @@
+usr/lib/coq/user-contrib/mathcomp/ssreflect/*.vo
diff --git a/debian/libssreflect-ocaml-dev.install b/debian/libssreflect-ocaml-dev.install
new file mode 100644
index 0000000..ca56461
--- /dev/null
+++ b/debian/libssreflect-ocaml-dev.install
@@ -0,0 +1 @@
+usr/lib/coq/user-contrib/mathcomp/ss*.cmi
diff --git a/debian/libssreflect-ocaml.install b/debian/libssreflect-ocaml.install
new file mode 100644
index 0000000..b0fbd6b
--- /dev/null
+++ b/debian/libssreflect-ocaml.install
@@ -0,0 +1,2 @@
+usr/lib/coq/user-contrib/mathcomp/ss*.cma
+usr/lib/coq/user-contrib/mathcomp/ss*.cmxs
diff --git a/debian/patches/0001-Build-docs-outside-of-a-Git-worktree.patch b/debian/patches/0001-Build-docs-outside-of-a-Git-worktree.patch
new file mode 100644
index 0000000..98e6c14
--- /dev/null
+++ b/debian/patches/0001-Build-docs-outside-of-a-Git-worktree.patch
@@ -0,0 +1,51 @@
+From: Nicolas Braud-Santoni <nicolas at braud-santoni.eu>
+Date: Tue, 12 Jul 2016 23:43:21 +0200
+Subject: Build docs outside of a Git worktree
+
+---
+ htmldoc/Makefile | 31 +++++++++----------------------
+ 1 file changed, 9 insertions(+), 22 deletions(-)
+
+diff --git a/htmldoc/Makefile b/htmldoc/Makefile
+index 5386dca..f300e3c 100644
+--- a/htmldoc/Makefile
++++ b/htmldoc/Makefile
+@@ -4,29 +4,16 @@ ifeq "$(COQBIN)" ""
+ COQBIN=$(dir $(shell which coqtop))/
+ endif
+
+-SRC=$(shell cd ../mathcomp; ls */*.v | grep -v ssrtest/ | grep -v attic/)
+-HEAD=$(shell git symbolic-ref HEAD)
+-ifeq "$(HEAD)" "refs/heads/master"
+-LAST=$(shell git tag -l --sort=v:refname "mathcomp-*" | tail -n 1)
+-RELEASED=$(shell git show $(LAST):mathcomp/Make | grep 'v *$$' | cut -d / -f 2 | cut -d . -f 1)
+-endif
++SRC=$(shell cd ../mathcomp; ls */*.v)
++RELEASED=$(shell grep 'v *$$' ../mathcomp/Make | cut -d / -f 2 | cut -d . -f 1)
+
+ all:
+- $(H) git diff-index --quiet HEAD ||\
+- (echo error: uncommitted files; exit 1)
+- $(H) cd ../mathcomp;\
+- $(COQBIN)/coqdep -R . mathcomp $(SRC) 2>/dev/null |\
+- grep -v vio: > ../htmldoc/depend
+- $(H) cat depend | ./buildlibgraph cytoscape $(RELEASED) > depend.js
+- $(H) . ../etc/utils/builddoc_lib.sh; \
+- cd ../mathcomp; mangle_sources $(SRC)
+- $(H) make -C ../mathcomp clean
+- $(H) make -C ../mathcomp -j2
+- $(H) cd ../mathcomp; $(COQBIN)/coqdoc -t "Mathematical Components"\
+- -g --utf8 -R . mathcomp \
+- --parse-comments \
++ $(H) cd ../mathcomp; $(COQBIN)/coqdep -R . mathcomp $(SRC) | \
++ grep -v 'vio:' > ../htmldoc/depends
++ ./buildlibgraph cytoscape $(RELEASED) < depend > depend.js
++ $(H) cd ../mathcomp; $(COQBIN)/coqdoc \
++ -t "Mathematical Components" \
++ -g --utf8 -R . mathcomp \
++ --parse-comments \
+ --multi-index $(SRC) -d ../htmldoc/
+ $(H) cp ../etc/artwork/coqdoc.css .
+- $(H) cd ../mathcomp; git checkout $(SRC)
+-
+-
diff --git a/debian/patches/series b/debian/patches/series
new file mode 100644
index 0000000..81035e7
--- /dev/null
+++ b/debian/patches/series
@@ -0,0 +1 @@
+0001-Build-docs-outside-of-a-Git-worktree.patch
diff --git a/debian/rules b/debian/rules
index 9c54e7c..4624c68 100755
--- a/debian/rules
+++ b/debian/rules
@@ -15,15 +15,14 @@ INSTALL_DIR := $(CURDIR)/debian/tmp/usr/lib/coq/user-contrib/MathComp
.PHONY: override_dh_auto_build
override_dh_auto_build:
- $(MAKE) -j2
- $(MAKE) -f Makefile.coq html
+ . ./etc/utils/builddoc_lib.sh; mangle_sources mathcomp/*/*.v
+ $(MAKE) -C mathcomp -j2
+ $(MAKE) -C htmldoc
.PHONY: override_dh_auto_install
override_dh_auto_install:
- $(MAKE) install DSTROOT=$(CURDIR)/debian/tmp
-
-.PHONY: override_dh_install
-override_dh_install:
+ $(MAKE) -C mathcomp install DSTROOT=$(CURDIR)/debian/tmp
+ find . -type f \( -name '*.glob' -or -name '*.v' \) -delete
dh_install --fail-missing
.PHONY: override_dh_clean
--
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/mathcomp.git
More information about the Pkg-ocaml-maint-commits
mailing list