diff options
41 files changed, 2428 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..527e5c78 --- /dev/null +++ b/debian/changelog @@ -0,0 +1,400 @@ +coq (8.1.pl1+dfsg-4) UNRELEASED; urgency=low + + * Corrected emacs-mode startup file, closes: #446170. + + -- Samuel Mimram <smimram@debian.org> Wed, 10 Oct 2007 22:36:07 +0000 + +coq (8.1.pl1+dfsg-3) unstable; urgency=low + + * Depend on ocaml-base-nox since coq_makefile needs ocamlrun, + closes: #439570. + + -- Samuel Mimram <smimram@debian.org> Sat, 08 Sep 2007 00:35:31 +0200 + +coq (8.1.pl1+dfsg-2) experimental; urgency=low + + * Updated for OCaml 3.10. + * Build-depend on camlp5. + * Added camlp5.dpatch to fix compilation problems. + + -- Samuel Mimram <smimram@debian.org> Wed, 22 Aug 2007 16:39:04 +0000 + +coq (8.1.pl1+dfsg-1) unstable; urgency=low + + * New upstream release. + + -- Samuel Mimram <smimram@debian.org> Sat, 18 Aug 2007 20:59:45 +0200 + +coq (8.1+dfsg-6) unstable; urgency=low + + * Add dependencies on ${misc:Depends}, closes: #431679. + + -- Samuel Mimram <smimram@debian.org> Wed, 04 Jul 2007 10:49:01 +0200 + +coq (8.1+dfsg-5) unstable; urgency=low + + * Correctly clean, closes: #424162. + + -- Samuel Mimram <smimram@debian.org> Tue, 22 May 2007 21:53:16 +0200 + +coq (8.1+dfsg-4) unstable; urgency=low + + * Correctly set Coq_config.best when rebuilding in byte mode. + * Removed tetex-extra from build-dependencies. + + -- Samuel Mimram <smimram@debian.org> Tue, 24 Apr 2007 14:46:59 +0000 + +coq (8.1+dfsg-3) unstable; urgency=low + + * Uploading to unstable. + + -- Samuel Mimram <smimram@debian.org> Mon, 09 Apr 2007 16:48:46 +0200 + +coq (8.1+dfsg-2) experimental; urgency=low + + * Added cmxa-install.dpatch to install cmxa only on native archs, + closes: #415867. + * Added configure.dpatch for the configure to correctly detect whether + ocamlopt is present or not. + * Use dh_installtex instead of hand-crafted postinst. + + -- Samuel Mimram <smimram@debian.org> Sun, 18 Mar 2007 13:21:56 +0100 + +coq (8.1+dfsg-1) experimental; urgency=low + + * New upstream release. + * Removed system.dpatch and next-ia64.dpatch, integrated upstream. + * Removed the subdirectories common, faq, RecTutorial, refman, rt, tools, + tutorial of the directory doc since they contain documentation under the + Open Publication License which is not DFSG-free (thus the +dfsg in the + version number). The script debian/utils/purify_tarball automates this + process. This documentation in packaged separately in non-free, in + the coq-doc package. + + -- Samuel Mimram <smimram@debian.org> Tue, 13 Feb 2007 11:38:43 +0000 + +coq (8.1~gamma-4) experimental; urgency=low + + * Correctly build glob.dump on non-native archs, closes: #400535. + + -- Samuel Mimram <smimram@debian.org> Sun, 11 Feb 2007 18:02:49 +0100 + +coq (8.1~gamma-3) experimental; urgency=low + + * Added next-ia64.dpatch to fix the FTBFS on ia64. + * Correctly install coqdoc.sty, closes: #409027. + * Build-depend on tetex-extra | texlive-latex-extra in order to allow + building with texlive. + + -- Samuel Mimram <smimram@debian.org> Sun, 4 Feb 2007 20:38:43 +0100 + +coq (8.1~gamma-2) experimental; urgency=low + + * Added no-complexity-test.dpatch to skip complexity checks (thanks Julien + Cristau), closes: #399919. + + -- Samuel Mimram <smimram@debian.org> Thu, 23 Nov 2006 14:27:15 +0000 + +coq (8.1~gamma-1) experimental; urgency=low + + * New upstream release. + * Made the package binNMU-safe. + * Minor improvements of the coqide.desktop file, closes: #383310. + * Added system.dpatch to avoid erroneous interpretation of ~. + * Removed assert.dpatch, integrated upstream. + + -- Samuel Mimram <smimram@debian.org> Tue, 21 Nov 2006 13:33:55 +0000 + +coq (8.0pl3+8.1beta.2-1) experimental; urgency=low + + * New upstream beta release. + * Added assert.dpatch to check assertions in native mode. + + -- Samuel Mimram <smimram@debian.org> Thu, 13 Jul 2006 16:28:24 +0000 + +coq (8.0pl3+8.1beta-1) experimental; urgency=low + + * New upstream release. + * Added --fsets all option to configure to build the theory of finite sets. + * Updated coqdoc_stdlib.dpatch, partly integrated upstream. + * Removed failing_tests.dpath, all the tests should succeed now. + * We don't need to remove rpaths anymore. + * Updated standards version to 3.7.2, no changes needed. + + -- Samuel Mimram <smimram@debian.org> Fri, 16 Jun 2006 12:59:07 +0000 + +coq (8.0pl3+8.1alpha-2) experimental; urgency=low + + * Added makefile.dpatch in order for ocamlopt not to be called when + compiling on non-native archs. + * Do not build the pdf documentation for the library since we don't ship it. + This will avoid the FTBFS because of missing LaTeX fonts. + + -- Samuel Mimram <smimram@debian.org> Sun, 30 Apr 2006 11:51:57 +0000 + +coq (8.0pl3+8.1alpha-1) experimental; urgency=low + + * New upstream release. + * No longer providing the compatibility coq7-libs package. + * coq-libs is now providing its documentation in html format. + * Added browser.dpatch to use the default Debian browser for help. + * Disabling checks which don't succeed for now: failing_tests.dpatch. + * Removed coq-8.0pl3-ocaml-3.09.dpatch. + + -- Samuel Mimram <smimram@debian.org> Thu, 27 Apr 2006 13:43:16 +0000 + +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..3824703e --- /dev/null +++ b/debian/control @@ -0,0 +1,53 @@ +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.7.2 +Build-Depends: debhelper (>= 4.0.0), dpkg-dev (>= 1.13.19), dpatch, ocaml-nox (>= 3.10), ocaml-best-compilers, camlp5, liblablgtk2-ocaml-dev (>= 2.4.0), texlive-latex-extra, hevea +XS-Vcs-Svn: svn://svn.debian.org/svn/pkg-ocaml-maint/trunk/packages/coq +XS-Vcs-Browser: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/trunk/ + +Package: coq +Architecture: any +Depends: ${shlibs:Depends}, ${misc:Depends}, ocaml-base-nox-${F:OCamlABI}, coq-libs (= ${source:Version}) +Recommends: coqide | proofgeneral-coq +Suggests: ocaml-nox (>= 3.08), proofgeneral-coq, ledit, cle, coq-doc +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}, ${misc: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 +Depends: ${misc:Depends} +Recommends: coq (>= 8.0) +Conflicts: coq (<< 8.0), coq-doc (<= 8.0pl1.0-2) +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. diff --git a/debian/copyright b/debian/copyright new file mode 100644 index 00000000..f0856000 --- /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.dirs b/debian/coq-libs.dirs new file mode 100644 index 00000000..aadcf27a --- /dev/null +++ b/debian/coq-libs.dirs @@ -0,0 +1,2 @@ +usr/share/doc/coq-libs +usr/share/doc/coq diff --git a/debian/coq-libs.doc-base b/debian/coq-libs.doc-base new file mode 100644 index 00000000..1a62a262 --- /dev/null +++ b/debian/coq-libs.doc-base @@ -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-libs/html/index.html +Files: /usr/share/doc/coq-libs/html/*.html diff --git a/debian/coq-libs.install b/debian/coq-libs.install new file mode 100644 index 00000000..653e2b54 --- /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..2a554d36 --- /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..59bcb594 --- /dev/null +++ b/debian/coq.install @@ -0,0 +1,18 @@ +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/lib/coq/*.cma +usr/lib/coq/*.cmxa +usr/lib/coq/tools/coqdoc/ +usr/share/emacs/site-lisp/coq/* +usr/share/man/man1/c* +usr/share/man/man1/gallina.1 +usr/share/texmf/tex/latex/misc/* +usr/share/emacs/site-lisp/coqdoc.sty usr/share/texmf/tex/latex/misc/ diff --git a/debian/coq.menu b/debian/coq.menu new file mode 100644 index 00000000..0552ecb8 --- /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="Applications/Science/Mathematics" title="Coq" diff --git a/debian/coq.xpm b/debian/coq.xpm new file mode 100644 index 00000000..fe188d02 --- /dev/null +++ b/debian/coq.xpm @@ -0,0 +1,52 @@ +/* XPM */ +static char * coq_xpm[] = { +"32 32 17 1", +" c None", +". c #5A261F", +"+ c #342A2C", +"@ c #BF381C", +"# c #EAB48F", +"$ c #B9ADA8", +"% c #F2D3B6", +"& c #D35E3A", +"* c #FCFDF9", +"= c #A59082", +"- c #CA7852", +"; c #220C08", +"> c #837671", +", c #923827", +"' c #6A4D4B", +") c #E19667", +"! c #996252", +" ", +" ", +" .+ ", +" @@#$$ ", +" @%%@&*= ", +" %#@@-**; ", +" =@@@>*** ", +" $;@,**** ", +" ;*****' ", +" $%*****$ = ", +" %*********; **$ ", +" $************ ;***+ ", +" =*************+**+****%. ", +" %**************'***%*#=+ ", +" =%%%******%%*%#**##*%))). ", +" >%%%%#%%**%%%%%#%%##--#- ", +" ##%%!%%%%%#%#%##-',-)-; ", +" +##%#!-)##))-&&,,.,--! ", +" ')##);,@.,));...;,'; ", +" !--)-&;;..&.;.;,'!; ", +" $,&,,@..;,;.;,,!; ", +" @.;,-,,,,,,,' ", +" ',,...;.;; ", +" ..;;.;. ", +" ;;;;+ ", +" ;' + ", +" ;> + ", +" #'.-'')= ", +" '+> $! ", +" ", +" ", +" "}; 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..8c1a0c60 --- /dev/null +++ b/debian/coqide.desktop @@ -0,0 +1,9 @@ +[Desktop Entry] +Encoding=UTF-8 +Name=CoqIDE Proof Assistant +Comment=Graphical interface for the Coq proof assistant +Exec=coqide +Type=Application +Categories=Development;Science;Math;IDE;GTK; +Terminal=false +Icon=coq 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..f214e01c --- /dev/null +++ b/debian/coqide.install @@ -0,0 +1,4 @@ +usr/bin/coqide* +usr/lib/coq/ide/coq.png +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..93feca90 --- /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="Applications/Science/Mathematics" 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..333bbd2f --- /dev/null +++ b/debian/patches/00list @@ -0,0 +1,7 @@ +camlp5 +coqdoc_stdlib +browser +makefile +no-complexity-test +configure +cmxa-install diff --git a/debian/patches/browser.dpatch b/debian/patches/browser.dpatch new file mode 100755 index 00000000..ba55f3de --- /dev/null +++ b/debian/patches/browser.dpatch @@ -0,0 +1,19 @@ +#! /bin/sh /usr/share/dpatch/dpatch-run +## browser.dpatch by Samuel Mimram <smimram@debian.org> +## +## All lines beginning with `## DP:' are a description of the patch. +## DP: Use the default Debian browser for help. + +@DPATCH@ +diff -urNad coq-8.0pl3+8.1alpha~/lib/options.ml coq-8.0pl3+8.1alpha/lib/options.ml +--- coq-8.0pl3+8.1alpha~/lib/options.ml 2005-12-26 20:07:21.000000000 +0000 ++++ coq-8.0pl3+8.1alpha/lib/options.ml 2006-04-29 16:06:20.000000000 +0000 +@@ -117,7 +117,4 @@ + "\" must contain exactly one placeholder \"%s\".") + else pre,post + with +- Not_found -> +- if Sys.os_type = "Win32" +- then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", "" +- else "netscape -remote \"OpenURL(", ")\"" ++ Not_found -> "/usr/bin/x-www-browser ", "" diff --git a/debian/patches/camlp5.dpatch b/debian/patches/camlp5.dpatch new file mode 100755 index 00000000..2c5b8643 --- /dev/null +++ b/debian/patches/camlp5.dpatch @@ -0,0 +1,563 @@ +#! /bin/sh /usr/share/dpatch/dpatch-run +## camlp5.dpatch by Samuel Mimram <smimram@debian.org> +## +## All lines beginning with `## DP:' are a description of the patch. +## DP: Use camlp5 instead of the new camlp4 for coq. + +@DPATCH@ +diff -urNad coq-8.1.pl1+dfsg~/Makefile coq-8.1.pl1+dfsg/Makefile +--- coq-8.1.pl1+dfsg~/Makefile 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/Makefile 2007-08-24 10:56:52.000000000 +0000 +@@ -1504,11 +1504,11 @@ + + # BEFOREDEPEND+= parsing/pcoq.ml parsing/extend.ml + +-# File using pa_ifdef and only necessary for parsing ml files ++# File using pa_macro and only necessary for parsing ml files + + parsing/q_coqast.cmo: parsing/q_coqast.ml4 + $(SHOW)'OCAMLC4 $<' +- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo $(CAMLP4COMPAT) -impl" -c -impl $< ++ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo $(CAMLP4COMPAT) -impl" -c -impl $< + + # toplevel/mltop.ml4 (ifdef Byte) + +@@ -1522,11 +1522,11 @@ + + toplevel/mltop.byteml: toplevel/mltop.ml4 + $(SHOW)'CAMLP4O $<' +- $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo -DByte -impl $< > $@ || rm -f $@ ++ $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo pr_o.cmo -DByte -impl $< > $@ || rm -f $@ + + toplevel/mltop.optml: toplevel/mltop.ml4 + $(SHOW)'CAMLP4O $<' +- $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo -impl $< > $@ || rm -f $@ ++ $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo pr_o.cmo -impl $< > $@ || rm -f $@ + + ML4FILES += toplevel/mltop.ml4 + +@@ -1571,11 +1571,11 @@ + + lib/compat.cmo: lib/compat.ml4 + $(SHOW)'OCAMLC4 $<' +- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo -impl" -c -impl $< ++ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo -impl" -c -impl $< + + lib/compat.cmx: lib/compat.ml4 + $(SHOW)'OCAMLOPT $<' +- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo -impl" -c -impl $< ++ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo -impl" -c -impl $< + + # files compiled with camlp4 because of streams syntax + +@@ -1654,7 +1654,7 @@ + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $< + + %.ml: %.ml4 +- $(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@ ++ $(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@ + + #.v.vo: + # $(BOOTCOQTOP) -compile $* +diff -urNad coq-8.1.pl1+dfsg~/Makefile.dep coq-8.1.pl1+dfsg/Makefile.dep +--- coq-8.1.pl1+dfsg~/Makefile.dep 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/Makefile.dep 2007-08-24 10:56:52.000000000 +0000 +@@ -12,4 +12,4 @@ + include .depend.camlp4 + + .ml4.ml: +- $(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@ ++ $(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@ +diff -urNad coq-8.1.pl1+dfsg~/config/Makefile.template coq-8.1.pl1+dfsg/config/Makefile.template +--- coq-8.1.pl1+dfsg~/config/Makefile.template 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/config/Makefile.template 2007-08-24 10:56:52.000000000 +0000 +@@ -62,7 +62,7 @@ + CAMLMKTOP="CAMLMKTOPEXEC" + + # Caml flags +-CAMLFLAGS=CAMLANNOTATEFLAG ++CAMLFLAGS=-rectypes CAMLANNOTATEFLAG + + # Compilation debug flag + CAMLDEBUG=COQDEBUGFLAG +@@ -80,8 +80,8 @@ + BEST=BESTCOMPILER + + # For Camlp4 use +-P4=$(COQTOP)/bin/$(ARCH)/call_camlp4 -I $(COQTOP)/src/parsing +-P4DEP=$(COQTOP)/bin/$(ARCH)/camlp4dep ++P4=$(COQTOP)/bin/$(ARCH)/call_camlp5 -I $(COQTOP)/src/parsing ++P4DEP=$(COQTOP)/bin/$(ARCH)/camlp5dep + + # Your architecture + # Can be obtain by UNIX command arch +diff -urNad coq-8.1.pl1+dfsg~/configure coq-8.1.pl1+dfsg/configure +--- coq-8.1.pl1+dfsg~/configure 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/configure 2007-08-24 10:56:52.000000000 +0000 +@@ -78,7 +78,7 @@ + ocamllexexec=ocamllex + ocamlyaccexec=ocamlyacc + ocamlmktopexec=ocamlmktop +-camlp4oexec=camlp4o ++camlp4oexec=camlp5o + + + coq_debug_flag= +@@ -153,7 +153,7 @@ + arch=$2 + shift;; + -opt|--opt) bytecamlc=ocamlc.opt +- camlp4oexec=camlp4o # can't add .opt since dyn load'll be required ++ camlp4oexec=camlp5o # can't add .opt since dyn load'll be required + nativecamlc=ocamlopt.opt;; + -fsets|--fsets) fsets_opt=yes + case "$2" in +@@ -297,7 +297,7 @@ + ocamllexexec=$CAMLBIN/ocamllex + ocamlyaccexec=$CAMLBIN/ocamlyacc + camlmktopexec=$CAMLBIN/ocamlmktop +- camlp4oexec=$CAMLBIN/camlp4o ++ camlp4oexec=$CAMLBIN/camlp5o + esac + + if test ! -f "$CAMLC" ; then +@@ -362,10 +362,10 @@ + + #case $OS in + # Win32) +- CAMLP4LIB=+camlp4 ++ CAMLP4LIB=+camlp5 + # ;; + # *) +-# CAMLP4LIB=${CAMLLIB}/camlp4 ++# CAMLP4LIB=${CAMLLIB}/camlp5 + #esac + + # OS dependent libraries +@@ -615,7 +615,7 @@ + ESCLIBDIR="`VAR=LIBDIR escape_var`" + ESCCAMLDIR="`VAR=CAMLBIN escape_var`" + ESCCAMLLIB="`VAR=CAMLLIB escape_var`" +-ESCCAMLP4LIB="$ESCCAMLLIB"/camlp4 ++ESCCAMLP4LIB="$ESCCAMLLIB"/camlp5 + + mlconfig_file="$COQSRC/config/coq_config.ml" + rm -f $mlconfig_file +@@ -739,8 +739,8 @@ + + if test "$coq_debug_flag" = "-g" ; then + rm -f $OCAMLDEBUGCOQ +- if [ "$CAMLP4LIB" = "+camlp4" ] ; then +- CAMLP4LIBFORCAMLDEBUG=$CAMLLIB/camlp4 ++ if [ "$CAMLP4LIB" = "+camlp5" ] ; then ++ CAMLP4LIBFORCAMLDEBUG=$CAMLLIB/camlp5 + else + CAMLP4LIBFORCAMLDEBUG=$CAMLP4LIB + fi +diff -urNad coq-8.1.pl1+dfsg~/dev/ocamldebug-coq.template coq-8.1.pl1+dfsg/dev/ocamldebug-coq.template +--- coq-8.1.pl1+dfsg~/dev/ocamldebug-coq.template 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/dev/ocamldebug-coq.template 2007-08-24 10:56:52.000000000 +0000 +@@ -7,7 +7,7 @@ + export COQTH=$COQLIB/theories + CAMLBIN=CAMLBINDIRECTORY + OCAMLDEBUG=$CAMLBIN/ocamldebug +-export CAMLP4LIB=`$CAMLBIN/camlp4 -where` ++export CAMLP4LIB=`$CAMLBIN/camlp5 -where` + + exec $OCAMLDEBUG \ + -I $CAMLP4LIB \ +diff -urNad coq-8.1.pl1+dfsg~/lib/compat.ml4 coq-8.1.pl1+dfsg/lib/compat.ml4 +--- coq-8.1.pl1+dfsg~/lib/compat.ml4 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/lib/compat.ml4 2007-08-24 10:56:52.000000000 +0000 +@@ -11,6 +11,7 @@ + (* IFDEF not available in 3.06; use ifdef instead *) + + (* type loc is different in 3.08 *) ++(* + ifdef OCAML_308 then + module M = struct + type loc = Token.flocation +@@ -32,8 +33,9 @@ + let make_loc x = x + let unloc x = x + end ++*) + +-type loc = M.loc +-let dummy_loc = M.dummy_loc +-let unloc = M.unloc +-let make_loc = M.make_loc ++type loc = Stdpp.location ++let dummy_loc = Stdpp.dummy_loc ++let make_loc = Stdpp.make_loc ++let unloc loc = Stdpp.first_pos loc, Stdpp.last_pos loc +diff -urNad coq-8.1.pl1+dfsg~/lib/util.ml coq-8.1.pl1+dfsg/lib/util.ml +--- coq-8.1.pl1+dfsg~/lib/util.ml 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/lib/util.ml 2007-08-24 10:56:52.000000000 +0000 +@@ -34,7 +34,7 @@ + let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s) + let join_loc loc1 loc2 = + if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc +- else (fst loc1, snd loc2) ++ else Stdpp.encl_loc loc1 loc2 + + (* Like Exc_located, but specifies the outermost file read, the filename + associated to the location of the error, and the error itself. *) +diff -urNad coq-8.1.pl1+dfsg~/parsing/argextend.ml4 coq-8.1.pl1+dfsg/parsing/argextend.ml4 +--- coq-8.1.pl1+dfsg~/parsing/argextend.ml4 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/parsing/argextend.ml4 2007-08-24 10:56:52.000000000 +0000 +@@ -12,7 +12,7 @@ + open Q_util + open Q_coqast + +-let join_loc (deb1,_) (_,fin2) = (deb1,fin2) ++let join_loc = Util.join_loc + let loc = Util.dummy_loc + let default_loc = <:expr< Util.dummy_loc >> + +@@ -226,7 +226,7 @@ + let t, g = interp_entry_name loc e sep in (g, Some (s,t)) + | s = STRING -> + if String.length s > 0 && Util.is_letter s.[0] then +- Pcoq.lexer.Token.using ("", s); ++ Pcoq.lexer.Token.tok_using ("", s); + (<:expr< (Gramext.Stoken (Lexer.terminal $str:s$)) >>, None) + ] ] + ; +diff -urNad coq-8.1.pl1+dfsg~/parsing/egrammar.mli coq-8.1.pl1+dfsg/parsing/egrammar.mli +--- coq-8.1.pl1+dfsg~/parsing/egrammar.mli 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/parsing/egrammar.mli 2007-08-24 10:56:52.000000000 +0000 +@@ -45,7 +45,7 @@ + type grammar_tactic_production = + | TacTerm of string + | TacNonTerm of +- loc * (Token.t Gramext.g_symbol * Genarg.argument_type) * string option ++ loc * ((string * string) Gramext.g_symbol * Genarg.argument_type) * string option + + val extend_tactic_grammar : + string -> grammar_tactic_production list list -> unit +@@ -61,7 +61,7 @@ + (* + val reset_extend_grammars_v8 : unit -> unit + *) +-val interp_entry_name : int -> string -> entry_type * Token.t Gramext.g_symbol ++val interp_entry_name : int -> string -> entry_type * (string * string) Gramext.g_symbol + + val recover_notation_grammar : + notation -> (precedence * tolerability list) -> notation_grammar +diff -urNad coq-8.1.pl1+dfsg~/parsing/pcoq.ml4 coq-8.1.pl1+dfsg/parsing/pcoq.ml4 +--- coq-8.1.pl1+dfsg~/parsing/pcoq.ml4 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/parsing/pcoq.ml4 2007-08-24 10:56:52.000000000 +0000 +@@ -30,20 +30,23 @@ + lexer. B.B. *) + + let lexer = { +- Token.func = Lexer.func; +- Token.using = Lexer.add_token; +- Token.removing = (fun _ -> ()); +- Token.tparse = Lexer.tparse; +- Token.text = Lexer.token_text } ++ Token.tok_func = Lexer.func; ++ Token.tok_using = Lexer.add_token; ++ Token.tok_removing = (fun _ -> ()); ++ Token.tok_match = Token.default_match; ++ (* Token.parse = Lexer.tparse; *) ++ Token.tok_comm = None; ++ Token.tok_text = Lexer.token_text } + + module L = + struct ++ type te = string * string + let lexer = lexer + end + + (* The parser of Coq *) + +-module G = Grammar.Make(L) ++module G = Grammar.GMake(L) + + let grammar_delete e rls = + List.iter +@@ -95,7 +98,7 @@ + | ByGrammar of + grammar_object G.Entry.e * Gramext.position option * + (string option * Gramext.g_assoc option * +- (Token.t Gramext.g_symbol list * Gramext.g_action) list) list ++ ((string * string) Gramext.g_symbol list * Gramext.g_action) list) list + | ByGEXTEND of (unit -> unit) * (unit -> unit) + + let camlp4_state = ref [] +diff -urNad coq-8.1.pl1+dfsg~/parsing/pcoq.mli coq-8.1.pl1+dfsg/parsing/pcoq.mli +--- coq-8.1.pl1+dfsg~/parsing/pcoq.mli 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/parsing/pcoq.mli 2007-08-24 10:56:52.000000000 +0000 +@@ -20,9 +20,9 @@ + + (* The lexer and parser of Coq. *) + +-val lexer : Token.lexer ++val lexer : (string * string) Token.glexer + +-module Gram : Grammar.S with type te = Token.t ++module Gram : Grammar.S with type te = (string * string) + + (* The superclass of all grammar entries *) + type grammar_object +@@ -42,7 +42,7 @@ + val grammar_extend : + grammar_object Gram.Entry.e -> Gramext.position option -> + (string option * Gramext.g_assoc option * +- (Token.t Gramext.g_symbol list * Gramext.g_action) list) list ++ ((string * string) Gramext.g_symbol list * Gramext.g_action) list) list + -> unit + + val remove_grammars : int -> unit +@@ -210,7 +210,7 @@ + (* Binding entry names to campl4 entries *) + + val symbol_of_production : Gramext.g_assoc option -> constr_entry -> +- bool -> constr_production_entry -> Token.t Gramext.g_symbol ++ bool -> constr_production_entry -> (string * string) Gramext.g_symbol + + (* Registering/resetting the level of an entry *) + +diff -urNad coq-8.1.pl1+dfsg~/parsing/ppconstr.ml coq-8.1.pl1+dfsg/parsing/ppconstr.ml +--- coq-8.1.pl1+dfsg~/parsing/ppconstr.ml 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/parsing/ppconstr.ml 2007-08-24 10:56:52.000000000 +0000 +@@ -95,9 +95,9 @@ + let pr_delimiters key strm = + strm ++ str ("%"^key) + +-let pr_located pr ((b,e),x) = +- if Options.do_translate() && (b,e)<>dummy_loc then +- let (b,e) = unloc (b,e) in ++let pr_located pr (loc,x) = ++ if Options.do_translate() && loc<>dummy_loc then ++ let (b,e) = unloc loc in + comment b ++ pr x ++ comment e + else pr x + +@@ -142,7 +142,7 @@ + | CHole _ -> mt () + | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t + +-let pr_lident (b,_ as loc,id) = ++let pr_lident (loc,id) = + if loc <> dummy_loc then + let (b,_) = unloc loc in + pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id) +diff -urNad coq-8.1.pl1+dfsg~/parsing/ppvernac.ml coq-8.1.pl1+dfsg/parsing/ppvernac.ml +--- coq-8.1.pl1+dfsg~/parsing/ppvernac.ml 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/parsing/ppvernac.ml 2007-08-24 10:56:52.000000000 +0000 +@@ -28,7 +28,7 @@ + + let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr + +-let pr_lident (b,_ as loc,id) = ++let pr_lident (loc,id) = + if loc <> dummy_loc then + let (b,_) = unloc loc in + pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id) +@@ -39,7 +39,7 @@ + + let pr_fqid fqid = str (string_of_fqid fqid) + +-let pr_lfqid (_,_ as loc,fqid) = ++let pr_lfqid (loc,fqid) = + if loc <> dummy_loc then + let (b,_) = unloc loc in + pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid) +diff -urNad coq-8.1.pl1+dfsg~/parsing/q_coqast.ml4 coq-8.1.pl1+dfsg/parsing/q_coqast.ml4 +--- coq-8.1.pl1+dfsg~/parsing/q_coqast.ml4 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/parsing/q_coqast.ml4 2007-08-24 10:56:52.000000000 +0000 +@@ -22,10 +22,8 @@ + let anti loc x = + let e = + let loc = +- ifdef OCAML_308 then +- loc +- else +- (1, snd loc - fst loc) ++ loc ++ (* (1, snd loc - fst loc) *) + in <:expr< $lid:purge_str x$ >> + in + <:expr< $anti:e$ >> +diff -urNad coq-8.1.pl1+dfsg~/parsing/q_util.ml4 coq-8.1.pl1+dfsg/parsing/q_util.ml4 +--- coq-8.1.pl1+dfsg~/parsing/q_util.ml4 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/parsing/q_util.ml4 2007-08-24 10:56:52.000000000 +0000 +@@ -37,18 +37,18 @@ + List.fold_right + (fun e1 e2 -> + let e1 = f e1 in +- let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in ++ let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in + <:expr< [$e1$ :: $e2$] >>) + l (let loc = dummy_loc in <:expr< [] >>) + + let mlexpr_of_pair m1 m2 (a1,a2) = + let e1 = m1 a1 and e2 = m2 a2 in +- let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in ++ let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in + <:expr< ($e1$, $e2$) >> + + let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)= + let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 in +- let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e3)) in ++ let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in + <:expr< ($e1$, $e2$, $e3$) >> + + (* We don't give location for tactic quotation! *) +diff -urNad coq-8.1.pl1+dfsg~/parsing/tacextend.ml4 coq-8.1.pl1+dfsg/parsing/tacextend.ml4 +--- coq-8.1.pl1+dfsg~/parsing/tacextend.ml4 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/parsing/tacextend.ml4 2007-08-24 10:56:52.000000000 +0000 +@@ -13,7 +13,7 @@ + open Q_coqast + open Argextend + +-let join_loc (deb1,_) (_,fin2) = (deb1,fin2) ++let join_loc = Util.join_loc + let loc = Util.dummy_loc + let default_loc = <:expr< Util.dummy_loc >> + +diff -urNad coq-8.1.pl1+dfsg~/parsing/vernacextend.ml4 coq-8.1.pl1+dfsg/parsing/vernacextend.ml4 +--- coq-8.1.pl1+dfsg~/parsing/vernacextend.ml4 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/parsing/vernacextend.ml4 2007-08-24 10:56:52.000000000 +0000 +@@ -13,7 +13,7 @@ + open Q_coqast + open Argextend + +-let join_loc (deb1,_) (_,fin2) = (deb1,fin2) ++let join_loc = Util.join_loc + let loc = Util.dummy_loc + let default_loc = <:expr< Util.dummy_loc >> + +diff -urNad coq-8.1.pl1+dfsg~/scripts/coqmktop.ml coq-8.1.pl1+dfsg/scripts/coqmktop.ml +--- coq-8.1.pl1+dfsg~/scripts/coqmktop.ml 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/scripts/coqmktop.ml 2007-08-24 10:57:13.000000000 +0000 +@@ -32,7 +32,7 @@ + + (* 3. Toplevel objects *) + let camlp4topobjs = +- ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"] ++ ["camlp5_top.cma"; "camlp5o.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"] + let topobjs = camlp4topobjs + + let gramobjs = [] +@@ -285,12 +285,12 @@ + (* native code *) + if !top then failwith "no custom toplevel in native code !"; + let ocamloptexec = Filename.concat Coq_config.camldir "ocamlopt" in +- (if !caml_inline_0 then ocamloptexec^" -linkall"^" -inline 0" else ocamloptexec^" -linkall") ++ (if !caml_inline_0 then ocamloptexec^" -linkall -rectypes"^" -inline 0" else ocamloptexec^" -linkall -rectypes") + end else + (* bytecode (we shunt ocamlmktop script which fails on win32) *) + let ocamlmktoplib = " toplevellib.cma" in + let ocamlcexec = Filename.concat Coq_config.camldir "ocamlc" in +- let ocamlccustom = ocamlcexec^" -custom -linkall" in ++ let ocamlccustom = ocamlcexec^" -custom -linkall -rectypes" in + (if !top then ocamlccustom^ocamlmktoplib else ocamlccustom) + in + (* files to link *) +diff -urNad coq-8.1.pl1+dfsg~/tools/coq_makefile.ml4 coq-8.1.pl1+dfsg/tools/coq_makefile.ml4 +--- coq-8.1.pl1+dfsg~/tools/coq_makefile.ml4 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/tools/coq_makefile.ml4 2007-08-24 10:56:52.000000000 +0000 +@@ -175,7 +175,7 @@ + | _ :: r -> var_aux r + in + section "Variables definitions."; +- print "CAMLP4LIB=`camlp4 -where`\n"; ++ print "CAMLP4LIB=`camlp5 -where`\n"; + (* print "MAKE=make \"COQBIN=$(COQBIN)\" \"OPT=$(OPT)\"\n"; *) + print "COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\ + -I $(COQTOP)/library -I $(COQTOP)/parsing \\ +@@ -204,8 +204,8 @@ + print "CAMLOPTLINK=ocamlopt\n"; + print "COQDEP=$(COQBIN)coqdep -c\n"; + print "GRAMMARS=grammar.cma\n"; +- print "CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo\n"; +- print "PP=-pp \"camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"; ++ print "CAMLP4EXTEND=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; ++ print "PP=-pp \"camlp5o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"; + var_aux l; + print "\n" + +diff -urNad coq-8.1.pl1+dfsg~/toplevel/metasyntax.ml coq-8.1.pl1+dfsg/toplevel/metasyntax.ml +--- coq-8.1.pl1+dfsg~/toplevel/metasyntax.ml 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/toplevel/metasyntax.ml 2007-08-24 10:56:52.000000000 +0000 +@@ -28,7 +28,7 @@ + (**********************************************************************) + (* Tokens *) + +-let cache_token (_,s) = Pcoq.lexer.Token.using ("", s) ++let cache_token (_,s) = Pcoq.lexer.Token.tok_using ("", s) + + let (inToken, outToken) = + declare_object {(default_object "TOKEN") with +diff -urNad coq-8.1.pl1+dfsg~/toplevel/mltop.ml4 coq-8.1.pl1+dfsg/toplevel/mltop.ml4 +--- coq-8.1.pl1+dfsg~/toplevel/mltop.ml4 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/toplevel/mltop.ml4 2007-08-24 10:56:52.000000000 +0000 +@@ -98,7 +98,7 @@ + str s; str" to Coq code." >]) + (* TO DO: .cma loading without toplevel *) + | WithoutTop -> +- ifdef Byte then ++ IFDEF Byte THEN + let _,gname = where_in_path !coq_mlpath_copy s in + try + Dynlink.loadfile gname; +@@ -108,7 +108,7 @@ + [Filename.dirname gname] + with | Dynlink.Error a -> + errorlabstrm "Mltop.load_object" [< str (Dynlink.error_message a) >] +- else () ++ ELSE () END + | Native -> + errorlabstrm "Mltop.no_load_object" + [< str"Loading of ML object file forbidden in a native Coq" >] +diff -urNad coq-8.1.pl1+dfsg~/toplevel/toplevel.ml coq-8.1.pl1+dfsg/toplevel/toplevel.ml +--- coq-8.1.pl1+dfsg~/toplevel/toplevel.ml 2007-08-24 10:56:51.000000000 +0000 ++++ coq-8.1.pl1+dfsg/toplevel/toplevel.ml 2007-08-24 10:56:52.000000000 +0000 +@@ -139,16 +139,16 @@ + + (* Functions to report located errors in a file. *) + +-let print_location_in_file s inlibrary fname (bp,ep) = ++let print_location_in_file s inlibrary fname loc = + let errstrm = (str"Error while reading " ++ str s ++ str" :" ++ fnl ()) in +- if (bp,ep) = dummy_loc then ++ if loc = dummy_loc then + (errstrm ++ str", unknown location." ++ fnl ()) + else + if inlibrary then + (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++ +- str" characters " ++ Cerrors.print_loc (bp,ep) ++ fnl ()) ++ str" characters " ++ Cerrors.print_loc loc ++ fnl ()) + else +- let (bp,ep) = unloc (bp,ep) in ++ let (bp,ep) = unloc loc in + let ic = open_in fname in + let rec line_of_pos lin bol cnt = + if cnt < bp then +@@ -172,15 +172,16 @@ + str(String.sub ib.str (bp-ib.start) (ep-bp)) ++ fnl ()) + | None -> (mt ()) + +-let valid_loc dloc (b,e) = +- (b,e) <> dummy_loc ++let valid_loc dloc loc = ++ let b, e = unloc loc in ++ loc <> dummy_loc + & match dloc with +- | Some (bd,ed) -> bd<=b & e<=ed ++ | Some dloc -> let bd,ed = unloc dloc in bd<=b & e<=ed + | _ -> true + +-let valid_buffer_loc ib dloc (b,e) = +- valid_loc dloc (b,e) & +- let (b,e) = unloc (b,e) in b-ib.start >= 0 & e-ib.start < ib.len & b<=e ++let valid_buffer_loc ib dloc loc = ++ valid_loc dloc loc & ++ let (b,e) = unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e + + (*s The Coq prompt is the name of the focused proof, if any, and "Coq" + otherwise. We trap all exceptions to prevent the error message printing diff --git a/debian/patches/cmxa-install.dpatch b/debian/patches/cmxa-install.dpatch new file mode 100755 index 00000000..7e8d2ffb --- /dev/null +++ b/debian/patches/cmxa-install.dpatch @@ -0,0 +1,23 @@ +#! /bin/sh /usr/share/dpatch/dpatch-run +## cmxa-install.dpatch by Samuel Mimram <smimram@debian.org> +## +## All lines beginning with `## DP:' are a description of the patch. +## DP: .cmxa are not generated on non-native archs, so don't install them. + +@DPATCH@ +diff -urNad coq-8.1+dfsg~/Makefile coq-8.1+dfsg/Makefile +--- coq-8.1+dfsg~/Makefile 2007-02-18 13:25:29.000000000 +0100 ++++ coq-8.1+dfsg/Makefile 2007-02-18 13:27:28.000000000 +0100 +@@ -1272,7 +1272,11 @@ + parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \ + parsing/highparsing.cma tactics/hightactics.cma contrib/contrib.cma + +-OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa) ++ifeq ($(BEST),opt) ++ OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa) ++else ++ OBJECTCMXA= ++endif + + install-library: + $(MKDIR) $(FULLCOQLIB) diff --git a/debian/patches/configure.dpatch b/debian/patches/configure.dpatch new file mode 100755 index 00000000..db3ef2a5 --- /dev/null +++ b/debian/patches/configure.dpatch @@ -0,0 +1,19 @@ +#! /bin/sh /usr/share/dpatch/dpatch-run +## configure.dpatch by Pierre Letouzey <pierre.letouzey@pps.jussieu.fr> +## +## All lines beginning with `## DP:' are a description of the patch. +## DP: Correctly detect whether ocamlopt is present or not. + +@DPATCH@ +diff -urNad coq-8.1+dfsg~/configure coq-8.1+dfsg/configure +--- coq-8.1+dfsg~/configure 2007-02-10 08:32:28.000000000 +0000 ++++ coq-8.1+dfsg/configure 2007-02-15 12:58:56.000000000 +0000 +@@ -340,7 +340,7 @@ + # do we have a native compiler: test of ocamlopt and its version + + if [ "$best_compiler" = "opt" ] ; then +- if test -e `which "$nativecamlc"` ; then ++ if test -e "`which $nativecamlc`" ; then + CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' ` + if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then + echo "native and bytecode compilers do not have the same version!"; fi diff --git a/debian/patches/coqdoc_stdlib.dpatch b/debian/patches/coqdoc_stdlib.dpatch new file mode 100755 index 00000000..fb618f56 --- /dev/null +++ b/debian/patches/coqdoc_stdlib.dpatch @@ -0,0 +1,19 @@ +#! /bin/sh /usr/share/dpatch/dpatch-run +## coqdoc_stdlib.dpatch by Samuel Mimram <smimram@debian.org> +## +## All lines beginning with `## DP:' are a description of the patch. +## DP: Add an option to coqdoc to be able to use a custom stdlib path in order +## DP: to be able to build the documentation before coqdoc is installed. + +@DPATCH@ +diff -urNad coq-8.0pl3+8.1beta~/doc/Makefile coq-8.0pl3+8.1beta/doc/Makefile +--- coq-8.0pl3+8.1beta~/doc/Makefile 2006-06-16 13:02:33.000000000 +0000 ++++ coq-8.0pl3+8.1beta/doc/Makefile 2006-06-16 13:19:11.000000000 +0000 +@@ -216,6 +216,7 @@ + mkdir stdlib/html + (cd stdlib/html;\ + $(COQDOC) -q --multi-index --html --glob-from $(GLOBDUMP)\ ++ --coqlib_path $(COQTOP) \ + -R $(COQTOP)/theories Coq $(COQTOP)/theories/*/*.v) + mv stdlib/html/index.html stdlib/index-body.html + diff --git a/debian/patches/makefile.dpatch b/debian/patches/makefile.dpatch new file mode 100755 index 00000000..b656a9bb --- /dev/null +++ b/debian/patches/makefile.dpatch @@ -0,0 +1,20 @@ +#! /bin/sh /usr/share/dpatch/dpatch-run +## makefile.dpatch by Samuel Mimram <smimram@debian.org> +## +## All lines beginning with `## DP:' are a description of the patch. +## DP: Do not use ocamlopt to test grammar.cma, we don't want to use ocamlopt +## DP: when compiling on non-native archs. + +@DPATCH@ +diff -urNad coq-8.0pl3+8.1alpha~/Makefile coq-8.0pl3+8.1alpha/Makefile +--- coq-8.0pl3+8.1alpha~/Makefile 2006-04-07 15:08:12.000000000 +0000 ++++ coq-8.0pl3+8.1alpha/Makefile 2006-04-30 11:41:09.000000000 +0000 +@@ -1401,7 +1401,7 @@ + parsing/grammar.cma: $(GRAMMARCMO) + $(SHOW)'Testing $@' + @touch test.ml4 +- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar ++ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar + @rm -f test-grammar test.* + $(SHOW)'OCAMLC -a $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@ diff --git a/debian/patches/no-complexity-test.dpatch b/debian/patches/no-complexity-test.dpatch new file mode 100644 index 00000000..bf89f1f7 --- /dev/null +++ b/debian/patches/no-complexity-test.dpatch @@ -0,0 +1,21 @@ +#! /bin/sh /usr/share/dpatch/dpatch-run +## no-complexity-test.dpatch by Julien Cristau <julien.cristau@ens-lyon.org> +## +## All lines beginning with `## DP:' are a description of the patch. +## DP: Don't run complexity tests, they are far too fragile. + +@DPATCH@ +diff -urNad coq-8.1gamma~/test-suite/check coq-8.1gamma/test-suite/check +--- coq-8.1gamma~/test-suite/check 2006-11-03 14:07:27.000000000 +0100 ++++ coq-8.1gamma/test-suite/check 2006-11-23 15:19:49.000000000 +0100 +@@ -145,8 +145,8 @@ + test_parser parser + echo "Interactive tests" + test_interactive interactive +-echo "Complexity tests" +-test_complexity complexity ++echo "Skipping complexity tests" ++#test_complexity complexity + echo "Module tests" + $coqtop -compile modules/Nat + $coqtop -compile modules/plik diff --git a/debian/purify_tarball b/debian/purify_tarball new file mode 100755 index 00000000..4682a21c --- /dev/null +++ b/debian/purify_tarball @@ -0,0 +1,26 @@ +#!/bin/sh + +set -e + +CURDIR=`pwd` +ORIG=$1 +WORKDIR=`dirname $ORIG` +ORIGFILE=`basename $ORIG` +VERSION=`echo "$ORIGFILE" | sed "s/^coq-\([0-9\.a-z]\+\)\.tar\.gz$/\1/"` + +cd $WORKDIR + +tar zxf $ORIGFILE + +rm -rf coq-$VERSION/doc/common +rm -rf coq-$VERSION/doc/faq +rm -rf coq-$VERSION/doc/RecTutorial +rm -rf coq-$VERSION/doc/refman +rm -rf coq-$VERSION/doc/rt +rm -rf coq-$VERSION/doc/tools +rm -rf coq-$VERSION/doc/tutorial + +tar zcf coq_$VERSION+dfsg.orig.tar.gz coq-$VERSION/ +rm -rf coq-$VERSION + +cd $CURDIR diff --git a/debian/rules b/debian/rules new file mode 100755 index 00000000..22cd9dc0 --- /dev/null +++ b/debian/rules @@ -0,0 +1,144 @@ +#!/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) + +OCAMLABI := $(shell ocamlc -version) + +CONFIGUREOPTS := --arch Linux --prefix /usr --mandir /usr/share/man --emacslib /usr/share/emacs/site-lisp/coq --reals all --fsets 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 \ + && sed -i -e 's/best = "opt"/best = "byte"/' config/coq_config.ml \ + && $(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 + if [ -e opt-stamp ]; then \ + $(MAKE) BEST=opt glob.dump; \ + else \ + $(MAKE) BEST=byte HASCOQIDE=byte glob.dump; \ + fi + cp tools/coqdoc/coqdoc.sty doc/stdlib/ + $(MAKE) -C doc stdlib/html/index.html + touch build-stamp + +clean: unpatch + dh_testdir + dh_testroot + rm -f build-stamp configure-stamp opt-stamp + + [ ! -f config/Makefile ] || $(MAKE) clean + [ ! -f config/Makefile ] || $(MAKE) archclean + rm -f bin/* + rm -f tools/coqdoc/*.cm[oi] + rm -f config/coq_config.ml config/Makefile test-suite/check.log + rm -f dev/ocamldebug-v7 + rm -f ide/undo.mli glob.dump + rm -f test-suite/modules/*.vo + + 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 + if [ -e opt-stamp ]; then \ + strip -R .note -R .comment $ $(COQPREF)/usr/bin/coqc; \ + strip -R .note -R .comment $(COQPREF)/usr/bin/coqmktop; \ + fi + 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 + + cp -r doc/stdlib/html debian/coq-libs/usr/share/doc/coq-libs/ + cd debian/coq-libs/usr/share/doc/coq; ln -s ../coq-libs/html stdlib + + # 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_installtex + dh_desktop + dh_link + dh_compress + dh_fixperms + dh_installdeb + dh_shlibdeps + dh_gencontrol -- -VF:OCamlABI="$(OCAMLABI)" + 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..45c97702 --- /dev/null +++ b/debian/watch @@ -0,0 +1,2 @@ +version=3 +ftp://ftp.inria.fr/INRIA/coq/current/coq-([0-9a-z\.]*)\.tar\.gz debian uupdate |