diff options
41 files changed, 1698 insertions, 0 deletions
diff --git a/debian/NEWS b/debian/NEWS new file mode 100644 index 00000000..b0d1db54 --- /dev/null +++ b/debian/NEWS @@ -0,0 +1,8 @@ +coq (8.2~rc2+dfsg-1) experimental; urgency=low + + The Coq library for programming in OCaml is now in its own binary + package, libcoq-ocaml-dev, along with coqmktop. The theories have been + moved from coq-libs to the more expressive name coq-theories. + + -- Stéphane Glondu <glondu@debian.org> Mon, 02 Feb 2009 09:48:03 +0100 + diff --git a/debian/README.Debian b/debian/README.Debian new file mode 100644 index 00000000..7e9997a1 --- /dev/null +++ b/debian/README.Debian @@ -0,0 +1,20 @@ +-------------------------- ++ Coq package for Debian + +-------------------------- + +Binary (in)compatibility +------------------------ +The compiled libraries of Coq (the *.vo) are not expected to be backward or +forward 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 + - a readline editor, such as ledit or rlwrap (or anything that provides the + readline-editor virtual packages); + - or the Proof-General (x)emacs mode, available in the proofgeneral-coq + package. + +However, we recommend you to use the CoqIde GTK+ interface provided in coqide. diff --git a/debian/README.source b/debian/README.source new file mode 100644 index 00000000..ab1f26cd --- /dev/null +++ b/debian/README.source @@ -0,0 +1,56 @@ +-------------------------- ++ Coq package for Debian + +-------------------------- + + +Packaging a new upstream version +-------------------------------- + +Coq documentation may be distributed only subject to the terms and +conditions set forth in the Open Publication License, v1.0 or later, +which is not DFSG-compliant. See: + + http://lists.debian.org/debian-legal/2004/03/msg00226.html + +Only coqdoc-generated documentation of the standard library is shipped +in main. The full documentation is shipped in non-free (as coq-doc +package). + +The script debian/purify_tarball removes non-DFSG content from an +upstream tarball. It should be run first when packaging a new upstream +version. The suffix "+dfsg" is used to being appended to upstream +version (the script will do it for you). + + +Patch system +------------ + +This source package is in format 3.0 (quilt). + +The quilt series, if any, is generated from the Git repository, using +dom-{apply,save}-patches, from the dh-ocaml (>= 0.5) package. Please +refer to the appendix about Git in the Debian OCaml Packaging Policy +(from the same package). + + +Version Control System +---------------------- + +Packaging is versioned with git, using git-import-orig (with +--pristine-tar option) and git-buildpackage (with --git-pristine-tar +option). Debian changelog can be updated based on git changelog using +git-dch. Please consider reading the documentation of these tools. + +It was versioned with subversion until Wed, 23 Jul 2008. + + +Build cache +----------- + +Since Coq takes so much time to compile, there is a build cache to +speed-up Debian development and debugging. Just copy a previous build +to ../coq.cache, and debian/rules will detect its presence and rsync +from there instead of really compiling Coq... + + + -- Stéphane Glondu <glondu@debian.org>, Mon, 31 May 2010 15:30:50 +0200 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..593104db --- /dev/null +++ b/debian/changelog @@ -0,0 +1,619 @@ +coq (8.3+dfsg-2) UNRELEASED; urgency=low + + * NOT RELEASED YET + + -- Stéphane Glondu <glondu@debian.org> Tue, 19 Oct 2010 12:10:18 +0200 + +coq (8.3+dfsg-1) experimental; urgency=low + + * New upstream release + - add 0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch + * Bump Standards-Version to 3.9.1 (no changes) + + -- Stéphane Glondu <glondu@debian.org> Sat, 16 Oct 2010 09:56:23 +0200 + +coq (8.3~rc1+dfsg-1) experimental; urgency=low + + * New upstream release candidate + + -- Stéphane Glondu <glondu@debian.org> Tue, 10 Aug 2010 19:22:15 +0200 + +coq (8.3~beta0+13323-1) experimental; urgency=low + + * New upstream snapshot + * Update copyright file + * Fix installation of emacs files + + -- Stéphane Glondu <glondu@debian.org> Sat, 24 Jul 2010 20:17:44 +0200 + +coq (8.3~beta0+13298-1) experimental; urgency=low + + * New upstream snapshot + - remove all patches + * Install plugins in new binary package libcoq-ocaml + + -- Stéphane Glondu <glondu@debian.org> Wed, 21 Jul 2010 15:16:53 +0200 + +coq (8.2.pl2+dfsg-1) unstable; urgency=low + + * New upstream release + - compiles with OCaml 3.12 (Closes: #585452) + - remove 0001-Update-for-why-2.19.patch (applied upstream) + - add 0002-Remove-dependency-to-Unix-from-module-Profile.patch + * Use dh with overrides + * debian/control: + - remove Stefano and Remi from Uploaders + - replace Conflicts with Breaks + - bump Standards-Version to 3.9.0 + * Switch source package format to 3.0 (quilt) + + -- Stéphane Glondu <glondu@debian.org> Fri, 02 Jul 2010 15:25:15 +0200 + +coq (8.2.pl1+dfsg-6) unstable; urgency=low + + * Add Disable-micromega-tests.patch (workaround for bug #570920) + + -- Stéphane Glondu <glondu@debian.org> Mon, 22 Feb 2010 10:41:15 +0100 + +coq (8.2.pl1+dfsg-5) unstable; urgency=low + + * Rebuild with OCaml 3.11.2 + * Bump Standards-Version to 3.8.4 (no changes) + + -- Stéphane Glondu <glondu@debian.org> Wed, 10 Feb 2010 09:24:03 +0100 + +coq (8.2.pl1+dfsg-4) unstable; urgency=low + + [ Stefano Zacchiroli ] + * debian/control: fix typo in long description (Closes: #557458) + + [ Stéphane Glondu ] + * Switch to dh-ocaml 0.9 + + -- Stéphane Glondu <glondu@debian.org> Thu, 03 Dec 2009 11:54:58 +0100 + +coq (8.2.pl1+dfsg-3) unstable; urgency=low + + * Update README.Debian (Closes: #538398) + * Add 0001-Update-for-why-2.19.patch + * debian/control: + - update my e-mail address and remove DMUA + - add why to Suggests + - add quilt to Build-Depends + - update Standards-Version to 3.8.3 (no changes) + * Update README.source to reflect use of quilt + + -- Stéphane Glondu <glondu@debian.org> Sat, 29 Aug 2009 16:58:45 +0200 + +coq (8.2.pl1+dfsg-2) unstable; urgency=low + + * During validation of stdlib, call coqchk without -silent to avoid + timeout on buildds because of lack of output + + -- Stephane Glondu <steph@glondu.net> Sun, 05 Jul 2009 12:51:15 +0200 + +coq (8.2.pl1+dfsg-1) unstable; urgency=low + + * New Upstream Version + * debian/purify_tarball: keep some files from doc/common/styles/html + needed for HTML API doc generation + + -- Stephane Glondu <steph@glondu.net> Sat, 04 Jul 2009 12:13:28 +0200 + +coq (8.2-1+dfsg-2) unstable; urgency=low + + [ Samuel Mimram ] + * Remove upstream url from long descriptions since we already use the + Homepage field, closes: #524037. + * Updated watch file. + + [ Stephane Glondu ] + * Remove suggestion on package cle (which has been removed), use + readline-editor instead + * Recompile with OCaml 3.11.1 (Closes: #535320) + * Add versioned dependencies to camlp5 and liblablgtk2-ocaml-dev to + ease OCaml 3.11.1 transition + * Move libcoq-ocaml-dev to section ocaml + * Update Standards-Version to 3.8.2 + + -- Stephane Glondu <steph@glondu.net> Wed, 01 Jul 2009 17:41:55 +0200 + +coq (8.2-1+dfsg-1) unstable; urgency=low + + * New Upstream Version + * Use variables and ocamlinit rule from dh-ocaml in rules + * Added coqvars.mk helper for coq-related packages, and remove + /usr/lib/coq/abi (its contents is now it the COQ_ABI variable) + * Remove dependency on dpatch + * Add some missing Conflicts and Replaces in coq and libcoq-ocaml-dev + (Closes: #517107) + * Add missing dependency for coqide.byte (no longer compiled in + custom mode): liblablgtk2-ocaml + * Rebuild with OCaml 3.11 + + -- Stephane Glondu <steph@glondu.net> Fri, 27 Feb 2009 13:31:30 +0100 + +coq (8.2~rc2+dfsg-3) experimental; urgency=low + + * Explicit more dependencies and drop dependency on + ocaml-best-compilers, for autobuilders + + -- Stephane Glondu <steph@glondu.net> Sun, 08 Feb 2009 22:42:51 +0100 + +coq (8.2~rc2+dfsg-2) experimental; urgency=low + + * Add more versioned dependencies to please buildds + + -- Stephane Glondu <steph@glondu.net> Sun, 08 Feb 2009 10:52:43 +0100 + +coq (8.2~rc2+dfsg-1) experimental; urgency=low + + * New upstream release candidate + * Bump debhelper compatibility level to 7 + * Remove obsolete patches + * Use debhelper 7, simplify debian/rules (Closes: #436684) + * Add binary package libcoq-ocaml-dev + * Rename package coq-libs to coq-theories to avoid confusion, and + add a NEWS file to document it + * Add virtual coq-$ABI package, to express some ABI dependencies, + and put $ABI in /usr/lib/coq/abi. + + -- Stephane Glondu <steph@glondu.net> Mon, 02 Feb 2009 09:23:42 +0100 + +coq (8.2~beta4+dfsg-2) experimental; urgency=low + + * [45cca7f] Add non-native-archs.dpatch; fixes FTBFS on non-native + architectures (Closes: #495165) + + -- Stephane Glondu <steph@glondu.net> Fri, 15 Aug 2008 13:20:16 +0200 + +coq (8.2~beta4+dfsg-1) experimental; urgency=low + + [ Samuel Mimram ] + * New upstream release. + * Updated patches and removed coqdoc_stdlib, makefile, configure and + cmxa-install obsolete patches. + + [ Stephane Glondu ] + * Update debian/rules and debhelper files + * [8dd1802] Fix typo in README.Debian + * [dec29bb] Add myself to Uploaders, and DM-Upload-Allowed to control + * [dd1436b] Switch packaging to git + * [2dd9e5d] Set doc-base section to Science/Mathematics + * [c89cb94] Add Homepage field + * [7dd7c53] Add debian/README.source + * [1c6c7c8] Bump Standards-Version to 3.8.0 + * [38db629] Remove browser.dpatch and use --browser configure option + * [9fd4621] Add use-env-in-coq-config.dpatch + * [c7560b2] Remove obsolete manpages (now shipped upstream) + + -- Stephane Glondu <steph@glondu.net> Tue, 12 Aug 2008 16:37:51 +0200 + +coq (8.1.pl3+dfsg-1) unstable; urgency=low + + [ Stefano Zacchiroli ] + * fix vcs-svn field to point just above the debian/ dir + + [ Samuel Mimram ] + * New upstream release. + * Makefile should now be compatible with dash, closes: #459050. + * Updated watch file. + + -- Samuel Mimram <smimram@debian.org> Fri, 04 Jan 2008 13:21:43 +0000 + +coq (8.1.pl2+dfsg-3) unstable; urgency=low + + * Added check.dpatch to remove warnings which made some tests erroneously + fail, closes: #452572. + * Added a dependency from coq to emacsen-common, closes: #435023. + + -- Samuel Mimram <smimram@debian.org> Thu, 29 Nov 2007 13:59:01 +0000 + +coq (8.1.pl2+dfsg-2) unstable; urgency=low + + * Upload to unstable. + + -- Samuel Mimram <smimram@debian.org> Fri, 16 Nov 2007 19:20:24 +0000 + +coq (8.1.pl2+dfsg-1) experimental; urgency=low + + * New upstream release. + * Removed camlp5.dpatch, integrated upstream. + * Updated browser.dpatch, coqdoc_stdlib.dpatch and makefile.dpatch. + * Corrected emacs-mode startup file, closes: #446170. + * Removed Sven Luther from uploaders. + + -- Samuel Mimram <smimram@debian.org> Mon, 15 Oct 2007 18:55:09 +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/clean b/debian/clean new file mode 100644 index 00000000..7c32f559 --- /dev/null +++ b/debian/clean @@ -0,0 +1 @@ +install diff --git a/debian/compat b/debian/compat new file mode 100644 index 00000000..7f8f011e --- /dev/null +++ b/debian/compat @@ -0,0 +1 @@ +7 diff --git a/debian/control b/debian/control new file mode 100644 index 00000000..cc64c1b2 --- /dev/null +++ b/debian/control @@ -0,0 +1,117 @@ +Source: coq +Section: math +Priority: optional +Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org> +Uploaders: + Ralf Treinen <treinen@debian.org>, + Samuel Mimram <smimram@debian.org>, + Stéphane Glondu <glondu@debian.org> +Standards-Version: 3.9.1 +Build-Depends: + debhelper (>= 7.2.11~), + dh-ocaml (>= 0.9.5~), + ocaml-nox (>= 3.11.1-3~), + ocaml-best-compilers, + camlp5 (>= 5.12-2~), + liblablgtk2-ocaml-dev (>= 2.14), + texlive-latex-extra, + hevea (>= 1.10-7) +Homepage: http://coq.inria.fr/ +Vcs-Browser: http://git.debian.org/?p=pkg-ocaml-maint/packages/coq.git +Vcs-Git: git://git.debian.org/git/pkg-ocaml-maint/packages/coq.git + +Package: coq +Architecture: any +Depends: + coq-theories (= ${source:Version}), + emacsen-common, + ${ocaml:Depends}, + ${shlibs:Depends}, + ${misc:Depends} +Provides: coq-${F:CoqABI} +Recommends: coqide | proofgeneral-coq +Suggests: + ocaml-nox, + proofgeneral-coq, + ledit | readline-editor, + libcoq-ocaml-dev, + why (>= 2.19), + coq-doc +Breaks: coq-libs (<< 8.2.pl1) +Replaces: coq-libs (<< 8.2.pl1) +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 Camlp5. + . + This package 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: + coq (= ${binary:Version}), + ${ocaml:Depends}, + ${shlibs:Depends}, + ${misc:Depends} +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 Camlp5. + . + This package provides CoqIde, a graphical user interface for + developing proofs. + +Package: coq-theories +Architecture: all +Depends: coq-${F:CoqABI}, ${misc:Depends} +Recommends: coq (>= 8.0) +Breaks: coq-doc (<= 8.0pl1.0-2), coq-libs (<< 8.2.pl1) +Replaces: coq-libs (<< 8.2.pl1) +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 Camlp5. + . + This package provides existing theories that new proofs can be + based upon, including theories of arithmetic and Boolean values. + +Package: libcoq-ocaml +Section: ocaml +Architecture: any +Depends: + ${ocaml:Depends}, + ${shlibs:Depends}, + ${misc:Depends} +Provides: ${ocaml:Provides} +Breaks: coq (<< 8.3~), libcoq-ocaml-dev (<< 8.3~), coq-libs +Replaces: coq (<< 8.3~), libcoq-ocaml-dev (<< 8.3~), coq-libs +Description: runtime libraries for Coq + 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 Camlp5. + . + This package provides runtime libraries for Coq. + +Package: libcoq-ocaml-dev +Section: ocaml +Architecture: any +Depends: + coq (= ${binary:Version}), + ${ocaml:Depends}, + ${shlibs:Depends}, + ${misc:Depends} +Provides: ${ocaml:Provides} +Breaks: coq (<< 8.2-1+dfsg-1), coq-libs (<< 8.2.pl1) +Replaces: coq (<< 8.2-1+dfsg-1), coq-libs (<< 8.2.pl1) +Description: development libraries and tools for Coq + 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 Camlp5. + . + This package provides coqmktop, and libraries needed to develop + OCaml-side extensions to Coq. diff --git a/debian/copyright b/debian/copyright new file mode 100644 index 00000000..6ff2511f --- /dev/null +++ b/debian/copyright @@ -0,0 +1,29 @@ +Packaged-By: Fernando Sanchez <fer@debian.org> +Packaged-Date: Fri, 03 Dec 1999 22:06:04 +0100 +Original-Source-Location: http://coq.inria.fr/ + +Files: * +Copyright: © 1999-2010 The Coq development team, + INRIA, CNRS, University Paris Sud, + University Paris 7, Ecole Polytechnique. +License: LGPL-2.1 + + This product includes also software developed by + Pierre Crégut, France Telecom R & D (plugins/omega and plugins/romega) + Pierre Courtieu and Julien Forest, CNAM (plugins/funind) + Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml) + Pierre Corbineau, Radbout University, Nijmegen (declarative mode) + John Harrison, University of Cambridge (csdp wrapper) + + The file /usr/share/doc/coq/CREDITS.gz contains a list of contributors. + + 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. + +Files: debian/* +Copyright: © 1999-2000 Fernando Sanchez <fer@debian.org> + © 2001-2002 Judicael Courant <Judicael.Courant@lri.fr> + © 2004-2009 Samuel Mimram <smimram@debian.org> + © 2008-2010 Stéphane Glondu <glondu@debian.org> +License: LGPL-2.1 diff --git a/debian/coq-theories.dirs b/debian/coq-theories.dirs new file mode 100644 index 00000000..633cedc0 --- /dev/null +++ b/debian/coq-theories.dirs @@ -0,0 +1,2 @@ +usr/share/doc/coq-theories +usr/share/doc/coq diff --git a/debian/coq-theories.doc-base b/debian/coq-theories.doc-base new file mode 100644 index 00000000..ab3904e8 --- /dev/null +++ b/debian/coq-theories.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: Science/Mathematics + +Format: HTML +Index: /usr/share/doc/coq-theories/html/index.html +Files: /usr/share/doc/coq-theories/html/*.html diff --git a/debian/coq-theories.install.in b/debian/coq-theories.install.in new file mode 100644 index 00000000..956a04f3 --- /dev/null +++ b/debian/coq-theories.install.in @@ -0,0 +1,2 @@ +doc/stdlib/html usr/share/doc/coq-theories/ +# *.vo files will be added here diff --git a/debian/coq-theories.links b/debian/coq-theories.links new file mode 100644 index 00000000..f367523c --- /dev/null +++ b/debian/coq-theories.links @@ -0,0 +1,2 @@ +/usr/share/doc/coq-theories/html /usr/share/doc/coq/stdlib-html +/usr/lib/coq/tools/coqdoc/coqdoc.css /usr/share/doc/coq-theories/html/coqdoc.css 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.in b/debian/coq.install.in new file mode 100644 index 00000000..2c0f9c86 --- /dev/null +++ b/debian/coq.install.in @@ -0,0 +1,24 @@ +usr/bin/coqc* +usr/bin/coqdep* +usr/bin/coqdoc* +usr/bin/coq_makefile* +usr/bin/coq-tex* +usr/bin/coqtop* +usr/bin/coqwc* +usr/bin/gallina* +usr/lib/coq/plugins/micromega/csdpcert +usr/lib/coq/tools/coqdoc/coqdoc.css +usr/lib/coq/tools/coqdoc/coqdoc.sty +usr/lib/coq/states/initial.coq +usr/share/emacs/site-lisp/coq/ +usr/share/man/man1/coqc* +usr/share/man/man1/coqdep* +usr/share/man/man1/coqdoc* +usr/share/man/man1/coq_makefile* +usr/share/man/man1/coq-tex* +usr/share/man/man1/coqtop* +usr/share/man/man1/coqwc* +usr/share/man/man1/gallina* +usr/share/emacs/site-lisp/coqdoc.sty usr/share/texmf/tex/latex/misc/ +debian/coq.xpm usr/share/pixmaps +debian/coqvars.mk usr/share/coq diff --git a/debian/coq.links.in b/debian/coq.links.in new file mode 100644 index 00000000..33c64ad9 --- /dev/null +++ b/debian/coq.links.in @@ -0,0 +1 @@ +OPT: /usr/share/man/man1/coqchk.1 /usr/share/man/man1/coqchk.opt.1
\ No newline at end of file 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/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..ea667c56 --- /dev/null +++ b/debian/coqide.desktop @@ -0,0 +1,8 @@ +[Desktop Entry] +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..6fcc323e --- /dev/null +++ b/debian/coqide.docs @@ -0,0 +1 @@ +ide/FAQ diff --git a/debian/coqide.install b/debian/coqide.install new file mode 100644 index 00000000..fc5b80fe --- /dev/null +++ b/debian/coqide.install @@ -0,0 +1,6 @@ +usr/bin/coqide* +usr/lib/coq/ide/coq.png +usr/lib/coq/ide/.coqide-gtk2rc +usr/lib/coq/ide/FAQ +usr/share/man/man1/coqide* +debian/coqide.desktop usr/share/applications diff --git a/debian/coqide.links.in b/debian/coqide.links.in new file mode 100644 index 00000000..c73095fe --- /dev/null +++ b/debian/coqide.links.in @@ -0,0 +1,2 @@ +/usr/share/man/man1/coqide.1 /usr/share/man/man1/coqide.byte.1 +OPT: /usr/share/man/man1/coqide.1 /usr/share/man/man1/coqide.opt.1 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/coqvars.mk.in b/debian/coqvars.mk.in new file mode 100644 index 00000000..efbbd248 --- /dev/null +++ b/debian/coqvars.mk.in @@ -0,0 +1,12 @@ +# Current coq version +COQ_VERSION ?= @CoqVersion@ + +# Current coq ABI +COQ_ABI ?= @CoqABI@ + +# Standard library path +COQ_STDLIB_DIR ?= $(shell /usr/bin/coqc -where) + +# Directory for contributions +# External libraries should go there +COQ_USERCONTRIB_DIR ?= $(COQ_STDLIB_DIR)/user-contrib 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/gbp.conf b/debian/gbp.conf new file mode 100644 index 00000000..dfa07a01 --- /dev/null +++ b/debian/gbp.conf @@ -0,0 +1,4 @@ +[DEFAULT] +pristine-tar = True +upstream-branch = experimental/upstream +debian-branch = experimental/master diff --git a/debian/libcoq-ocaml-dev.install.in b/debian/libcoq-ocaml-dev.install.in new file mode 100644 index 00000000..cfaf7ca6 --- /dev/null +++ b/debian/libcoq-ocaml-dev.install.in @@ -0,0 +1,17 @@ +usr/bin/coqmktop* +usr/share/man/man1/coqmktop* +usr/lib/coq/proofs/proofs.cma +usr/lib/coq/ide/ide.cma +usr/lib/coq/interp/interp.cma +usr/lib/coq/tactics/tactics.cma +usr/lib/coq/tactics/hightactics.cma +usr/lib/coq/lib/lib.cma +usr/lib/coq/toplevel/toplevel.cma +usr/lib/coq/parsing/highparsing.cma +usr/lib/coq/parsing/grammar.cma +usr/lib/coq/parsing/parsing.cma +usr/lib/coq/pretyping/pretyping.cma +usr/lib/coq/library/library.cma +usr/lib/coq/kernel/kernel.cma +usr/lib/coq/config/coq_config.cmo +# other *.cm* files will be added here by debian/rules diff --git a/debian/libcoq-ocaml.install.in b/debian/libcoq-ocaml.install.in new file mode 100644 index 00000000..746a3577 --- /dev/null +++ b/debian/libcoq-ocaml.install.in @@ -0,0 +1,47 @@ +usr/lib/coq/dllcoqrun.so @OCamlDllDir@ +usr/lib/coq/plugins/ring/ring_plugin.cma +usr/lib/coq/plugins/fourier/fourier_plugin.cma +usr/lib/coq/plugins/extraction/extraction_plugin.cma +usr/lib/coq/plugins/omega/omega_plugin.cma +usr/lib/coq/plugins/cc/cc_plugin.cma +usr/lib/coq/plugins/syntax/string_syntax_plugin.cma +usr/lib/coq/plugins/syntax/nat_syntax_plugin.cma +usr/lib/coq/plugins/syntax/numbers_syntax_plugin.cma +usr/lib/coq/plugins/syntax/z_syntax_plugin.cma +usr/lib/coq/plugins/syntax/r_syntax_plugin.cma +usr/lib/coq/plugins/syntax/ascii_syntax_plugin.cma +usr/lib/coq/plugins/funind/recdef_plugin.cma +usr/lib/coq/plugins/nsatz/nsatz_plugin.cma +usr/lib/coq/plugins/xml/xml_plugin.cma +usr/lib/coq/plugins/dp/dp_plugin.cma +usr/lib/coq/plugins/romega/romega_plugin.cma +usr/lib/coq/plugins/firstorder/ground_plugin.cma +usr/lib/coq/plugins/subtac/subtac_plugin.cma +usr/lib/coq/plugins/field/field_plugin.cma +usr/lib/coq/plugins/rtauto/rtauto_plugin.cma +usr/lib/coq/plugins/setoid_ring/newring_plugin.cma +usr/lib/coq/plugins/micromega/micromega_plugin.cma +usr/lib/coq/plugins/quote/quote_plugin.cma +DYN: usr/lib/coq/plugins/ring/ring_plugin.cmxs +DYN: usr/lib/coq/plugins/fourier/fourier_plugin.cmxs +DYN: usr/lib/coq/plugins/extraction/extraction_plugin.cmxs +DYN: usr/lib/coq/plugins/omega/omega_plugin.cmxs +DYN: usr/lib/coq/plugins/cc/cc_plugin.cmxs +DYN: usr/lib/coq/plugins/syntax/string_syntax_plugin.cmxs +DYN: usr/lib/coq/plugins/syntax/nat_syntax_plugin.cmxs +DYN: usr/lib/coq/plugins/syntax/numbers_syntax_plugin.cmxs +DYN: usr/lib/coq/plugins/syntax/z_syntax_plugin.cmxs +DYN: usr/lib/coq/plugins/syntax/r_syntax_plugin.cmxs +DYN: usr/lib/coq/plugins/syntax/ascii_syntax_plugin.cmxs +DYN: usr/lib/coq/plugins/funind/recdef_plugin.cmxs +DYN: usr/lib/coq/plugins/nsatz/nsatz_plugin.cmxs +DYN: usr/lib/coq/plugins/xml/xml_plugin.cmxs +DYN: usr/lib/coq/plugins/dp/dp_plugin.cmxs +DYN: usr/lib/coq/plugins/romega/romega_plugin.cmxs +DYN: usr/lib/coq/plugins/firstorder/ground_plugin.cmxs +DYN: usr/lib/coq/plugins/subtac/subtac_plugin.cmxs +DYN: usr/lib/coq/plugins/field/field_plugin.cmxs +DYN: usr/lib/coq/plugins/rtauto/rtauto_plugin.cmxs +DYN: usr/lib/coq/plugins/setoid_ring/newring_plugin.cmxs +DYN: usr/lib/coq/plugins/micromega/micromega_plugin.cmxs +DYN: usr/lib/coq/plugins/quote/quote_plugin.cmxs diff --git a/debian/patches/0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch b/debian/patches/0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch new file mode 100644 index 00000000..c3092bac --- /dev/null +++ b/debian/patches/0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch @@ -0,0 +1,23 @@ +From: Stephane Glondu <steph@glondu.net> +Date: Fri, 15 Oct 2010 17:24:18 +0200 +Subject: [PATCH] Fix missing -coqlib argument to coqdep in test-suite + +Signed-off-by: Stephane Glondu <steph@glondu.net> +--- + test-suite/Makefile | 2 +- + 1 files changed, 1 insertions(+), 1 deletions(-) + +diff --git a/test-suite/Makefile b/test-suite/Makefile +index 62d443d..98bab43 100644 +--- a/test-suite/Makefile ++++ b/test-suite/Makefile +@@ -40,7 +40,7 @@ endif + + command := $(coqtop) -top Top -load-vernac-source + coqc := $(coqtop) -compile +-coqdep := $(BIN)coqdep ++coqdep := $(BIN)coqdep -coqlib $(LIB) + + SHOW := $(if $(VERBOSE),@true,@echo) + HIDE := $(if $(VERBOSE),,@) +-- diff --git a/debian/patches/0002-Fix-mixed-implicit-and-normal-rules.patch b/debian/patches/0002-Fix-mixed-implicit-and-normal-rules.patch new file mode 100644 index 00000000..79c1a22b --- /dev/null +++ b/debian/patches/0002-Fix-mixed-implicit-and-normal-rules.patch @@ -0,0 +1,85 @@ +From: Stephane Glondu <steph@glondu.net> +Date: Tue, 19 Oct 2010 12:00:55 +0200 +Subject: [PATCH] Fix mixed implicit and normal rules + +This fixes build with GNU Make 3.82. See threads: + + https://sympa-roc.inria.fr/wws/arc/coqdev/2010-10/msg00025.html + http://thread.gmane.org/gmane.comp.gnu.make.bugs/4912 + +Signed-off-by: Stephane Glondu <steph@glondu.net> +--- + Makefile | 10 ++++++++++ + Makefile.common | 15 +++++++++------ + 2 files changed, 19 insertions(+), 6 deletions(-) + +diff --git a/Makefile b/Makefile +index 975ece0..908dbd6 100644 +--- a/Makefile ++++ b/Makefile +@@ -160,9 +160,19 @@ else + stage1 $(STAGE1_TARGETS) : always + $(call stage-template,1) + ++ifneq (,$(STAGE1_IMPLICITS)) ++$(STAGE1_IMPLICITS) : always ++ $(call stage-template,1) ++endif ++ + stage2 $(STAGE2_TARGETS) : stage1 + $(call stage-template,2) + ++ifneq (,$(STAGE2_IMPLICITS)) ++$(STAGE2_IMPLICITS) : stage1 ++ $(call stage-template,2) ++endif ++ + # Nota: + # - world is one of the targets in $(STAGE2_TARGETS), hence launching + # "make" or "make world" leads to recursion into stage1 then stage2 +diff --git a/Makefile.common b/Makefile.common +index cc38980..46bf217 100644 +--- a/Makefile.common ++++ b/Makefile.common +@@ -365,7 +365,7 @@ DATE=$(shell LANG=C date +"%B %Y") + + SOURCEDOCDIR=dev/source-doc + +-CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot ++CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.o %.cmi %.cma %.cmxa %.a %.cmxs %.dep.ps %.dot + + ### Targets forwarded by Makefile to a specific stage: + +@@ -374,10 +374,12 @@ CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot + STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \ + $(GENFILES) \ + source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \ +- $(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o ++ $(STAGE1_ML4:.ml4=.ml4-preprocessed) ++ ++STAGE1_IMPLICITS:= + + ifdef CM_STAGE1 +- STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS) ++ STAGE1_IMPLICITS+=$(CAML_OBJECT_PATTERNS) + endif + + ## Enumeration of targets that require being done at stage2 +@@ -402,12 +404,13 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \ + printers debug initplugins plugins \ + world install coqide coqide-files coq coqlib \ + coqlight states check init theories theories-light \ +- $(DOC_TARGETS) $(VO_TARGETS) validate \ +- %.vo %.glob states/% install-% %.ml4-preprocessed \ ++ $(DOC_TARGETS) $(VO_TARGETS) validate ++ ++STAGE2_IMPLICITS:= %.vo %.glob states/% install-% %.ml4-preprocessed \ + $(DOC_TARGET_PATTERNS) + + ifndef CM_STAGE1 +- STAGE2_TARGETS+=$(CAML_OBJECT_PATTERNS) ++ STAGE2_IMPLICITS+=$(CAML_OBJECT_PATTERNS) + endif + + +-- diff --git a/debian/patches/0003-Support-for-camlp5-6.02.1.patch b/debian/patches/0003-Support-for-camlp5-6.02.1.patch new file mode 100644 index 00000000..4dfaa7b9 --- /dev/null +++ b/debian/patches/0003-Support-for-camlp5-6.02.1.patch @@ -0,0 +1,156 @@ +From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> +Date: Tue, 16 Nov 2010 20:25:56 +0000 +Subject: [PATCH] Support for camlp5 6.02.1 + +Signed-off-by: Stephane Glondu <steph@glondu.net> +--- + lib/compat.ml4 | 12 ++++++++++++ + parsing/pcoq.ml4 | 23 ++++++++++++++--------- + parsing/pcoq.mli | 2 ++ + toplevel/metasyntax.ml | 26 +++++++++++++------------- + 4 files changed, 41 insertions(+), 22 deletions(-) + +diff --git a/lib/compat.ml4 b/lib/compat.ml4 +index 9b6bb19..a77c2bc 100644 +--- a/lib/compat.ml4 ++++ b/lib/compat.ml4 +@@ -65,3 +65,15 @@ let unloc = M.unloc + let join_loc = M.join_loc + type token = M.token + type lexer = M.lexer ++ ++IFDEF CAMLP5_6_00 THEN ++ ++let slist0sep x y = Gramext.Slist0sep (x, y, false) ++let slist1sep x y = Gramext.Slist1sep (x, y, false) ++ ++ELSE ++ ++let slist0sep x y = Gramext.Slist0sep (x, y) ++let slist1sep x y = Gramext.Slist1sep (x, y) ++ ++END +diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 +index 90a9220..de1b3ed 100644 +--- a/parsing/pcoq.ml4 ++++ b/parsing/pcoq.ml4 +@@ -145,6 +145,11 @@ module Gram = + G.delete_rule e pil + end + ++IFDEF CAMLP5_6_02_1 THEN ++let entry_print x = Gram.Entry.print !Pp_control.std_ft x ++ELSE ++let entry_print = Gram.Entry.print ++END + + let camlp4_verbosity silent f x = + let a = !Gramext.warning_verbose in +@@ -631,16 +636,16 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ = + | ETConstrList (typ',[]) -> + Gramext.Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ')) + | ETConstrList (typ',tkl) -> +- Gramext.Slist1sep +- (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'), +- make_sep_rules tkl) ++ Compat.slist1sep ++ (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ')) ++ (make_sep_rules tkl) + | ETBinderList (false,[]) -> + Gramext.Slist1 + (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false)) + | ETBinderList (false,tkl) -> +- Gramext.Slist1sep +- (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false), +- make_sep_rules tkl) ++ Compat.slist1sep ++ (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false)) ++ (make_sep_rules tkl) + | _ -> + match interp_constr_prod_entry_key assoc from forpat typ with + | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj) +@@ -654,16 +659,16 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ = + let rec symbol_of_prod_entry_key = function + | Alist1 s -> Gramext.Slist1 (symbol_of_prod_entry_key s) + | Alist1sep (s,sep) -> +- Gramext.Slist1sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep)) ++ Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep)) + | Alist0 s -> Gramext.Slist0 (symbol_of_prod_entry_key s) + | Alist0sep (s,sep) -> +- Gramext.Slist0sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep)) ++ Compat.slist0sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep)) + | Aopt s -> Gramext.Sopt (symbol_of_prod_entry_key s) + | Amodifiers s -> + Gramext.srules + [([], Gramext.action(fun _loc -> [])); + ([Gramext.Stoken ("", "("); +- Gramext.Slist1sep ((symbol_of_prod_entry_key s), Gramext.Stoken ("", ",")); ++ Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", ",")); + Gramext.Stoken ("", ")")], + Gramext.action (fun _ l _ _loc -> l))] + | Aself -> Gramext.Sself +diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli +index e4566e7..7dbd78e 100644 +--- a/parsing/pcoq.mli ++++ b/parsing/pcoq.mli +@@ -23,6 +23,8 @@ open Libnames + + module Gram : Grammar.S with type te = Compat.token + ++val entry_print : 'a Gram.Entry.e -> unit ++ + (**********************************************************************) + (* The parser of Coq is built from three kinds of rule declarations: + - dynamic rules declared at the evaluation of Coq files (using +diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml +index 6ee00f4..ddb1b11 100644 +--- a/toplevel/metasyntax.ml ++++ b/toplevel/metasyntax.ml +@@ -106,33 +106,33 @@ let add_tactic_notation (n,prods,e) = + let print_grammar = function + | "constr" | "operconstr" | "binder_constr" -> + msgnl (str "Entry constr is"); +- Gram.Entry.print Pcoq.Constr.constr; ++ entry_print Pcoq.Constr.constr; + msgnl (str "and lconstr is"); +- Gram.Entry.print Pcoq.Constr.lconstr; ++ entry_print Pcoq.Constr.lconstr; + msgnl (str "where binder_constr is"); +- Gram.Entry.print Pcoq.Constr.binder_constr; ++ entry_print Pcoq.Constr.binder_constr; + msgnl (str "and operconstr is"); +- Gram.Entry.print Pcoq.Constr.operconstr; ++ entry_print Pcoq.Constr.operconstr; + | "pattern" -> +- Gram.Entry.print Pcoq.Constr.pattern ++ entry_print Pcoq.Constr.pattern + | "tactic" -> + msgnl (str "Entry tactic_expr is"); +- Gram.Entry.print Pcoq.Tactic.tactic_expr; ++ entry_print Pcoq.Tactic.tactic_expr; + msgnl (str "Entry binder_tactic is"); +- Gram.Entry.print Pcoq.Tactic.binder_tactic; ++ entry_print Pcoq.Tactic.binder_tactic; + msgnl (str "Entry simple_tactic is"); +- Gram.Entry.print Pcoq.Tactic.simple_tactic; ++ entry_print Pcoq.Tactic.simple_tactic; + | "vernac" -> + msgnl (str "Entry vernac is"); +- Gram.Entry.print Pcoq.Vernac_.vernac; ++ entry_print Pcoq.Vernac_.vernac; + msgnl (str "Entry command is"); +- Gram.Entry.print Pcoq.Vernac_.command; ++ entry_print Pcoq.Vernac_.command; + msgnl (str "Entry syntax is"); +- Gram.Entry.print Pcoq.Vernac_.syntax; ++ entry_print Pcoq.Vernac_.syntax; + msgnl (str "Entry gallina is"); +- Gram.Entry.print Pcoq.Vernac_.gallina; ++ entry_print Pcoq.Vernac_.gallina; + msgnl (str "Entry gallina_ext is"); +- Gram.Entry.print Pcoq.Vernac_.gallina_ext; ++ entry_print Pcoq.Vernac_.gallina_ext; + | _ -> error "Unknown or unprintable grammar entry." + + (**********************************************************************) +-- diff --git a/debian/patches/series b/debian/patches/series new file mode 100644 index 00000000..de7a4950 --- /dev/null +++ b/debian/patches/series @@ -0,0 +1,3 @@ +0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch +0002-Fix-mixed-implicit-and-normal-rules.patch +0003-Support-for-camlp5-6.02.1.patch diff --git a/debian/purify_tarball b/debian/purify_tarball new file mode 100755 index 00000000..f1d79961 --- /dev/null +++ b/debian/purify_tarball @@ -0,0 +1,30 @@ +#!/bin/bash + +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 + +mv coq-$VERSION/doc/common/styles/html/simple/{style.css,header.html,footer.html} coq-$VERSION +rm -rf coq-$VERSION/doc/common +mkdir -p coq-$VERSION/doc/common/styles/html/simple +mv coq-$VERSION/{style.css,header.html,footer.html} coq-$VERSION/doc/common/styles/html/simple +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 +find coq-$VERSION -name '*~' -delete + +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..3471198a --- /dev/null +++ b/debian/rules @@ -0,0 +1,88 @@ +#!/usr/bin/make -f +# debian/rules for coq + +# Uncomment this to turn on verbose mode. +#export DH_VERBOSE=1 + +# Build cache (for accelerating Debian debugging) +BUILDCACHE := $(wildcard ../coq.cache) + +# This has to be exported to make some magic below work. +export CAML_LD_LIBRARY_PATH = $(shell pwd)/kernel/byterun + +# Show full commands when building Coq +export VERBOSE=1 + +include /usr/share/ocaml/ocamlvars.mk + +HTMLDOC := doc/stdlib/html/index.html + +COQPREF := $(CURDIR)/debian/tmp +ADDPREF := COQINSTALLPREFIX=$(COQPREF) OLDROOT= + +PACKAGES := $(shell dh_listpackages) + +COQ_VERSION := $(shell dpkg-parsechangelog | sed -n -e 's/~/+/g' -e 's/^Version: \(.*\)-[0-9]\+/\1/p') +COQ_ABI := $(COQ_VERSION)+$(OCAML_ABI) + +CONFIGUREOPTS := --arch Linux --prefix /usr --mandir /usr/share/man \ + --emacslib /usr/share/emacs/site-lisp/coq \ + --browser "/usr/bin/x-www-browser %s &" \ + --with-doc no --coqrunbyteflags "-dllib -lcoqrun" + +export OCAMLINIT_SED += \ + -e 's%@CoqVersion@%$(COQ_VERSION)%' \ + -e 's%@CoqABI@%$(COQ_ABI)%' + +%: + +dh --with ocaml $@ + +# There is already a file named "build" in upstream sources, so the +# above rule is never called. We make it explicitly a phony rule here. +.PHONY: build +build: + +dh --with ocaml $@ + +.PHONY: override_dh_auto_configure +override_dh_auto_configure: + ./configure $(CONFIGUREOPTS) + +.PHONY: override_dh_auto_build +override_dh_auto_build: +ifeq ($(BUILDCACHE),) + +# VALIDOPTS are the options given to coqchk; the value given here is +# the default one without -silent (-silent maybe cause buildd to +# timeout because of lack of output) + + $(MAKE) world STRIP=true + $(MAKE) DOC_TARGETS=$(HTMLDOC) $(HTMLDOC) +else + rsync -a --exclude=debian --exclude=.git $(BUILDCACHE)/ . +endif + +.PHONY: override_dh_auto_test +override_dh_auto_test: + $(MAKE) check COMPLEXITY= BESTCHICKEN=/bin/true + +.PHONY: override_dh_auto_install +override_dh_auto_install: + $(MAKE) $(ADDPREF) install + find debian/tmp -regextype posix-awk \ + -regex '.*\.(cm[xi]|cmxa|[ao])$$' \ + >> debian/libcoq-ocaml-dev.install + find debian/tmp -name '*.vo' -printf '%P\n' \ + >> debian/coq-theories.install + +.PHONY: override_dh_install +override_dh_install: + dh_install --list-missing + cp debian/coq.xpm debian/coqide/usr/share/pixmaps/coqide.xpm + +.PHONY: override_dh_gencontrol +override_dh_gencontrol: + for u in $(PACKAGES); do \ + echo 'F:OCamlABI=$(OCAML_ABI)' >> debian/$$u.substvars; \ + echo 'F:CoqABI=$(COQ_ABI)' >> debian/$$u.substvars; \ + done + dh_gencontrol diff --git a/debian/source/format b/debian/source/format new file mode 100644 index 00000000..163aaf8d --- /dev/null +++ b/debian/source/format @@ -0,0 +1 @@ +3.0 (quilt) diff --git a/debian/source/local-options b/debian/source/local-options new file mode 100644 index 00000000..c4cf4805 --- /dev/null +++ b/debian/source/local-options @@ -0,0 +1,2 @@ +abort-on-upstream-changes +unapply-patches diff --git a/debian/watch b/debian/watch new file mode 100644 index 00000000..37d70519 --- /dev/null +++ b/debian/watch @@ -0,0 +1,4 @@ +version=3 + +opts=uversionmangle=s/pl/.pl/,dversionmangle=s/\+dfsg\d*$// \ + http://coq.inria.fr/download distrib/[^/]+/files/coq-(.*)\.tar\.gz |