[Pkg-ocaml-maint-commits] r912 - packages/coq-doc/trunk/debian
Samuel Mimram
smimram-guest@costa.debian.org
Wed, 19 Jan 2005 12:51:40 +0100
Author: smimram-guest
Date: 2005-01-19 12:51:39 +0100 (Wed, 19 Jan 2005)
New Revision: 912
Added:
packages/coq-doc/trunk/debian/coq-doc-html.dirs
packages/coq-doc/trunk/debian/coq-doc-html.doc-base.faq
packages/coq-doc/trunk/debian/coq-doc-html.doc-base.library
packages/coq-doc/trunk/debian/coq-doc-html.doc-base.manual
packages/coq-doc/trunk/debian/coq-doc-html.doc-base.tutorial
packages/coq-doc/trunk/debian/coq-doc-html.docs
packages/coq-doc/trunk/debian/coq-doc-ps.dirs
packages/coq-doc/trunk/debian/coq-doc-ps.docs
Removed:
packages/coq-doc/trunk/debian/coq-doc.doc-base.faq
packages/coq-doc/trunk/debian/coq-doc.doc-base.library
packages/coq-doc/trunk/debian/coq-doc.doc-base.manual
packages/coq-doc/trunk/debian/coq-doc.doc-base.tutorial
packages/coq-doc/trunk/debian/docs
Modified:
packages/coq-doc/trunk/debian/changelog
packages/coq-doc/trunk/debian/control
packages/coq-doc/trunk/debian/dirs
packages/coq-doc/trunk/debian/rules
Log:
Split the package in html / ps + going to non-free.
Modified: packages/coq-doc/trunk/debian/changelog
===================================================================
--- packages/coq-doc/trunk/debian/changelog 2005-01-19 11:40:32 UTC (rev 911)
+++ packages/coq-doc/trunk/debian/changelog 2005-01-19 11:51:39 UTC (rev 912)
@@ -1,3 +1,10 @@
+coq-doc (8.0pl1.0-2) unstable; urgency=low
+
+ * Split into -html and -ps, closes: #266019.
+ * Moving to non-free since we don't have the sources for the documentation.
+
+ -- Samuel Mimram <smimram@debian.org> Wed, 5 Jan 2005 19:32:14 +0100
+
coq-doc (8.0pl1.0-1) unstable; urgency=low
* Added the Coq faq, moved the tutorial to the root directory and added
Modified: packages/coq-doc/trunk/debian/control
===================================================================
--- packages/coq-doc/trunk/debian/control 2005-01-19 11:40:32 UTC (rev 911)
+++ packages/coq-doc/trunk/debian/control 2005-01-19 11:51:39 UTC (rev 912)
@@ -1,17 +1,40 @@
Source: coq-doc
-Section: doc
+Section: non-free/doc
Priority: optional
-Maintainer: Samuel Mimram <samuel.mimram@ens-lyon.org>
+Maintainer: Samuel Mimram <smimram@debian.org>
Standards-Version: 3.6.1
Build-Depends-Indep: debhelper (>= 4.0.0)
Package: coq-doc
Architecture: all
-Description: Documentation for Coq
+Depends: coq-doc-html coq-doc-ps
+Description: documentation for Coq in html format
Coq is a proof assistant for higher-order logic, which allows the
development of computer programs consistent with their formal
specification. It is developed using Objective Caml and Camlp4.
For more information, see <http://coq.inria.fr/>.
.
- This package contains its documentation and tutorials in postscript and html
- formats.
+ This is a dummy package which will install the documentation in html and
+ postscript formats.
+
+Package: coq-doc-html
+Architecture: all
+Replaces: coq-doc (<= 8.0pl1.0-1)
+Description: documentation for Coq in html format
+ Coq is a proof assistant for higher-order logic, which allows the
+ development of computer programs consistent with their formal
+ specification. It is developed using Objective Caml and Camlp4.
+ For more information, see <http://coq.inria.fr/>.
+ .
+ This package contains its documentation and tutorials in html format.
+
+Package: coq-doc-ps
+Architecture: all
+Replaces: coq-doc (<= 8.0pl1.0-1)
+Description: documentation for Coq in postscript format
+ Coq is a proof assistant for higher-order logic, which allows the
+ development of computer programs consistent with their formal
+ specification. It is developed using Objective Caml and Camlp4.
+ For more information, see <http://coq.inria.fr/>.
+ .
+ This package contains its documentation and tutorials in postscript format.
Added: packages/coq-doc/trunk/debian/coq-doc-html.dirs
===================================================================
--- packages/coq-doc/trunk/debian/coq-doc-html.dirs 2005-01-19 11:40:32 UTC (rev 911)
+++ packages/coq-doc/trunk/debian/coq-doc-html.dirs 2005-01-19 11:51:39 UTC (rev 912)
@@ -0,0 +1,2 @@
+usr/share/doc/coq
+usr/share/doc/coq-doc-html
Copied: packages/coq-doc/trunk/debian/coq-doc-html.doc-base.faq (from rev 886, packages/coq-doc/trunk/debian/coq-doc.doc-base.faq)
===================================================================
--- packages/coq-doc/trunk/debian/coq-doc.doc-base.faq 2005-01-01 17:26:43 UTC (rev 886)
+++ packages/coq-doc/trunk/debian/coq-doc-html.doc-base.faq 2005-01-19 11:51:39 UTC (rev 912)
@@ -0,0 +1,9 @@
+Document: coq-faq
+Title: Coq Version 8.0 for the Clueless (FAQ)
+Author: Hugo Herbelin, Florent Kirchner, Benjamin Monate, Julien Narboux
+Abstract: This note intends to provide an easy way to get acquainted with the Coq theorem prover. It tries to formulate appropriate answers to some of the questions any newcomers will face, and to give pointers to other references when possible.
+Section: Apps/Math
+
+Format: HTML
+Index: /usr/share/doc/coq-doc-html/faq.html
+Files: /usr/share/doc/coq-doc-html/faq.html
Copied: packages/coq-doc/trunk/debian/coq-doc-html.doc-base.library (from rev 886, packages/coq-doc/trunk/debian/coq-doc.doc-base.library)
===================================================================
--- packages/coq-doc/trunk/debian/coq-doc.doc-base.library 2005-01-01 17:26:43 UTC (rev 886)
+++ packages/coq-doc/trunk/debian/coq-doc-html.doc-base.library 2005-01-19 11:51:39 UTC (rev 912)
@@ -0,0 +1,9 @@
+Document: coq-library
+Title: The Coq Standard Library
+Author: The Coq Development Team
+Abstract: Standard Library documentation of version 8.0 of the Coq proof assistant which is a system designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that programs are correct with respect to their specification.
+Section: Apps/Math
+
+Format: HTML
+Index: /usr/share/doc/coq-doc-html/library/index.html
+Files: /usr/share/doc/coq-doc-html/library/*.html
Copied: packages/coq-doc/trunk/debian/coq-doc-html.doc-base.manual (from rev 886, packages/coq-doc/trunk/debian/coq-doc.doc-base.manual)
===================================================================
--- packages/coq-doc/trunk/debian/coq-doc.doc-base.manual 2005-01-01 17:26:43 UTC (rev 886)
+++ packages/coq-doc/trunk/debian/coq-doc-html.doc-base.manual 2005-01-19 11:51:39 UTC (rev 912)
@@ -0,0 +1,9 @@
+Document: coq-manual
+Title: The Coq Proof Assistant Reference Manual
+Author: The Coq Development Team
+Abstract: Reference Manual of version 8.0 of the Coq proof assistant which is a system designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that programs are correct with respect to their specification.
+Section: Apps/Math
+
+Format: HTML
+Index: /usr/share/doc/coq-doc-html/manual/index.html
+Files: /usr/share/doc/coq-doc-html/manual/*.html
Copied: packages/coq-doc/trunk/debian/coq-doc-html.doc-base.tutorial (from rev 886, packages/coq-doc/trunk/debian/coq-doc.doc-base.tutorial)
===================================================================
--- packages/coq-doc/trunk/debian/coq-doc.doc-base.tutorial 2005-01-01 17:26:43 UTC (rev 886)
+++ packages/coq-doc/trunk/debian/coq-doc-html.doc-base.tutorial 2005-01-19 11:51:39 UTC (rev 912)
@@ -0,0 +1,9 @@
+Document: coq-tutorial
+Title: The Coq Proof Assistant -- A Tutorial
+Author: Gérard Huet, Gilles Kahn and Christine Paulin-Mohring
+Abstract: This documents presents in the most elementary manner a tutorial on the basic specification language of the Coq proof-assistant, called Gallina, in which formal axiomatisations may be developed, and on the main proof tools.
+Section: Apps/Math
+
+Format: HTML
+Index: /usr/share/doc/coq-doc-html/tutorial.html
+Files: /usr/share/doc/coq-doc-html/tutorial.html
Added: packages/coq-doc/trunk/debian/coq-doc-html.docs
===================================================================
--- packages/coq-doc/trunk/debian/coq-doc-html.docs 2005-01-19 11:40:32 UTC (rev 911)
+++ packages/coq-doc/trunk/debian/coq-doc-html.docs 2005-01-19 11:51:39 UTC (rev 912)
@@ -0,0 +1,4 @@
+library
+manual
+tutorial.html
+faq.html
Added: packages/coq-doc/trunk/debian/coq-doc-ps.dirs
===================================================================
--- packages/coq-doc/trunk/debian/coq-doc-ps.dirs 2005-01-19 11:40:32 UTC (rev 911)
+++ packages/coq-doc/trunk/debian/coq-doc-ps.dirs 2005-01-19 11:51:39 UTC (rev 912)
@@ -0,0 +1,2 @@
+usr/share/doc/coq
+usr/share/doc/coq-doc-ps
Added: packages/coq-doc/trunk/debian/coq-doc-ps.docs
===================================================================
--- packages/coq-doc/trunk/debian/coq-doc-ps.docs 2005-01-19 11:40:32 UTC (rev 911)
+++ packages/coq-doc/trunk/debian/coq-doc-ps.docs 2005-01-19 11:51:39 UTC (rev 912)
@@ -0,0 +1,3 @@
+Reference-Manual.ps.gz
+Syntax-v8.ps.gz
+Translator.ps.gz
Deleted: packages/coq-doc/trunk/debian/coq-doc.doc-base.faq
===================================================================
--- packages/coq-doc/trunk/debian/coq-doc.doc-base.faq 2005-01-19 11:40:32 UTC (rev 911)
+++ packages/coq-doc/trunk/debian/coq-doc.doc-base.faq 2005-01-19 11:51:39 UTC (rev 912)
@@ -1,9 +0,0 @@
-Document: coq-faq
-Title: Coq Version 8.0 for the Clueless (FAQ)
-Author: Hugo Herbelin, Florent Kirchner, Benjamin Monate, Julien Narboux
-Abstract: This note intends to provide an easy way to get acquainted with the Coq theorem prover. It tries to formulate appropriate answers to some of the questions any newcomers will face, and to give pointers to other references when possible.
-Section: Apps/Math
-
-Format: HTML
-Index: /usr/share/doc/coq-doc/faq.html
-Files: /usr/share/doc/coq-doc/faq.html
Deleted: packages/coq-doc/trunk/debian/coq-doc.doc-base.library
===================================================================
--- packages/coq-doc/trunk/debian/coq-doc.doc-base.library 2005-01-19 11:40:32 UTC (rev 911)
+++ packages/coq-doc/trunk/debian/coq-doc.doc-base.library 2005-01-19 11:51:39 UTC (rev 912)
@@ -1,9 +0,0 @@
-Document: coq-library
-Title: The Coq Standard Library
-Author: The Coq Development Team
-Abstract: Standard Library documentation of version 8.0 of the Coq proof assistant which is a system designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that programs are correct with respect to their specification.
-Section: Apps/Math
-
-Format: HTML
-Index: /usr/share/doc/coq-doc/library/index.html
-Files: /usr/share/doc/coq-doc/library/*.html
Deleted: packages/coq-doc/trunk/debian/coq-doc.doc-base.manual
===================================================================
--- packages/coq-doc/trunk/debian/coq-doc.doc-base.manual 2005-01-19 11:40:32 UTC (rev 911)
+++ packages/coq-doc/trunk/debian/coq-doc.doc-base.manual 2005-01-19 11:51:39 UTC (rev 912)
@@ -1,9 +0,0 @@
-Document: coq-manual
-Title: The Coq Proof Assistant Reference Manual
-Author: The Coq Development Team
-Abstract: Reference Manual of version 8.0 of the Coq proof assistant which is a system designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that programs are correct with respect to their specification.
-Section: Apps/Math
-
-Format: HTML
-Index: /usr/share/doc/coq-doc/manual/index.html
-Files: /usr/share/doc/coq-doc/manual/*.html
Deleted: packages/coq-doc/trunk/debian/coq-doc.doc-base.tutorial
===================================================================
--- packages/coq-doc/trunk/debian/coq-doc.doc-base.tutorial 2005-01-19 11:40:32 UTC (rev 911)
+++ packages/coq-doc/trunk/debian/coq-doc.doc-base.tutorial 2005-01-19 11:51:39 UTC (rev 912)
@@ -1,9 +0,0 @@
-Document: coq-tutorial
-Title: The Coq Proof Assistant -- A Tutorial
-Author: Gérard Huet, Gilles Kahn and Christine Paulin-Mohring
-Abstract: This documents presents in the most elementary manner a tutorial on the basic specification language of the Coq proof-assistant, called Gallina, in which formal axiomatisations may be developed, and on the main proof tools.
-Section: Apps/Math
-
-Format: HTML
-Index: /usr/share/doc/coq-doc/tutorial.html
-Files: /usr/share/doc/coq-doc/tutorial.html
Modified: packages/coq-doc/trunk/debian/dirs
===================================================================
--- packages/coq-doc/trunk/debian/dirs 2005-01-19 11:40:32 UTC (rev 911)
+++ packages/coq-doc/trunk/debian/dirs 2005-01-19 11:51:39 UTC (rev 912)
@@ -1,2 +1,4 @@
+usr/share/doc/coq
usr/share/doc/coq-doc
-usr/share/doc/coq
+usr/share/doc/coq-doc-ps
+usr/share/doc/coq-doc-html
Deleted: packages/coq-doc/trunk/debian/docs
===================================================================
--- packages/coq-doc/trunk/debian/docs 2005-01-19 11:40:32 UTC (rev 911)
+++ packages/coq-doc/trunk/debian/docs 2005-01-19 11:51:39 UTC (rev 912)
@@ -1,7 +0,0 @@
-library
-manual
-tutorial.html
-faq.html
-Reference-Manual.ps.gz
-Syntax-v8.ps.gz
-Translator.ps.gz
Modified: packages/coq-doc/trunk/debian/rules
===================================================================
--- packages/coq-doc/trunk/debian/rules 2005-01-19 11:40:32 UTC (rev 911)
+++ packages/coq-doc/trunk/debian/rules 2005-01-19 11:51:39 UTC (rev 912)
@@ -4,8 +4,6 @@
# Uncomment this to turn on verbose mode.
#export DH_VERBOSE=1
-PREFIX = debian/coq-doc
-
build:
clean:
@@ -20,8 +18,10 @@
dh_installdirs
dh_installdocs
- cd $(PREFIX)/usr/share/doc/coq-doc/manual; ln -s main.html index.html
- cd $(PREFIX)/usr/share/doc/coq; ln -s ../coq-doc docs
+ cd debian/coq-doc-html/usr/share/doc/coq-doc-html/manual; ln -s main.html index.html
+ cd debian/coq-doc-html/usr/share/doc/coq; ln -s ../coq-doc-html html;
+ cd debian/coq-doc-ps/usr/share/doc/coq; ln -s ../coq-doc-ps ps
+ cd debian/coq-doc/usr/share/doc/coq-doc; ln -s ../coq-doc-html html; ln -s ../coq-doc-ps ps
touch install-stamp