diff options
Diffstat (limited to 'debian')
33 files changed, 2065 insertions, 0 deletions
diff --git a/debian/README.Debian b/debian/README.Debian new file mode 100644 index 00000000..685f6047 --- /dev/null +++ b/debian/README.Debian @@ -0,0 +1,42 @@ +-------------------------- ++ Coq package for Debian + +-------------------------- + +Binary (in)compatibility +------------------------ +The compiled libraries of Coq (the *.vo) are not expected to be backward or +upward compatible between releases (including plX releases). In case of a new +upstream release, your Coq files should be recompiled. + + +Coq frontends +------------- +For interactive use of coqtop, we suggest +- either the Debian cle package +- or the Proof-General (x)emacs mode, which unfortunately can not be +distributed by Debian for copyright reasons. However, a Debian package +might become available at proof general home page in the future +(http://zermelo.dcs.ed.ac.uk/~proofgen) + +However we recommand you to use the CoqIde gtk interface provided in coqide. + + +Unstripped binaries +------------------- + +Note that all bytecode files in this package need to be left +'unstripped' after compiling. The reason is the following: + + It is possible to strip the .out corresponding to ocaml code compiled in + native code (and it is done in Coq (coqopt.out) When compiling in + byte-code, the Coq system uses the -custom option in order to get an + autonomous executable (running independently of an ocaml implementation on + your computer). The way it works is that the .out file is composed of the + executable of the byte-code interpreter plus the byte-code for your own + program which is stored in the symbol table zone... stripping such an + executable, just remove your byte-code and consequentely cannot run + properly. + +Moreover the bytecode version is installed even on platforms having a +native version as the dynamic loading of tactics works only with the +bytecode version. diff --git a/debian/TODO.Debian b/debian/TODO.Debian new file mode 100644 index 00000000..5cba552e --- /dev/null +++ b/debian/TODO.Debian @@ -0,0 +1,4 @@ +* Move the coqide stuff from /usr/lib/coq/ide to /usr/share/coqide. The variable + lib_ide should be changed to do that. + +* Remove the .byte files on native archs. diff --git a/debian/changelog b/debian/changelog new file mode 100644 index 00000000..afb42a67 --- /dev/null +++ b/debian/changelog @@ -0,0 +1,255 @@ +coq (8.0pl3-2) unstable; urgency=low + + * Added coq-8.0pl3-ocaml-3.09.dpatch in order to prevent intuition from + looping forever, closes: #353493. + + -- Samuel Mimram <smimram@debian.org> Sun, 19 Feb 2006 11:33:21 +0000 + +coq (8.0pl3-1) unstable; urgency=low + + * New upstream release. + * Removed unnecessary dependency on liblablgtk2-ocaml for coqide. + * Removed ocaml309.dpatch and text_view_typing_error.dpatch, integrated + upstream. + * Removing rpath from coqide binaries. + + -- Samuel Mimram <smimram@debian.org> Thu, 19 Jan 2006 22:22:39 +0100 + +coq (8.0pl2-4) unstable; urgency=low + + * Added ocaml309.dpatch patch to compile cleanly with OCaml 3.09, + closes: #340185. + * Removed recommends on coq-doc which is not in main anymore. + * Updated standards version to 3.6.2, no changes needed. + + -- Samuel Mimram <smimram@debian.org> Mon, 21 Nov 2005 19:52:53 +0100 + +coq (8.0pl2-3) unstable; urgency=low + + * Added text_view_typing_error patch to avoid a typing error and solve the + FTBFS, closes: #326740. + * Added forgotten call to dh_installmenu. + + -- Samuel Mimram <smimram@debian.org> Wed, 7 Sep 2005 21:26:36 +0200 + +coq (8.0pl2-2) unstable; urgency=medium + + * Rebuilding with OCaml 3.08.3 is necessary because of the former dependency + on ocaml-base-nox-3.08. + * Removed the dependency on ocaml-base-nox-3.08 since ocamlrun does not seem + to be necessary, even on non-native archs. + * Cleaner handling of -arch and -indep targets. + * Added utf8.v in coq and utf8.vo to coq-libs since utf8 can be useful for + non-coqide users too. + * Using dh_desktop to register .desktop files. + + -- Samuel Mimram <smimram@debian.org> Tue, 22 Mar 2005 17:40:08 +0100 + +coq (8.0pl2-1) unstable; urgency=low + + * New upstream release. + * Put the libraries in arch all since they are supposed to be + arch-independant. + * Updated the README.Debian to explain that .vo are not compatible between + different upstream releases. + * Renamed coq.desktop into coqide.desktop, updated it and put it in + /usr/share/applications/ to be compliant with the policy. + * Description synopsis now begin with lowercase letters. + * Updated Standards-Version to 3.6.1.1. + + -- Samuel Mimram <smimram@debian.org> Mon, 31 Jan 2005 13:25:06 +0100 + +coq (8.0pl1-5) unstable; urgency=low + + * Reuploaded since powerpc .deb did not include native code executable + + -- Stefano Zacchiroli <zack@debian.org> Mon, 13 Dec 2004 16:05:18 +0100 + +coq (8.0pl1-4) unstable; urgency=low + + * Rebuilt against ocaml 3.08.2 + + -- Stefano Zacchiroli <zack@debian.org> Tue, 30 Nov 2004 21:38:21 +0100 + +coq (8.0pl1-3) unstable; urgency=high + + * Small patch to be able to compile with ocaml 3.08.1. + * Added a dependency to ocaml-base-nox when coq is compiled in bytecode. + * Added a menu for coqide. + * Enhanced the manpages. + * Enhanced the short descriptions of the packages. + + -- Samuel Mimram <samuel.mimram@ens-lyon.org> Tue, 17 Aug 2004 20:54:25 +0200 + +coq (8.0pl1-2) unstable; urgency=medium + + * Changed section to math. + * Versionned the dependency to liblablgtk2-ocaml(-dev). + * If we fallback on bytecode, we also try to build coqide in bytecode (I hope + this will fix the FTBFS on alpha). + * Added a watch file. + * Removed the unnecessary patch an unpatch targets in the rules. + + -- Samuel Mimram <samuel.mimram@ens-lyon.org> Mon, 16 Aug 2004 20:39:48 +0200 + +coq (8.0pl1-1) unstable; urgency=low + + * New upstream release: finally the version without QPL-licensed files is out, + closes: #230356, #250497. + * Libraries are now in separate packages (coq-libs and coq7-libs). + * An additional package provides coqide. + * Built with OCaml 3.08. + * Thank you Martin Ellis and Julien Cristau for your help on this package. + + -- Samuel Mimram <samuel.mimram@ens-lyon.org> Sun, 18 Jul 2004 01:10:24 +0200 + +coq (7.3.1-3) unstable; urgency=low + + * Added build-dependency on ocaml-best-compilers, check for opt compilers + in the configure-stamp target of debian/rules. Thanks to Mike Furr for + the patch (closes: #242761). + * Converted changelog to UTF-8. + + -- Ralf Treinen <treinen@debian.org> Fri, 9 Apr 2004 18:03:41 +0200 + +coq (7.3.1-2) unstable; urgency=low + + * Standards-Version 3.6.1. + * File debian/compat instead of variable DH_COMPAT. + * Build with ocaml-3.07. + * Maintainers: debian-ocaml-maint, Uploaders: The Ocaml Gang. + * Switch to dpatch system: + - 01_ocaml307: patch by Hugo Herbelin (thanks!) for compilation with + ocaml 3.07. + * Removed timeout crutch which used to be necessary for ocaml 3.04. + * Removed forcing of byte compilation on ppc. + * debian/rules: some cosmetic changes. + * Short description: capitalize first letter, drop terminal dot. + + -- Ralf Treinen <treinen@debian.org> Tue, 7 Oct 2003 22:11:31 +0200 + +coq (7.3.1-1) unstable; urgency=low + + * New bugfix upstream version. + * Proof General is now Recommended since he has been freed (closes: + Bug#162894). + + -- Judicael Courant <Judicael.Courant@lri.fr> Mon, 7 Oct 2002 12:34:03 +0200 + +coq (7.3-1) unstable; urgency=low + + * New upstream version. + + -- Judicael Courant <Judicael.Courant@lri.fr> Wed, 22 May 2002 14:48:21 +0200 + +coq (7.2-9) unstable; urgency=low + * ocamlc.opt completely broken on powerpc. Added a special case in + "rules" for using only bytecode. + + -- Judicael Courant <Judicael.Courant@lri.fr> Fri, 15 Feb 2002 09:17:20 +0100 + +coq (7.2-8) unstable; urgency=low + + * "timeout" time is now 5300s (< 90 min). + + -- Judicael Courant <Judicael.Courant@lri.fr> Thu, 14 Feb 2002 17:38:06 +0100 + +coq (7.2-7) unstable; urgency=low + + * Build now uses ocamlc.opt and ocamlopt.opt if available. + * Dependency forced on ocaml >= 3.04 (dependency ocaml >=3.04 | camlp4 + does not make buildd happy. See http://buildd.debian.org/fetch.php? + &pkg=coq&ver=7.2-5&arch=arm&stamp=1013388706&file=log&as=raw). + + -- Judicael Courant <Judicael.Courant@lri.fr> Tue, 12 Feb 2002 09:10:01 +0100 + +coq (7.2-6) unstable; urgency=low + + * Typo in rules, which made the build process always build in + bytecode. Fixed. + + -- Judicael Courant <Judicael.Courant@lri.fr> Mon, 11 Feb 2002 11:22:21 +0100 + +coq (7.2-5) unstable; urgency=low + + * Pb with timeout, used in 7.2-4 (bug 132927) making the build process + fail when compilation in native mode fails. Workaround in rules: after + a "timeout ... make ..." we try a "make -q" to check that everything + has been done correctly. + + -- Judicael Courant <Judicael.Courant@lri.fr> Fri, 8 Feb 2002 10:08:10 +0100 + +coq (7.2-4) unstable; urgency=low + * Native code compilation failed on sparc; coqtop built by ocamlopt + entered an infinite loop on powerpc. Fixed (using timeout for powerpc: + if coqtop loops, it is rebuild using the bytecode compiler) + + -- Judicael Courant <Judicael.Courant@lri.fr> Fri, 1 Feb 2002 11:04:25 +0100 + +coq (7.2-3) unstable; urgency=low + * Workaround for problems with buildd/apt trying to install camlp4 + (closes: Bug#130046). + + -- Judicaël Courant <Judicael.Courant@lri.fr> Mon, 21 Jan 2002 09:46:16 +0100 + +coq (7.2-2) unstable; urgency=low + + * Build-Depends now requires camlp4 instead of camlp4 (>=3.01) since + camlp4 is a virtual package provided by ocaml >=3.04. + + -- Judicaël Courant <Judicael.Courant@lri.fr> Fri, 11 Jan 2002 11:08:03 +0100 + +coq (7.2-1) unstable; urgency=low + * New upstream version. + + -- Judicaël Courant <Judicael.Courant@lri.fr> Wed, 9 Jan 2002 14:02:42 +0100 + +coq (7.1-2) unstable; urgency=low + + * Fixed policy problem (conf files). + * Trying to compile in bytecode if native code compilation fails + (closes: Bug#119714) + * Errors raised by the Simpl tactic is an upstream bug and should + have been fixed in 7.0 (closes: Bug#74518). + + -- Judicaël Courant <Judicael.Courant@lri.fr> Tue, 11 Dec 2001 13:33:15 +0100 + +coq (7.1-1) unstable; urgency=low + * New upstream version. + + -- Judicaël Courant <Judicael.Courant@lri.fr> Tue, 25 Sep 2001 16:27:04 +0200 + +coq (7.0-1) unstable; urgency=low + * New maintainer Judicaël Courant <Judicael.Courant@lri.fr>. + * New upstream version. + * Added Build-Depends (closes: Bug#70273). + * Cleaned up dependencies. + * Emacs mode installation now follows Emacs policy. + * Made compilation non-interactive (closes: Bug#92461). + * Added Suggests cle. + + + -- Judicaël Courant <Judicael.Courant@lri.fr> Tue, 17 Apr 2001 19:24:34 +0200 + +coq (6.3.1-3) unstable; urgency=low + + * Patched to allow use of ocaml3. + + -- Fernando Sanchez <fer@debian.org> Fri, 7 Jul 2000 08:05:47 +0200 + +coq (6.3.1-2) unstable; urgency=low + + * Some changes to allow successful porting of this package: + * Added checking for ocamlopt.opt before running ./configure with -opt, + and configure without it if it is not present for this architecture. + * Added checking for ocamlopt before making world-opt. + + -- Fernando Sanchez <fer@debian.org> Sat, 18 Dec 1999 16:45:01 +0100 + +coq (6.3.1-1) unstable; urgency=low + + * Initial Release. + + -- Fernando Sanchez <fer@debian.org> Fri, 3 Dec 1999 22:06:04 +0100 + + diff --git a/debian/compat b/debian/compat new file mode 100644 index 00000000..b8626c4c --- /dev/null +++ b/debian/compat @@ -0,0 +1 @@ +4 diff --git a/debian/control b/debian/control new file mode 100644 index 00000000..9ec22d2f --- /dev/null +++ b/debian/control @@ -0,0 +1,65 @@ +Source: coq +Section: math +Priority: optional +Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org> +Uploaders: Ralf Treinen <treinen@debian.org>, Sven Luther <luther@debian.org>, Remi Vanicat <vanicat@debian.org>, Stefano Zacchiroli <zack@debian.org>, Samuel Mimram <smimram@debian.org> +Standards-Version: 3.6.2 +Build-Depends: debhelper (>= 4.0.0), dpatch, ocaml-nox (>= 3.09.0), ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0), chrpath + +Package: coq +Architecture: any +Depends: ${shlibs:Depends}, coq-libs (= ${Source-Version}) +Recommends: coqide | proofgeneral-coq +Suggests: ocaml-nox (>= 3.08), proofgeneral-coq, ledit, cle +Description: proof assistant for higher-order logic (toplevel and compiler) + 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 packages provides coqtop, a command line interface to Coq. + . + A graphical interface for Coq is provided in the coqide package. + Coq can also be used with ProofGeneral, which allows proofs to be + edited using emacs and xemacs. This requires the proofgeneral-coq + package to be installed. + +Package: coqide +Architecture: any +Depends: ${shlibs:Depends}, coq (>= 8.0) +Description: proof assistant for higher-order logic (gtk interface) + 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 provides CoqIde, a graphical user interface for + developing proofs. + +Package: coq-libs +Architecture: all +Recommends: coq (>= 8.0) +Conflicts: coq (<< 8.0) +Description: proof assistant for higher-order logic (theories) + 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 provides existing theories that new proofs can be + based upon, including theories of arithmetic and Boolean values. + +Package: coq7-libs +Architecture: all +Recommends: coq (>= 8.0) +Description: proof assistant for higher-order logic (Coq 7 theories) + 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 provides existing theories from Coq 7 in Coq 8, and + allows proofs that were developed in Coq 7 to be used in Coq 8. + It is also required to translate theories in Coq 7 syntax into + the new syntax introduced in Coq 8. However, this package does + not need to be installed to use Coq 7. diff --git a/debian/copyright b/debian/copyright new file mode 100644 index 00000000..c53b8733 --- /dev/null +++ b/debian/copyright @@ -0,0 +1,47 @@ +This package was debianized by Fernando Sanchez <fer@debian.org> + +It was downloaded from + +ftp://ftp.inria.fr/INRIA/LogiCal/coq/current + +The Coq proof assistant V7 and V8 includes software developed by the +Coq development team inside the LogiCal project, at INRIA, CNRS and +University Paris Sud. + +Copyright 1999-2005 The Coq development team, +INRIA-CNRS, University Paris Sud, All rights reserved. + +This product includes also software developed by + Yves Bertot, Lemme, INRIA Sophia-Antipolis (contrib/interface, + parsing/search.ml) + Pierre Crégut, France Telecom R & D (contrib/omega and contrib/romega) + Pierre Courtieu, Lemme (contrib/funind) + Loïc Pottier, Lemme, INRIA Sophia-Antipolis (contrib/fourier) + Claudio Sacerdoti Coen, HELM, University of Bologna (contrib/xml) + +Coq includes a tactic Jp based on JProver, a theorem prover for +first-order intuitionistic logic. Jprover was originally implemented +by Stephan Schmitt and then integrated into MetaPRL by Aleksey +Nogin. After this, Huang extracted the necessary ML-codes from MetaPRL +and then integrated it into Coq. + +The Coq development Team (march 2004) + Bruno Barras (INRIA) + Pierre Corbineau (Université Paris Sud) + Jean-Christophe Filliâtre (CNRS) + Hugo Herbelin (INRIA) + Pierre Letouzey (Université Paris Sud) + Claude Marché (Université Paris Sud-INRIA) + Christine Paulin (Université Paris Sud) + Clément Renard (INRIA) + +The complete list of developpers and contributors can be found in +/usr/share/doc/doc/CREDITS.gz + +Copyright: the Coq Proof Assistant is distributed under the terms of the GNU +Lesser General Public Licence, version 2.1, see +/usr/share/common-licenses/LGPL-2.1. + +However there are two exceptions: files in the directories contrib/jprover and +ide/utils are distributed under the terms of the GNU General Public Licence, +see /usr/share/common-licenses/GPL. diff --git a/debian/coq-interface.1 b/debian/coq-interface.1 new file mode 100644 index 00000000..73e6eaa6 --- /dev/null +++ b/debian/coq-interface.1 @@ -0,0 +1,154 @@ +.TH COQ 1 "April 25, 2001" + +.SH NAME +coq-interface \- + + +.SH SYNOPSIS +.B coq-interface +[ +.B options +] + +.SH DESCRIPTION + +.B coq-interface +is a Coq customized toplevel system for Coq containing some modules +useful for the graphical interface. This program is not for the casual +user. + +.SH OPTIONS + +.TP +.B \-h +Help. Will give you the complete list of options accepted by +coq-interface (the same as coqtop). +.BI \-I\ dir ,\ \-include\ dir +Add directory dir in the include path. +.TP +.BI \-R\ dir\ coqdir +Recursively map physical +.I dir +to logical +.IR coqdir . +.TP +.B \-src +Add source directories in the include path. +.TP +.BI \-is\ f ,\ \-inputstate\ f +Read state from +.IR f .coq. +.TP +.B \-nois +Start with an empty state. +.TP +.BI \-outputstate\ f +Write state in file +.IR f .coq. +.TP +.BI \-load\-ml\-object\ f +Load ML object file +.IR f . +.TP +.BI \-load\-ml\-source\ f +Load ML file +.IR f . +.TP +.BI \-l\ f ,\ \-load\-vernac\-source\ f +Load Coq file +.IR f .v +(Load +.IR f .). +.TP +.BI \-lv\ f ,\ \-load\-vernac\-source\-verbose\ f +Load Coq file +.IR f .v +(Load Verbose +.IR f .). +.TP +.BI \-load\-vernac\-object\ f +Load Coq object file +.IR f .vo. +.TP +.BI \-require\ f +Load Coq object file +.IR f .vo +and import it (Require +.IR f .). +.TP +.BI \-compile\ f +Compile Coq file +.IR f .v +(implies +.BR \-batch ). +.TP +.BI \-compile\-verbose\ f +Verbosely compile Coq file +.IR f .v +(implies +.BR -batch ). +.TP +.B \-opt +Run the native-code version of Coq or Coq_SearchIsos. +.TP +.B \-byte +Run the bytecode version of Coq or Coq_SearchIsos. +.TP +.B \-where +Print Coq's standard library location and exit. +.TP +.B -v +Print Coq version and exit. +.TP +.B \-q +Skip loading of rcfile. +.TP +.BI \-init\-file\ f +Set the rcfile to +.IR f . +.TP +.BI \-user\ u +Use the rcfile of user +.IR u . +.TP +.B \-batch +Batch mode (exits just after arguments parsing). +.TP +.B \-boot +Boot mode (implies +.B \-q +and +.BR \-batch ). +.TP +.B \-emacs +Tells Coq it is executed under Emacs. +.TP +.BI \-dump\-glob\ f +Dump globalizations in file +.I f +(to be used by +.BR coqdoc (1)). +.TP +.B \-impredicative\-set +Set sort Set impredicative. +.TP +.B \-dont\-load\-proofs +Don't load opaque proofs in memory. +.TP +.B \-xml +Export XML files either to the hierarchy rooted in +the directory +.B COQ_XML_LIBRARY_ROOT +(if set) or to stdout (if unset). + +.SH SEE ALSO + +.BR coqc (1), +.BR coqdep (1), +.BR coqtop (1), +.BR parser (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr diff --git a/debian/coq-libs.install b/debian/coq-libs.install new file mode 100644 index 00000000..c721f0c8 --- /dev/null +++ b/debian/coq-libs.install @@ -0,0 +1,4 @@ +usr/lib/coq/contrib +usr/lib/coq/states +usr/lib/coq/theories +usr/lib/coq/ide/utf8.vo usr/lib/coq diff --git a/debian/coq.dirs b/debian/coq.dirs new file mode 100644 index 00000000..1166b157 --- /dev/null +++ b/debian/coq.dirs @@ -0,0 +1,5 @@ +usr/bin +usr/lib +usr/lib/coq +usr/share/man/man1 +usr/share/pixmaps diff --git a/debian/coq.docs b/debian/coq.docs new file mode 100644 index 00000000..9b2bbcd7 --- /dev/null +++ b/debian/coq.docs @@ -0,0 +1 @@ +ide/utf8.v diff --git a/debian/coq.emacsen-install b/debian/coq.emacsen-install new file mode 100644 index 00000000..1ed8fe43 --- /dev/null +++ b/debian/coq.emacsen-install @@ -0,0 +1,45 @@ +#! /bin/sh -e +# /usr/lib/emacsen-common/packages/install/coq + +# Written by Jim Van Zandt <jrv@vanzandt.mv.com>, borrowing heavily +# from the install scripts for gettext by Santiago Vila +# <sanvila@ctv.es> and octave by Dirk Eddelbuettel <edd@debian.org>. + +FLAVOR=$1 +PACKAGE=coq + +if [ ${FLAVOR} = emacs ]; then exit 0; fi + +echo install/${PACKAGE}: Handling install for emacsen flavor ${FLAVOR} + +#FLAVORTEST=`echo $FLAVOR | cut -c-6` +#if [ ${FLAVORTEST} = xemacs ] ; then +# SITEFLAG="-no-site-file" +#else +# SITEFLAG="--no-site-file" +#fi +FLAGS="${SITEFLAG} -q -batch -l path.el -f batch-byte-compile" + +ELDIR=/usr/share/emacs/site-lisp/${PACKAGE} +ELCDIR=/usr/share/${FLAVOR}/site-lisp/${PACKAGE} + +# Install-info-altdir does not actually exist. +# Maybe somebody will write it. +if test -x /usr/sbin/install-info-altdir; then + echo install/${PACKAGE}: install Info links for ${FLAVOR} + install-info-altdir --quiet --section "" "" --dirname=${FLAVOR} /usr/info/${PACKAGE}.info.gz +fi + +install -m 755 -d ${ELCDIR} +cd ${ELDIR} +FILES=`echo *.el` +cp ${FILES} ${ELCDIR} +cd ${ELCDIR} + +cat << EOF > path.el +(setq load-path (cons "." load-path) byte-compile-warnings nil) +EOF +${FLAVOR} ${FLAGS} ${FILES} +rm -f *.el path.el + +exit 0 diff --git a/debian/coq.emacsen-remove b/debian/coq.emacsen-remove new file mode 100644 index 00000000..02b6392c --- /dev/null +++ b/debian/coq.emacsen-remove @@ -0,0 +1,15 @@ +#!/bin/sh -e +# /usr/lib/emacsen-common/packages/remove/coq + +FLAVOR=$1 +PACKAGE=coq + +if [ ${FLAVOR} != emacs ]; then + if test -x /usr/sbin/install-info-altdir; then + echo remove/${PACKAGE}: removing Info links for ${FLAVOR} + install-info-altdir --quiet --remove --dirname=${FLAVOR} /usr/info/coq.info.gz + fi + + echo remove/${PACKAGE}: purging byte-compiled files for ${FLAVOR} + rm -rf /usr/share/${FLAVOR}/site-lisp/${PACKAGE} +fi diff --git a/debian/coq.emacsen-startup b/debian/coq.emacsen-startup new file mode 100644 index 00000000..91b56915 --- /dev/null +++ b/debian/coq.emacsen-startup @@ -0,0 +1,21 @@ +;; -*-emacs-lisp-*- +;; +;; Emacs startup file for the Debian GNU/Linux coq package +;; +;; Originally contributed by Nils Naumann <naumann@unileoben.ac.at> +;; Modified by Dirk Eddelbuettel <edd@debian.org> +;; Adapted for dh-make by Jim Van Zandt <jrv@vanzandt.mv.com> + +;; The coq package follows the Debian/GNU Linux 'emacsen' policy and +;; byte-compiles its elisp files for each 'emacs flavor' (emacs19, +;; xemacs19, emacs20, xemacs20...). The compiled code is then +;; installed in a subdirectory of the respective site-lisp directory. +;; We have to add this to the load-path: + +(setq load-path (cons (concat "/usr/share/" + (symbol-name flavor) + "/site-lisp/coq") load-path)) + +(setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) +(autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t) + diff --git a/debian/coq.install b/debian/coq.install new file mode 100644 index 00000000..d1182ab6 --- /dev/null +++ b/debian/coq.install @@ -0,0 +1,15 @@ +usr/bin/coqc +usr/bin/coqdep +usr/bin/coqdoc +usr/bin/coq-interface* +usr/bin/coq_makefile +usr/bin/coqmktop +usr/bin/coq-tex +usr/bin/coqtop* +usr/bin/coqwc +usr/bin/gallina +usr/share/emacs/site-lisp/coq +usr/share/emacs/site-lisp/coqdoc.sty +usr/share/man/man1/c* +usr/share/man/man1/gallina.1 +usr/share/texmf/tex/latex/misc/* diff --git a/debian/coq.menu b/debian/coq.menu new file mode 100644 index 00000000..0a1e30f7 --- /dev/null +++ b/debian/coq.menu @@ -0,0 +1,4 @@ +?package(coq):command="/usr/bin/coqtop" \ + icon="/usr/share/pixmaps/coq.xpm" \ + needs="text" \ + section="Apps/Math" title="Coq" diff --git a/debian/coq.xpm b/debian/coq.xpm new file mode 100644 index 00000000..e58ebad7 --- /dev/null +++ b/debian/coq.xpm @@ -0,0 +1,54 @@ +/* XPM */ +static char *coq[] = { +/* columns rows colors chars-per-pixel */ +"32 32 16 1", +" c #220C08", +". c #342A2C", +"X c #5A261F", +"o c #6A4D4B", +"O c #923827", +"+ c #BF381C", +"@ c #996252", +"# c #837671", +"$ c #D35E3A", +"% c #CA7852", +"& c #E19667", +"* c #A59082", +"= c #B9ADA8", +"- c #EAB48F", +"; c #F2D3B6", +": c #FCFDF9", +/* pixels */ +"::::::::::::::::::::::::::::::::", +"::::::::::::::::::::::::::::::::", +":::::X.:::::::::::::::::::::::::", +"::::++-==:::::::::::::::::::::::", +":::+;;+$:*::::::::::::::::::::::", +":::;-++%:: :::::::::::::::::::::", +":::*+++#:::;::::::::::::::::::::", +"::::= +O::::::::::::::::::::::::", +":::::: :::::o:::::::::::::::::::", +"::::::=;:::::=::::::::::::::*:::", +"::::::;::::::::: :::::::::::=:::", +":::::=:::::::::::::::::: :::.:::", +":::::*:::::::::::::.::.::::;X:::", +":::::;::::::::::::::o:::;:-*.:::", +"::::*;;;::::::;;:;-::--:;&&&X:::", +"::::#;;;;-;;::;;;;;-;;--%%-%::::", +":::::--;;@;;;;;-;-;--%oO%&% ::::", +":::::.--;-@%&--&&%$$OOXO%%@:::::", +"::::::o&--& O+XO&& XXX Oo ::::::", +"::::::;@%%&%$ XX$X X Oo@ ::::::", +"::::::::=O$OO+XX O X OO@ :::::::", +"::::::::::;+X O%OOOOOOOo::::::::", +"::::::::::::oOOXXX X ::::::::::", +":::::::::::::XX X X::::::::::::", +":::::::::::::: .:::::::::::::", +":::::::::::::: o:.::::::::::::::", +":::::::::::::: #:.::::::::::::::", +":::::::::::-oX%oo&*:::::::::::::", +"::::::::::::o.#:::=@::::::::::::", +"::::::::::::::::::::::::::::::::", +"::::::::::::::::::::::::::::::::", +"::::::::::::::::::::::::::::::::" +}; diff --git a/debian/coq7-libs.install b/debian/coq7-libs.install new file mode 100644 index 00000000..e888a17f --- /dev/null +++ b/debian/coq7-libs.install @@ -0,0 +1,3 @@ +usr/lib/coq/contrib7 +usr/lib/coq/states7 +usr/lib/coq/theories7 diff --git a/debian/coq_makefile.1 b/debian/coq_makefile.1 new file mode 100644 index 00000000..7890fde1 --- /dev/null +++ b/debian/coq_makefile.1 @@ -0,0 +1,96 @@ +.TH COQ 1 "April 25, 2001" + +.SH NAME +coq_makefile \- The Coq Proof Assistant makefile generator + + +.SH SYNOPSIS +.B coq_makefile +[ +.B options +] +[ +.I subdirectory +] +[ +.I file.v +] +[ +.I file.ml +] + +.SH DESCRIPTION + +.B coq_makefile +is a makefile generator for Coq proof developments. + +.SH OPTIONS + +.TP +.I subdirectory +Subdirectory that should be "made". +.TP +.I file.v +Coq file to be compiled. +.TP +.I file.ml +ML file to be compiled. +.TP +.B \-h,\ \-\-help +Will give you a description of the whole list of options of +.BR coq_makefile . +.TP +.BI \-custom\ command\ dependencies\ file +Add target +.I file +with command +.I command +and dependencies +.I dependencies. +.TP +.BI \-I dir +Look for dependencies in +.IR dir . +.TP +.BI \-R\ physicalpath\ logicalpath +Look for dependencies recursively starting from. +.IR physicalpath . +The logical path associated to the physical path is +.IR logicalpath . +.TP +.IB VARIABLE\ =\ value +Add the variable definition "VARIABLE=value". +.TP +.B \-byte +Compile with byte-code version of +.BR coq (1). +.TP +.B \-opt +Compile with native-code version of +.BR coq (1). +.TP +.B \-impredicative\-set +Compile with option +.B \-impredicative\-set +of +.BR coq (1). +.TP +.B +.BI \-f\ file +Take the contents of file as arguments. +.TP +.BI \-o\ file +Output should go in file +.IR file . + + +.SH SEE ALSO + +.BR coqtop (1), +.BR coqtc (1), +.BR coqdep (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr diff --git a/debian/coqc.1 b/debian/coqc.1 new file mode 100644 index 00000000..baa04a88 --- /dev/null +++ b/debian/coqc.1 @@ -0,0 +1,172 @@ +.TH COQ 1 "April 25, 2001" + +.SH NAME +coqc \- The Coq Proof Assistant compiler + + +.SH SYNOPSIS +.B coqc +[ +.B general \ Coq \ options +] +.I file + + +.SH DESCRIPTION + +.B coqc +is the batch compiler for the Coq Proof Assistant. +The options are basically the same as coqtop(1). +.IR file.v \& +is the vernacular file to compile. +.IR file \& +must be formed +only with the characters `a` to `Z`, `0`-`9` or `_` and must begin +with a letter. +The compiler produces an object file +.IR file.vo \&. + +For interactive use of Coq, see +.BR coqtop(1). + + +.SH OPTIONS + +.TP +.BI \-h +Show the whole list of options of coqc and coqtop. +.TP +.B \-verbose +Compile verbosely. +.TP +.BI \-image\ f +Specify an alternative executable for Coq. +.TP +.B \-t +Keep temporary files. +.TP +.BI \-I\ dir ,\ \-include\ dir +Add directory dir in the include path. +.TP +.BI \-R\ dir\ coqdir +Recursively map physical dir to logical coqdir. +.TP +.B \-src +Add source directories in the include path. +.TP +.BI \-is\ f ,\ \-inputstate\ f +Read state from file +.IR f .coq. +.TP +.B \-nois +Start with an empty state. +.TP +.BI \-outputstate\ f +Write state in file +.IR f .coq. +.TP +.BR \-load\-ml\-object\ f +Load ML object file +.IR f . +.TP +.BI \-load\-ml\-source\ f +Load ML file +.IR f . +.TP +.BI \-l\ f ,\ \-load\-vernac\-source\ f +Load Coq file +.IR f .v +(Load +.IR f .). +.TP +.BI \-lv\ f ,\ \-load\-vernac\-source\-verbose\ f +Load Coq file +.IR f .v +(Load Verbose +.IR f .). +.TP +.BI \-load\-vernac\-object\ f +Load Coq object file +.IR f .vo. +.TP +.BI \-require\ f +Load Coq object file +.IR f .vo +and import it (Require +.IR f .). +.TP +.BI \-compile\ f +Compile Coq file +.IR f .v +(implies +.BR \-batch ). +.TP +.BI \-compile\-verbose\ f +Verbosely compile Coq file +.IR f .v +(implies +.BR \-batch ). +.TP +.B \-opt +Run the native-code version of Coq or Coq_SearchIsos. +.TP +.B \-byte +Run the bytecode version of Coq or Coq_SearchIsos. +.TP +.B \-where +Print Coq's standard library location and exit. +.TP +.B \-v +Print Coq version and exit. +.TP +.B \-q +Skip loading of rcfile. +.TP +.BI \-init\-file\ f +Set the rcfile to +.IR f . +.TP +.BI \-user\ u +Use the rcfile of user +.IR u . +.TP +.B \-batch +Batch mode (exits just after arguments parsing). +.TP +.B \-boot +Boot mode (implies +.B \-q +and +.BR \-batch ). +.TP +.B \-emacs +Tells Coq it is executed under Emacs. +.TP +.BI \-dump\-glob\ f +Dump globalizations in file +.I f +(to be used by +.BR coqdoc (1)). +.TP +.B \-impredicative\-set +Set sort Set impredicative. +.TP +.B \-dont\-load\-proofs +Don't load opaque proofs in memory. +.TP +.B \-xml +Export XML files either to the hierarchy rooted in +the directory +.B COQ_XML_LIBRARY_ROOT +(if set) or to stdout (if unset). + +.SH SEE ALSO + +.BR coqtop (1), +.BR coq_makefile (1), +.BR coqdep (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr diff --git a/debian/coqide.1 b/debian/coqide.1 new file mode 100644 index 00000000..20379ef4 --- /dev/null +++ b/debian/coqide.1 @@ -0,0 +1,166 @@ +.TH COQIDE 1 "July 16, 2004" + +.SH NAME +coqide \- The Coq Proof Assistant graphical interface + + +.SH SYNOPSIS +.B coqide +[ +.B options +] + +.SH DESCRIPTION + +.B coqtop +is a gtk graphical interface for the Coq proof assistant. + +For command-line-oriented use of Coq, see +.BR coqide (1) +; for batch-oriented use of Coq, see +.BR coqc (1). + + +.SH OPTIONS + +.TP +.B \-h +Show the complete list of options accepted by +.BR coqide . +.TP +.BI \-I\ dir ,\ \-include\ dir +Add directory dir in the include path. +.TP +.BI \-R\ dir\ coqdir +Recursively map physical +.I dir +to logical +.IR coqdir . +.TP +.B \-src +Add source directories in the include path. +.TP +.BI \-is\ f ,\ \-inputstate\ f +Read state from +.IR f .coq. +.TP +.B \-nois +Start with an empty state. +.TP +.BI \-outputstate\ f +Write state in file +.IR f .coq. +.TP +.BI \-load\-ml\-object\ f +Load ML object file +.IR f . +.TP +.BI \-load\-ml\-source\ f +Load ML file +.IR f . +.TP +.BI \-l\ f ,\ \-load\-vernac\-source\ f +Load Coq file +.IR f .v +(Load +.IR f .). +.TP +.BI \-lv\ f ,\ \-load\-vernac\-source\-verbose\ f +Load Coq file +.IR f .v +(Load Verbose +.IR f .). +.TP +.BI \-load\-vernac\-object\ f +Load Coq object file +.IR f .vo. +.TP +.BI \-require\ f +Load Coq object file +.IR f .vo +and import it (Require +.IR f .). +.TP +.BI \-compile\ f +Compile Coq file +.IR f .v +(implies +.BR \-batch ). +.TP +.BI \-compile\-verbose\ f +Verbosely compile Coq file +.IR f .v +(implies +.BR -batch ). +.TP +.B \-opt +Run the native-code version of Coq or Coq_SearchIsos. +.TP +.B \-byte +Run the bytecode version of Coq or Coq_SearchIsos. +.TP +.B \-where +Print Coq's standard library location and exit. +.TP +.B -v +Print Coq version and exit. +.TP +.B \-q +Skip loading of rcfile. +.TP +.BI \-init\-file\ f +Set the rcfile to +.IR f . +.TP +.BI \-user\ u +Use the rcfile of user +.IR u . +.TP +.B \-batch +Batch mode (exits just after arguments parsing). +.TP +.B \-boot +Boot mode (implies +.B \-q +and +.BR \-batch ). +.TP +.B \-emacs +Tells Coq it is executed under Emacs. +.TP +.BI \-dump\-glob\ f +Dump globalizations in file +.I f +(to be used by +.BR coqdoc (1)). +.TP +.B \-impredicative\-set +Set sort Set impredicative. +.TP +.B \-dont\-load\-proofs +Don't load opaque proofs in memory. +.TP +.B \-xml +Export XML files either to the hierarchy rooted in +the directory +.B COQ_XML_LIBRARY_ROOT +(if set) or to stdout (if unset). + + +.SH SEE ALSO + +.BR coqc (1), +.BR coqtop (1), +.BR coq-tex (1), +.BR coqdep (1). +.br +.I +The Coq Reference Manual, +.I +The Coq web site: http://coq.inria.fr, +.I +/usr/share/doc/coqide/FAQ. + +.SH AUTHOR +This manual page was written by Samuel Mimram <samuel.mimram@ens-lyon.org>, +for the Debian project (but may be used by others). diff --git a/debian/coqide.desktop b/debian/coqide.desktop new file mode 100644 index 00000000..1515c273 --- /dev/null +++ b/debian/coqide.desktop @@ -0,0 +1,9 @@ +[Desktop Entry] +Encoding=UTF-8 +Name=CoqIde +Comment=Graphical interface for the Coq proof assistant +Exec=/usr/bin/coqide +Type=Application +Categories=GTK;Science;Math; +Terminal=false +Icon=/usr/share/pixmaps/coq.xpm diff --git a/debian/coqide.dirs b/debian/coqide.dirs new file mode 100644 index 00000000..bf32ae9c --- /dev/null +++ b/debian/coqide.dirs @@ -0,0 +1,5 @@ +usr/lib/coq/ide +usr/share/doc/coqide +usr/share/applications +usr/share/man/man1 +usr/share/pixmaps diff --git a/debian/coqide.docs b/debian/coqide.docs new file mode 100644 index 00000000..3a260c89 --- /dev/null +++ b/debian/coqide.docs @@ -0,0 +1,2 @@ +ide/FAQ +ide/utf8.v diff --git a/debian/coqide.install b/debian/coqide.install new file mode 100644 index 00000000..7df75581 --- /dev/null +++ b/debian/coqide.install @@ -0,0 +1,5 @@ +usr/bin/coqide* +usr/lib/coq/ide/coq.ico +usr/lib/coq/ide/coq2.ico +usr/lib/coq/ide/utf8.vo +usr/lib/coq/ide/.coqide-gtk2rc diff --git a/debian/coqide.menu b/debian/coqide.menu new file mode 100644 index 00000000..0fb1935a --- /dev/null +++ b/debian/coqide.menu @@ -0,0 +1,4 @@ +?package(coqide):command="/usr/bin/coqide" \ + icon="/usr/share/pixmaps/coqide.xpm" \ + needs="X11" \ + section="Apps/Math" title="CoqIde" diff --git a/debian/coqmktop.1 b/debian/coqmktop.1 new file mode 100644 index 00000000..a35e436a --- /dev/null +++ b/debian/coqmktop.1 @@ -0,0 +1,70 @@ +.TH COQ 1 "April 25, 2001" + +.SH NAME +coqmktop \- The Coq Proof Assistant user-tactics linker + + +.SH SYNOPSIS +.B coqmktop +[ +.I options +] +.I files + + +.SH DESCRIPTION + +.B coqmktop +builds a new Coq toplevel extended with user-tactics. +.IR files \& +are the Objective Caml object or library files (i.e. with suffix .cmo, +.cmx, .cma or .cmxa) to link with the Coq system. +The linker produces an executable Coq toplevel which can be called +directly or through coqc(1), using the -image option. + +.SH OPTIONS + +.TP +.BI \-h +Show a list of the available options. +.TP +.BI \-srcdir\ dir +Specify where the Coq source files are. +.TP +.BI \-o\ exec\-fil +Specify the name of the resulting toplevel. +.TP +.B \-opt +Compile in native code. +.TP +.B \-full +Link high level tactics. +.TP +.B \-top +Build Coq on a ocaml toplevel (incompatible with +.BR \-opt ). +.TP +.B \-searchisos +Build a toplevel for SearchIsos. +.TP +.B \-ide +Build a toplevel for the Coq IDE. +.TP +.BI \-R\ dir +Specify recursively directories for Ocaml. +.TP +.B \-v8 +Link with V8 grammar. + + +.SH SEE ALSO + +.BR coqtop (1), +.BR ocamlmktop (1). +.BR ocamlc (1). +.BR ocamlopt (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr diff --git a/debian/coqtop.1 b/debian/coqtop.1 new file mode 100644 index 00000000..b136a68b --- /dev/null +++ b/debian/coqtop.1 @@ -0,0 +1,155 @@ +.TH COQ 1 "April 25, 2001" + +.SH NAME +coqtop \- The Coq Proof Assistant toplevel system + + +.SH SYNOPSIS +.B coqtop +[ +.B options +] + +.SH DESCRIPTION + +.B coqtop +is the toplevel system of Coq, for interactive use. +It reads phrases on the standard input, and prints results on the +standard output. + +For batch-oriented use of Coq, see +.BR coqc (1). + + +.SH OPTIONS + +.TP +.B \-h +Show the complete list of options accepted by coqtop. +.TP +.BI \-I\ dir ,\ \-include\ dir +Add directory dir in the include path. +.TP +.BI \-R\ dir\ coqdir +Recursively map physical dir to logical coqdir. +.TP +.B \-src +Add source directories in the include path. +.TP +.BI \-is\ f ,\ \-inputstate\ f +Read state from file +.IR f .coq. +.TP +.B \-nois +Start with an empty state. +.TP +.BI \-outputstate\ f +Write state in file +.IR f .coq. +.TP +.BR \-load\-ml\-object\ f +Load ML object file +.IR f . +.TP +.BI \-load\-ml\-source\ f +Load ML file +.IR f . +.TP +.BI \-l\ f ,\ \-load\-vernac\-source\ f +Load Coq file +.IR f .v +(Load +.IR f .). +.TP +.BI \-lv\ f ,\ \-load\-vernac\-source\-verbose\ f +Load Coq file +.IR f .v +(Load Verbose +.IR f .). +.TP +.BI \-load\-vernac\-object\ f +Load Coq object file +.IR f .vo. +.TP +.BI \-require\ f +Load Coq object file +.IR f .vo +and import it (Require +.IR f .). +.TP +.BI \-compile\ f +Compile Coq file +.IR f .v +(implies +.BR \-batch ). +.TP +.BI \-compile\-verbose\ f +Verbosely compile Coq file +.IR f .v +(implies +.BR \-batch ). +.TP +.B \-opt +Run the native-code version of Coq or Coq_SearchIsos. +.TP +.B \-byte +Run the bytecode version of Coq or Coq_SearchIsos. +.TP +.B \-where +Print Coq's standard library location and exit. +.TP +.B \-v +Print Coq version and exit. +.TP +.B \-q +Skip loading of rcfile. +.TP +.BI \-init\-file\ f +Set the rcfile to +.IR f . +.TP +.BI \-user\ u +Use the rcfile of user +.IR u . +.TP +.B \-batch +Batch mode (exits just after arguments parsing). +.TP +.B \-boot +Boot mode (implies +.B \-q +and +.BR \-batch ). +.TP +.B \-emacs +Tells Coq it is executed under Emacs. +.TP +.BI \-dump\-glob\ f +Dump globalizations in file +.I f +(to be used by +.BR coqdoc (1)). +.TP +.B \-impredicative\-set +Set sort Set impredicative. +.TP +.B \-dont\-load\-proofs +Don't load opaque proofs in memory. +.TP +.B \-xml +Export XML files either to the hierarchy rooted in +the directory +.B COQ_XML_LIBRARY_ROOT +(if set) or to stdout (if unset). + + +.SH SEE ALSO + +.BR coqc (1), +.BR coq-tex (1), +.BR coqdep (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr diff --git a/debian/docs b/debian/docs new file mode 100644 index 00000000..297170db --- /dev/null +++ b/debian/docs @@ -0,0 +1,2 @@ +README +CREDITS diff --git a/debian/patches/00list b/debian/patches/00list new file mode 100644 index 00000000..3804c9ad --- /dev/null +++ b/debian/patches/00list @@ -0,0 +1 @@ +coq-8.0pl3-ocaml-3.09 diff --git a/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch b/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch new file mode 100755 index 00000000..90b4d583 --- /dev/null +++ b/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch @@ -0,0 +1,507 @@ +#! /bin/sh /usr/share/dpatch/dpatch-run +## coq-8.0pl3-ocaml-3.09.dpatch by Samuel Mimram <smimram@debian.org> +## +## All lines beginning with `## DP:' are a description of the patch. +## DP: Patch provided by coq's upstream to fix problems with OCaml 3.09. +## DP: ftp://ftp.inria.fr/INRIA/coq/V8.0pl3/patch-coq-8.0pl3-ocaml-3.09 + +@DPATCH@ +diff -urNad coq-8.0pl3~/Makefile coq-8.0pl3/Makefile +--- coq-8.0pl3~/Makefile 2006-01-11 23:18:05.000000000 +0000 ++++ coq-8.0pl3/Makefile 2006-02-19 11:28:43.000000000 +0000 +@@ -77,8 +77,8 @@ + + MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) + +-BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) +-OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) ++BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) -w y ++OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) -w y + OCAMLDEP=ocamldep + DEPFLAGS=-slash $(LOCALINCLUDES) + +diff -urNad coq-8.0pl3~/contrib/first-order/sequent.ml coq-8.0pl3/contrib/first-order/sequent.ml +--- coq-8.0pl3~/contrib/first-order/sequent.ml 2004-07-16 19:30:10.000000000 +0000 ++++ coq-8.0pl3/contrib/first-order/sequent.ml 2006-02-19 11:28:43.000000000 +0000 +@@ -6,7 +6,7 @@ + (* * GNU Lesser General Public License Version 2.1 *) + (************************************************************************) + +-(* $Id: sequent.ml,v 1.17.2.1 2004/07/16 19:30:10 herbelin Exp $ *) ++(* $Id: sequent.ml,v 1.17.2.2 2006/01/25 22:40:30 herbelin Exp $ *) + + open Term + open Util +@@ -278,7 +278,7 @@ + let h dbname= + let hdb= + try +- Util.Stringmap.find dbname !searchtable ++ searchtable_map dbname + with Not_found-> + error ("Firstorder: "^dbname^" : No such Hint database") in + Hint_db.iter g hdb in +diff -urNad coq-8.0pl3~/contrib/interface/blast.ml coq-8.0pl3/contrib/interface/blast.ml +--- coq-8.0pl3~/contrib/interface/blast.ml 2004-07-16 19:30:11.000000000 +0000 ++++ coq-8.0pl3/contrib/interface/blast.ml 2006-02-19 11:28:43.000000000 +0000 +@@ -351,16 +351,16 @@ + let db_list = + List.map + (fun x -> +- try Stringmap.find x !searchtable ++ try searchtable_map x + with Not_found -> error ("EAuto: "^x^": No such Hint database")) + ("core"::dbnames) + in + tclTRY (e_search_auto debug np db_list) + + let full_eauto debug n gl = +- let dbnames = stringmap_dom !searchtable in ++ let dbnames = current_db_names () in + let dbnames = list_subtract dbnames ["v62"] in +- let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in ++ let db_list = List.map searchtable_map dbnames in + let local_db = make_local_hint_db gl in + tclTRY (e_search_auto debug n db_list) gl + +@@ -369,8 +369,6 @@ + (********************************************************************** + copié de tactics/auto.ml on a juste modifié search_gen + *) +-let searchtable_map name = +- Stringmap.find name !searchtable + + (* local_db is a Hint database containing the hypotheses of current goal *) + (* Papageno : cette fonction a été pas mal simplifiée depuis que la base +@@ -499,9 +497,9 @@ + let default_search_depth = ref 5 + + let full_auto n gl = +- let dbnames = stringmap_dom !searchtable in ++ let dbnames = current_db_names () in + let dbnames = list_subtract dbnames ["v62"] in +- let db_list = List.map (fun x -> searchtable_map x) dbnames in ++ let db_list = List.map searchtable_map dbnames in + let hyps = pf_hyps gl in + tclTRY (search n db_list (make_local_hint_db gl) hyps) gl + +diff -urNad coq-8.0pl3~/interp/symbols.ml coq-8.0pl3/interp/symbols.ml +--- coq-8.0pl3~/interp/symbols.ml 2004-11-17 09:33:38.000000000 +0000 ++++ coq-8.0pl3/interp/symbols.ml 2006-02-19 11:28:43.000000000 +0000 +@@ -6,7 +6,7 @@ + (* * GNU Lesser General Public License Version 2.1 *) + (************************************************************************) + +-(* $Id: symbols.ml,v 1.31.2.2 2004/11/17 09:33:38 herbelin Exp $ *) ++(* $Id: symbols.ml,v 1.31.2.3 2006/01/25 22:40:30 herbelin Exp $ *) + + (*i*) + open Util +@@ -43,18 +43,18 @@ + type delimiters = string + + type scope = { +- notations: (interpretation * (dir_path * string) * bool) Stringmap.t; ++ notations: (string, interpretation * (dir_path * string) * bool) Gmap.t; + delimiters: delimiters option + } + + (* Uninterpreted notation map: notation -> level * dir_path *) +-let notation_level_map = ref Stringmap.empty ++let notation_level_map = ref Gmap.empty + + (* Scopes table: scope_name -> symbol_interpretation *) +-let scope_map = ref Stringmap.empty ++let scope_map = ref Gmap.empty + + let empty_scope = { +- notations = Stringmap.empty; ++ notations = Gmap.empty; + delimiters = None + } + +@@ -62,20 +62,20 @@ + let type_scope = "type_scope" (* special scope used for interpreting types *) + + let init_scope_map () = +- scope_map := Stringmap.add default_scope empty_scope !scope_map; +- scope_map := Stringmap.add type_scope empty_scope !scope_map ++ scope_map := Gmap.add default_scope empty_scope !scope_map; ++ scope_map := Gmap.add type_scope empty_scope !scope_map + + (**********************************************************************) + (* Operations on scopes *) + + let declare_scope scope = +- try let _ = Stringmap.find scope !scope_map in () ++ try let _ = Gmap.find scope !scope_map in () + with Not_found -> + (* Options.if_verbose message ("Creating scope "^scope);*) +- scope_map := Stringmap.add scope empty_scope !scope_map ++ scope_map := Gmap.add scope empty_scope !scope_map + + let find_scope scope = +- try Stringmap.find scope !scope_map ++ try Gmap.find scope !scope_map + with Not_found -> error ("Scope "^scope^" is not declared") + + let check_scope sc = let _ = find_scope sc in () +@@ -124,7 +124,7 @@ + (**********************************************************************) + (* Delimiters *) + +-let delimiters_map = ref Stringmap.empty ++let delimiters_map = ref Gmap.empty + + let declare_delimiters scope key = + let sc = find_scope scope in +@@ -134,15 +134,15 @@ + warning ("Overwritting previous delimiting key "^old^" in scope "^scope) + end; + let sc = { sc with delimiters = Some key } in +- scope_map := Stringmap.add scope sc !scope_map; +- if Stringmap.mem key !delimiters_map then begin +- let oldsc = Stringmap.find key !delimiters_map in ++ scope_map := Gmap.add scope sc !scope_map; ++ if Gmap.mem key !delimiters_map then begin ++ let oldsc = Gmap.find key !delimiters_map in + Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc) + end; +- delimiters_map := Stringmap.add key scope !delimiters_map ++ delimiters_map := Gmap.add key scope !delimiters_map + + let find_delimiters_scope loc key = +- try Stringmap.find key !delimiters_map ++ try Gmap.find key !delimiters_map + with Not_found -> + user_err_loc + (loc, "find_delimiters", str ("Unknown scope delimiting key "^key)) +@@ -229,7 +229,7 @@ + let find_with_delimiters = function + | None -> None + | Some scope -> +- match (Stringmap.find scope !scope_map).delimiters with ++ match (Gmap.find scope !scope_map).delimiters with + | Some key -> Some (Some scope, Some key) + | None -> None + +@@ -257,23 +257,23 @@ + (* Uninterpreted notation levels *) + + let declare_notation_level ntn level = +- if not !Options.v7 & Stringmap.mem ntn !notation_level_map then ++ if not !Options.v7 & Gmap.mem ntn !notation_level_map then + error ("Notation "^ntn^" is already assigned a level"); +- notation_level_map := Stringmap.add ntn level !notation_level_map ++ notation_level_map := Gmap.add ntn level !notation_level_map + + let level_of_notation ntn = +- Stringmap.find ntn !notation_level_map ++ Gmap.find ntn !notation_level_map + + (* The mapping between notations and their interpretation *) + + let declare_notation_interpretation ntn scopt pat df pp8only = + let scope = match scopt with Some s -> s | None -> default_scope in + let sc = find_scope scope in +- if Stringmap.mem ntn sc.notations && Options.is_verbose () then ++ if Gmap.mem ntn sc.notations && Options.is_verbose () then + warning ("Notation "^ntn^" was already used"^ + (if scopt = None then "" else " in scope "^scope)); +- let sc = { sc with notations = Stringmap.add ntn (pat,df,pp8only) sc.notations } in +- scope_map := Stringmap.add scope sc !scope_map; ++ let sc = { sc with notations = Gmap.add ntn (pat,df,pp8only) sc.notations } in ++ scope_map := Gmap.add scope sc !scope_map; + if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack + + let declare_uninterpretation rule (metas,c as pat) = +@@ -292,7 +292,7 @@ + let rec interp_notation loc ntn scopes = + let f sc = + let scope = find_scope sc in +- let (pat,df,pp8only) = Stringmap.find ntn scope.notations in ++ let (pat,df,pp8only) = Gmap.find ntn scope.notations in + if pp8only then raise Not_found; + pat,(df,if sc = default_scope then None else Some sc) in + try find_interpretation f (List.fold_right push_scope scopes !scope_stack) +@@ -308,7 +308,7 @@ + + let availability_of_notation (ntn_scope,ntn) scopes = + let f scope = +- Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in ++ Gmap.mem ntn (Gmap.find scope !scope_map).notations in + find_without_delimiters f (ntn_scope,Some ntn) scopes + + let rec interp_numeral_gen loc f n = function +@@ -356,8 +356,8 @@ + let exists_notation_in_scope scopt ntn r = + let scope = match scopt with Some s -> s | None -> default_scope in + try +- let sc = Stringmap.find scope !scope_map in +- let (r',_,pp8only) = Stringmap.find ntn sc.notations in ++ let sc = Gmap.find scope !scope_map in ++ let (r',_,pp8only) = Gmap.find ntn sc.notations in + r' = r, pp8only + with Not_found -> false, false + +@@ -487,14 +487,14 @@ + + let pr_named_scope prraw scope sc = + (if scope = default_scope then +- match Stringmap.fold (fun _ _ x -> x+1) sc.notations 0 with ++ match Gmap.fold (fun _ _ x -> x+1) sc.notations 0 with + | 0 -> str "No lonely notation" + | n -> str "Lonely notation" ++ (if n=1 then mt() else str"s") + else + str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters) + ++ fnl () + ++ pr_scope_classes scope +- ++ Stringmap.fold ++ ++ Gmap.fold + (fun ntn ((_,r),(_,df),_) strm -> + pr_notation_info prraw df r ++ fnl () ++ strm) + sc.notations (mt ()) +@@ -502,12 +502,12 @@ + let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope) + + let pr_scopes prraw = +- Stringmap.fold ++ Gmap.fold + (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm) + !scope_map (mt ()) + + let rec find_default ntn = function +- | Scope scope::_ when Stringmap.mem ntn (find_scope scope).notations -> ++ | Scope scope::_ when Gmap.mem ntn (find_scope scope).notations -> + Some scope + | SingleNotation ntn'::_ when ntn = ntn' -> Some default_scope + | _::scopes -> find_default ntn scopes +@@ -531,9 +531,9 @@ + if String.contains ntn ' ' then (=) ntn + else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in + let l = +- Stringmap.fold ++ Gmap.fold + (fun scope_name sc -> +- Stringmap.fold (fun ntn ((_,r),df,_) l -> ++ Gmap.fold (fun ntn ((_,r),df,_) l -> + if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations) + map [] in + let l = List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l in +@@ -560,7 +560,7 @@ + + let collect_notation_in_scope scope sc known = + assert (scope <> default_scope); +- Stringmap.fold ++ Gmap.fold + (fun ntn ((_,r),(_,df),_) (l,known as acc) -> + if List.mem ntn known then acc else ((df,r)::l,ntn::known)) + sc.notations ([],known) +@@ -578,7 +578,7 @@ + if List.mem ntn knownntn then (all,knownntn) + else + let ((_,r),(_,df),_) = +- Stringmap.find ntn (find_scope default_scope).notations in ++ Gmap.find ntn (find_scope default_scope).notations in + let all' = match all with + | (s,lonelyntn)::rest when s = default_scope -> + (s,(df,r)::lonelyntn)::rest +@@ -614,13 +614,13 @@ + + (* Concrete syntax for symbolic-extension table *) + let printing_rules = +- ref (Stringmap.empty : unparsing_rule Stringmap.t) ++ ref (Gmap.empty : (string, unparsing_rule) Gmap.t) + + let declare_notation_printing_rule ntn unpl = +- printing_rules := Stringmap.add ntn unpl !printing_rules ++ printing_rules := Gmap.add ntn unpl !printing_rules + + let find_notation_printing_rule ntn = +- try Stringmap.find ntn !printing_rules ++ try Gmap.find ntn !printing_rules + with Not_found -> anomaly ("No printing rule found for "^ntn) + + (**********************************************************************) +@@ -644,13 +644,13 @@ + let init () = + init_scope_map (); + (* +- scope_stack := Stringmap.empty ++ scope_stack := Gmap.empty + arguments_scope := Refmap.empty + *) +- notation_level_map := Stringmap.empty; +- delimiters_map := Stringmap.empty; ++ notation_level_map := Gmap.empty; ++ delimiters_map := Gmap.empty; + notations_key_table := Gmapl.empty; +- printing_rules := Stringmap.empty; ++ printing_rules := Gmap.empty; + class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty + + let _ = +diff -urNad coq-8.0pl3~/tactics/auto.ml coq-8.0pl3/tactics/auto.ml +--- coq-8.0pl3~/tactics/auto.ml 2005-05-15 12:47:04.000000000 +0000 ++++ coq-8.0pl3/tactics/auto.ml 2006-02-19 11:28:43.000000000 +0000 +@@ -6,7 +6,7 @@ + (* * GNU Lesser General Public License Version 2.1 *) + (************************************************************************) + +-(* $Id: auto.ml,v 1.63.2.3 2005/05/15 12:47:04 herbelin Exp $ *) ++(* $Id: auto.ml,v 1.63.2.4 2006/01/25 22:40:29 herbelin Exp $ *) + + open Pp + open Util +@@ -134,24 +134,28 @@ + + end + +-type frozen_hint_db_table = Hint_db.t Stringmap.t ++module Hintdbmap = Gmap + +-type hint_db_table = Hint_db.t Stringmap.t ref ++type frozen_hint_db_table = (string,Hint_db.t) Hintdbmap.t ++ ++type hint_db_table = (string,Hint_db.t) Hintdbmap.t ref + + type hint_db_name = string + +-let searchtable = (ref Stringmap.empty : hint_db_table) ++let searchtable = (ref Hintdbmap.empty : hint_db_table) + + let searchtable_map name = +- Stringmap.find name !searchtable ++ Hintdbmap.find name !searchtable + let searchtable_add (name,db) = +- searchtable := Stringmap.add name db !searchtable ++ searchtable := Hintdbmap.add name db !searchtable ++let current_db_names () = ++ Hintdbmap.dom !searchtable + + (**************************************************************************) + (* Definition of the summary *) + (**************************************************************************) + +-let init () = searchtable := Stringmap.empty ++let init () = searchtable := Hintdbmap.empty + let freeze () = !searchtable + let unfreeze fs = searchtable := fs + +@@ -498,7 +502,7 @@ + + (* Print all hints associated to head c in any database *) + let fmt_hint_list_for_head c = +- let dbs = stringmap_to_list !searchtable in ++ let dbs = Hintdbmap.to_list !searchtable in + let valid_dbs = + map_succeed + (fun (name,db) -> (name,db,Hint_db.map_all c db)) +@@ -523,7 +527,7 @@ + | [] -> assert false + in + let hd = head_of_constr_reference hdc in +- let dbs = stringmap_to_list !searchtable in ++ let dbs = Hintdbmap.to_list !searchtable in + let valid_dbs = + if occur_existential cl then + map_succeed +@@ -568,7 +572,7 @@ + + (* displays all the hints of all databases *) + let print_searchtable () = +- Stringmap.iter ++ Hintdbmap.iter + (fun name db -> + msg (str "In the database " ++ str name ++ fnl ()); + print_hint_db db) +@@ -693,7 +697,7 @@ + tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl + + let full_trivial gl = +- let dbnames = stringmap_dom !searchtable in ++ let dbnames = Hintdbmap.dom !searchtable in + let dbnames = list_subtract dbnames ["v62"] in + let db_list = List.map (fun x -> searchtable_map x) dbnames in + tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl +@@ -798,7 +802,7 @@ + let default_auto = auto !default_search_depth [] + + let full_auto n gl = +- let dbnames = stringmap_dom !searchtable in ++ let dbnames = Hintdbmap.dom !searchtable in + let dbnames = list_subtract dbnames ["v62"] in + let db_list = List.map (fun x -> searchtable_map x) dbnames in + let hyps = pf_hyps gl in +@@ -911,7 +915,7 @@ + to_add empty_named_context in + let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in + let db = Hint_db.add_list db0 (make_local_hint_db g) in +- super_search n [Stringmap.find "core" !searchtable] db argl g ++ super_search n [Hintdbmap.find "core" !searchtable] db argl g + + let superauto n to_add argl = + tclTRY (tclCOMPLETE (search_superauto n to_add argl)) +diff -urNad coq-8.0pl3~/tactics/auto.mli coq-8.0pl3/tactics/auto.mli +--- coq-8.0pl3~/tactics/auto.mli 2005-01-21 16:41:52.000000000 +0000 ++++ coq-8.0pl3/tactics/auto.mli 2006-02-19 11:28:43.000000000 +0000 +@@ -6,7 +6,7 @@ + (* * GNU Lesser General Public License Version 2.1 *) + (************************************************************************) + +-(*i $Id: auto.mli,v 1.22.2.2 2005/01/21 16:41:52 herbelin Exp $ i*) ++(*i $Id: auto.mli,v 1.22.2.3 2006/01/25 22:40:29 herbelin Exp $ i*) + + (*i*) + open Util +@@ -56,12 +56,16 @@ + val iter : (constr_label -> stored_data list -> unit) -> t -> unit + end + +-type frozen_hint_db_table = Hint_db.t Stringmap.t ++type frozen_hint_db_table + +-type hint_db_table = Hint_db.t Stringmap.t ref ++type hint_db_table + + type hint_db_name = string + ++val searchtable_map : hint_db_name -> Hint_db.t ++ ++val current_db_names : unit -> hint_db_name list ++ + val add_hints : locality_flag -> hint_db_name list -> hints -> unit + + val print_searchtable : unit -> unit +diff -urNad coq-8.0pl3~/tactics/eauto.ml4 coq-8.0pl3/tactics/eauto.ml4 +--- coq-8.0pl3~/tactics/eauto.ml4 2004-07-16 19:30:52.000000000 +0000 ++++ coq-8.0pl3/tactics/eauto.ml4 2006-02-19 11:28:43.000000000 +0000 +@@ -8,7 +8,7 @@ + + (*i camlp4deps: "parsing/grammar.cma" i*) + +-(* $Id: eauto.ml4,v 1.11.2.1 2004/07/16 19:30:52 herbelin Exp $ *) ++(* $Id: eauto.ml4,v 1.11.2.2 2006/01/25 22:40:29 herbelin Exp $ *) + + open Pp + open Util +@@ -391,16 +391,16 @@ + let db_list = + List.map + (fun x -> +- try Stringmap.find x !searchtable ++ try searchtable_map x + with Not_found -> error ("EAuto: "^x^": No such Hint database")) + ("core"::dbnames) + in + tclTRY (e_search_auto debug np db_list) + + let full_eauto debug n gl = +- let dbnames = stringmap_dom !searchtable in ++ let dbnames = current_db_names () in + let dbnames = list_subtract dbnames ["v62"] in +- let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in ++ let db_list = List.map (fun x -> searchtable_map x) dbnames in + let local_db = make_local_hint_db gl in + tclTRY (e_search_auto debug n db_list) gl + diff --git a/debian/rules b/debian/rules new file mode 100755 index 00000000..b4498d12 --- /dev/null +++ b/debian/rules @@ -0,0 +1,131 @@ +#!/usr/bin/make -f +# debian/rules for coq + +# Uncomment this to turn on verbose mode. +#export DH_VERBOSE=1 + +# This has to be exported to make some magic below work. +export DH_OPTIONS + +# We want to use dpatch +include /usr/share/dpatch/dpatch.make + +COQPREF=$(CURDIR)/debian/tmp +ADDPREF=COQINSTALLPREFIX=$(COQPREF) + +CONFIGUREOPTS=--prefix /usr --mandir /usr/share/man \ + --emacslib /usr/share/emacs/site-lisp/coq --reals all + +configure: configure-stamp +configure-stamp: + dh_testdir + if [ -e /usr/bin/ocamlc.opt ]; \ + then \ + ./configure -opt $(CONFIGUREOPTS); \ + else \ + ./configure $(CONFIGUREOPTS); \ + fi + touch configure-stamp + +build: patch-stamp configure-stamp build-stamp +build-stamp: + dh_testdir + if grep -q BEST=opt config/Makefile; \ + then \ + ($(MAKE) check \ + && touch opt-stamp) \ + || (echo WARNING: NATIVE CODE COMPILATION FAILED \ + && echo Trying to build coq in bytecode instead \ + && $(MAKE) archclean clean \ + && $(MAKE) BEST=byte HASCOQIDE=byte check \ + && echo NATIVE CODE COMPILATION FAILED \ + && echo Coq was built in bytecode instead); \ + else \ + $(MAKE) BEST=byte HASCOQIDE=byte check; \ + fi + touch build-stamp + +clean: unpatch + dh_testdir + dh_testroot + rm -f build-stamp configure-stamp opt-stamp + + -$(MAKE) clean + -$(MAKE) archclean + rm -f bin/parser.opt + rm -f tools/coqdoc/*.cm[oi] + rm -f config/coq_config.ml config/Makefile test-suite/check.log + + dh_clean + +install: build + dh_testdir + dh_testroot + dh_clean -k + dh_installdirs + + if [ -e opt-stamp ]; then \ + $(MAKE) $(ADDPREF) install; \ + else \ + $(MAKE) BEST=byte HASCOQIDE=byte $(ADDPREF) install; \ + fi + + -for i in $(COQPREF)/usr/bin/*.opt; do \ + echo "Stripping: $$i"; \ + strip -R .note -R .comment $$i; \ + done + -for i in $(COQPREF)/usr/bin/coqide.*; do \ + echo "Rpath for `chrpath $$i`"; \ + echo "Removing rpath: $$i"; \ + chrpath -d $$i; \ + done + cp debian/coq.xpm debian/coq/usr/share/pixmaps/coq.xpm + cp debian/coq.xpm debian/coqide/usr/share/pixmaps/coqide.xpm + cp debian/coqide.desktop debian/coqide/usr/share/applications + + cp ide/index_urls.txt debian/coqide/usr/lib/coq/ide/index_urls.txt + if [ -e opt-stamp ]; then \ + cp debian/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.opt.1; \ + cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.opt.1; \ + fi + cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.1 + cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.byte.1 + cp debian/coqc.1 debian/coq/usr/share/man/man1/coqc.1 + cp debian/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.1 + cp debian/coq_makefile.1 debian/coq/usr/share/man/man1/coq_makefile.1 + cp debian/coqmktop.1 debian/coq/usr/share/man/man1/coqmktop.1 + cp debian/coqtop.1 debian/coq/usr/share/man/man1/coqtop.1 + + chmod -x debian/tmp/usr/lib/coq/ide/coq2.ico + + # These are installed as docs + rm -f $(COQPREF)/usr/lib/coq/ide/utf8.v $(COQPREF)/usr/lib/coq/ide/FAQ + + dh_install --sourcedir=$(COQPREF) --list-missing + +binary-common: + dh_testdir + dh_testroot + dh_installdocs + dh_installmenu + dh_installemacsen + dh_installman + dh_installchangelogs CHANGES + dh_desktop + dh_link + dh_compress + dh_fixperms + dh_installdeb + dh_shlibdeps + dh_gencontrol + dh_md5sums + dh_builddeb + +binary-indep: build install + $(MAKE) -f debian/rules DH_OPTIONS=-i binary-common + +binary-arch: build install + $(MAKE) -f debian/rules DH_OPTIONS=-a binary-common + +binary: binary-indep binary-arch +.PHONY: build clean binary-indep binary-arch binary-common binary install configure diff --git a/debian/svn-deblayout b/debian/svn-deblayout new file mode 100644 index 00000000..b849ea05 --- /dev/null +++ b/debian/svn-deblayout @@ -0,0 +1,3 @@ +origDir=../upstream +origUrl=svn+ssh://svn.debian.org/svn/pkg-ocaml-maint/trunk/packages/coq/upstream +tagsUrl=svn+ssh://svn.debian.org/svn/pkg-ocaml-maint/tags/packages/coq diff --git a/debian/watch b/debian/watch new file mode 100644 index 00000000..8867705d --- /dev/null +++ b/debian/watch @@ -0,0 +1,2 @@ +version=2 +ftp://ftp.inria.fr/INRIA/coq/current/coq-([0-9a-z\.]*)\.tar\.gz debian uupdate |