diff options
38 files changed, 1644 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..55825cf9 --- /dev/null +++ b/debian/README.Debian @@ -0,0 +1,22 @@ +-------------------------- ++ 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 + package. + +However, we recommend you to use the CoqIde GTK+ interface provided in coqide. + + -- Stéphane Glondu <glondu@debian.org>, Sun, 19 Jan 2014 15:11:59 +0100 diff --git a/debian/README.source b/debian/README.source new file mode 100644 index 00000000..37984e0b --- /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 git-import-orig tool automatically filters out problematic files, +thanks to the configuration in debian/gbp.conf. It is suggested to +append the "dfsg" suffix to the upstream version to make repackaging +explicit. + + +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, 20 Aug 2012 18:20:18 +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..9a1b0ba3 --- /dev/null +++ b/debian/changelog @@ -0,0 +1,763 @@ +coq (8.5~beta1+dfsg-1) experimental; urgency=medium + + * New upstream release + * Add Enrico Tassi to uploaders + * Disable patch for lockf on Hurd (not needed anymore) + * coq-theories is now arch any, since it contains .coq-native/ directories + (i.e. cmxs files for native compute) + * coq depends on coq-theories binary:Version + * lintian-overrides for coq-native/*cmx* files (hardening-no-relro) + + -- Enrico Tassi <gareuselesinge@debian.org> Sun, 25 Jan 2015 13:48:50 +0100 + +coq (8.4pl4dfsg-1) unstable; urgency=medium + + * New upstream release (Closes: #755953) + * Switch debian/copyright to Format 1.0 + * Bump Standards-Version to 3.9.5 + * Bump debhelper compat level to 9 + + -- Stéphane Glondu <glondu@debian.org> Sun, 27 Jul 2014 15:25:03 +0200 + +coq (8.4pl3dfsg-1) unstable; urgency=medium + + * New upstream release + * Update README.Debian (Closes: #680248) + + -- Stéphane Glondu <glondu@debian.org> Sun, 19 Jan 2014 16:16:36 +0100 + +coq (8.4pl2dfsg-4) unstable; urgency=low + + * Upload to unstable + + -- Stéphane Glondu <glondu@debian.org> Tue, 03 Dec 2013 19:54:49 +0100 + +coq (8.4pl2dfsg-3) experimental; urgency=low + + * Compile with OCaml 4.01.0 + * Disable micromega tests on Hurd (because of missing lockf) + + -- Stéphane Glondu <glondu@debian.org> Fri, 22 Nov 2013 14:38:00 +0100 + +coq (8.4pl2dfsg-2) experimental; urgency=low + + * Compile with OCaml >= 4 + * Update Vcs-* + + -- Stéphane Glondu <glondu@debian.org> Fri, 26 Jul 2013 14:17:30 +0200 + +coq (8.4pl2dfsg-1) unstable; urgency=low + + * New upstream release + * Upload to unstable + + -- Stéphane Glondu <glondu@debian.org> Wed, 08 May 2013 18:10:14 +0200 + +coq (8.4pl1dfsg-1) experimental; urgency=low + + * New upstream release + - 0002-Fix-use-of-HASNATDYNLINK-in-coq_makefile-output.patch + has been merged upstream + - add ocaml-findlib to Build-Depends + + -- Stéphane Glondu <glondu@debian.org> Sat, 29 Dec 2012 15:56:53 +0100 + +coq (8.4dfsg-2) experimental; urgency=low + + * Upstream bugfix: Fix use of $(HASNATDYNLINK) in coq_makefile output + + -- Stéphane Glondu <glondu@debian.org> Sat, 22 Sep 2012 12:43:13 +0200 + +coq (8.4dfsg-1) experimental; urgency=low + + * New upstream release + + -- Stéphane Glondu <glondu@debian.org> Mon, 20 Aug 2012 18:33:45 +0200 + +coq (8.4~gamma0+really8.4beta2+dfsg-1) experimental; urgency=low + + * New upstream beta release + + -- Stéphane Glondu <glondu@debian.org> Tue, 05 Jun 2012 07:38:25 +0200 + +coq (8.4~beta+dfsg-4) experimental; urgency=low + + * Recompile with camlp5 6.05 (no changes) + + -- Stéphane Glondu <glondu@debian.org> Fri, 06 Apr 2012 10:04:06 +0200 + +coq (8.4~beta+dfsg-3) experimental; urgency=low + + * Replace proofgeneral-coq by proofgeneral in dependencies + * Disable a test that uses too much memory, causing random FTBFS + + -- Stéphane Glondu <glondu@debian.org> Sun, 15 Jan 2012 12:37:23 +0100 + +coq (8.4~beta+dfsg-2) experimental; urgency=low + + * Fix a typo that caused decl_mode_plugin.cmxs not being installed, + making coqtop.opt useless + * Fix an ordering issue that was causing a test to fail in bytecode + + -- Stéphane Glondu <glondu@debian.org> Sat, 14 Jan 2012 11:11:48 +0100 + +coq (8.4~beta+dfsg-1) experimental; urgency=low + + * New upstream beta release + + -- Stéphane Glondu <glondu@debian.org> Thu, 12 Jan 2012 18:53:08 +0100 + +coq (8.3.pl4+dfsg-2) unstable; urgency=low + + * Recompile with camlp5 6.06 (no changes) + + -- Stéphane Glondu <glondu@debian.org> Wed, 06 Jun 2012 07:35:26 +0200 + +coq (8.3.pl4+dfsg-1) unstable; urgency=low + + * New upstream release + * Replace proofgeneral-coq by proofgeneral in dependencies + * Switch debian/copyright to format 1.0 + * Bump Standards-Version to 3.9.3 + + -- Stéphane Glondu <glondu@debian.org> Tue, 27 Mar 2012 07:59:07 +0200 + +coq (8.3.pl3+dfsg-2) unstable; urgency=low + + * Recompile with camlp5 6.04 (no changes) + + -- Stéphane Glondu <glondu@debian.org> Sun, 04 Mar 2012 18:59:12 +0100 + +coq (8.3.pl3+dfsg-1) unstable; urgency=low + + * New upstream release + - remove all patches (applied upstream) + + -- Stéphane Glondu <glondu@debian.org> Sun, 25 Dec 2011 13:46:09 +0100 + +coq (8.3.pl2+dfsg-2) unstable; urgency=low + + * Recompile with OCaml 3.12.1 (no changes) + * Bump Standards-Version to 3.9.2 (no changes) + + -- Stéphane Glondu <glondu@debian.org> Wed, 02 Nov 2011 22:27:18 +0100 + +coq (8.3.pl2+dfsg-1) unstable; urgency=low + + * New upstream release + * Add patch to fix thumb2-related build error (Closes: #622882) + * Upload to unstable + + -- Stéphane Glondu <glondu@debian.org> Tue, 19 Apr 2011 17:37:30 +0200 + +coq (8.3.pl1+dfsg-2) experimental; urgency=low + + * Set and check COQ_VERSION used to compute COQ_ABI in debian/rules + + -- Stéphane Glondu <glondu@debian.org> Sat, 26 Feb 2011 18:12:12 +0100 + +coq (8.3.pl1+dfsg-1) experimental; urgency=low + + * New upstream release + - remove all patches (applied upstream) + * debian/rules: + - run test-suite in override_dh_auto_test, skip coqchk run + - make "build" explicitly a phony target + * Update copyright file + * Fix installation of emacs files + * Install plugins in new binary package libcoq-ocaml + * Bump Standards-Version to 3.9.1 (no changes) + + -- Stéphane Glondu <glondu@debian.org> Fri, 24 Dec 2010 12:51:59 +0100 + +coq (8.2.pl2+dfsg-2) unstable; urgency=low + + * Add Fix-build-with-camlp5-6.02.1.patch + * Bump versioned build-dependency on liblablgtk2-ocaml-dev to ease + lablgtk2 transition + + -- Stéphane Glondu <glondu@debian.org> Mon, 21 Feb 2011 16:51:11 +0100 + +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/compat b/debian/compat new file mode 100644 index 00000000..ec635144 --- /dev/null +++ b/debian/compat @@ -0,0 +1 @@ +9 diff --git a/debian/control b/debian/control new file mode 100644 index 00000000..9b0db8b7 --- /dev/null +++ b/debian/control @@ -0,0 +1,120 @@ +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>, + Enrico Tassi <gareuselesinge@debian.org> +Standards-Version: 3.9.5 +Build-Depends: + debhelper (>= 9), + dh-ocaml (>= 0.9.5~), + ocaml-nox (>= 4), + ocaml-best-compilers, + ocaml-findlib (>= 1.4), + camlp5 (>= 5.12-2~), + liblablgtk2-ocaml-dev (>= 2.14), + texlive-latex-extra, + hevea (>= 1.10-7) +Homepage: http://coq.inria.fr/ +Vcs-Browser: http://anonscm.debian.org/gitweb/?p=pkg-ocaml-maint/packages/coq.git +Vcs-Git: git://anonscm.debian.org/pkg-ocaml-maint/packages/coq.git + +Package: coq +Architecture: any +Depends: + coq-theories (= ${binary:Version}), + emacsen-common, + ${ocaml:Depends}, + ${shlibs:Depends}, + ${misc:Depends}, + ocaml-best-compilers +Provides: coq-${F:CoqABI} +Recommends: coqide | proofgeneral +Suggests: + ocaml-nox, + proofgeneral, + 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 + 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: any +Depends: coq-${F:CoqABI}, ${misc:Depends}, ${shlibs: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..43189711 --- /dev/null +++ b/debian/copyright @@ -0,0 +1,20 @@ +Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/ +Packaged-By: Fernando Sanchez <fer@debian.org> +Packaged-Date: Fri, 03 Dec 1999 22:06:04 +0100 +Source: http://coq.inria.fr/ + +Files: * +Copyright: 1999-2015 The Coq development team, INRIA, CNRS, University Paris Sud, University Paris 7, Ecole Polytechnique +License: 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-2014 Stéphane Glondu <glondu@debian.org> +License: LGPL-2.1 + +License: LGPL-2.1 + 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'. 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..f21378b0 --- /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 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-theories.lintian-overrides b/debian/coq-theories.lintian-overrides new file mode 100644 index 00000000..6ae619ae --- /dev/null +++ b/debian/coq-theories.lintian-overrides @@ -0,0 +1 @@ +hardening-no-relro *coq-native* 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..de06ab23 --- /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/bin/coqworkmgr* +usr/lib/coq/plugins/micromega/csdpcert +usr/lib/coq/tools/coqdoc/coqdoc.css +usr/lib/coq/tools/coqdoc/coqdoc.sty +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..c1da623a --- /dev/null +++ b/debian/coqide.dirs @@ -0,0 +1 @@ +usr/share/pixmaps diff --git a/debian/coqide.install b/debian/coqide.install new file mode 100644 index 00000000..c0189e2d --- /dev/null +++ b/debian/coqide.install @@ -0,0 +1,8 @@ +usr/bin/coqide* +usr/share/coq/coq.png +usr/share/coq/*.lang +usr/share/coq/*_style.xml +usr/share/doc/coq/FAQ-CoqIde usr/share/doc/coqide +usr/share/man/man1/coqide* +usr/lib/coq/toploop/coqidetop.* +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..126a7b7a --- /dev/null +++ b/debian/gbp.conf @@ -0,0 +1,18 @@ +[DEFAULT] +pristine-tar = True +filter-pristine-tar = True +filter = [ + "doc/common/styles/html/coqremote/cover.html", + "doc/common/styles/html/coqremote/hevea.css", + "doc/common/styles/html/coqremote/styles.hva", + "doc/common/styles/html/simple/cover.html", + "doc/common/styles/html/simple/hevea.css", + "doc/common/styles/html/simple/styles.hva", + "doc/common/macros.tex", + "doc/common/title.tex", + "doc/RecTutorial", + "doc/faq", + "doc/refman", + "doc/rt", + "doc/tools", + "doc/tutorial" ] diff --git a/debian/libcoq-ocaml-dev.install.in b/debian/libcoq-ocaml-dev.install.in new file mode 100644 index 00000000..49efecbc --- /dev/null +++ b/debian/libcoq-ocaml-dev.install.in @@ -0,0 +1,21 @@ +usr/bin/coqmktop* +usr/share/man/man1/coqmktop* +usr/lib/coq/grammar/grammar.cma +usr/lib/coq/ide/ide.cma +usr/lib/coq/interp/interp.cma +usr/lib/coq/kernel/kernel.cma +usr/lib/coq/lib/clib.cma +usr/lib/coq/lib/lib.cma +usr/lib/coq/library/library.cma +usr/lib/coq/parsing/highparsing.cma +usr/lib/coq/parsing/parsing.cma +usr/lib/coq/pretyping/pretyping.cma +usr/lib/coq/printing/printing.cma +usr/lib/coq/proofs/proofs.cma +usr/lib/coq/stm/stm.cma +usr/lib/coq/tactics/hightactics.cma +usr/lib/coq/tactics/tactics.cma +usr/lib/coq/toplevel/toplevel.cma +usr/lib/coq/tools/compat5.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..2b7783db --- /dev/null +++ b/debian/libcoq-ocaml.install.in @@ -0,0 +1,49 @@ +usr/lib/coq/dllcoqrun.so @OCamlDllDir@ +usr/lib/coq/plugins/quote/quote_plugin.cma +usr/lib/coq/plugins/rtauto/rtauto_plugin.cma +usr/lib/coq/plugins/extraction/extraction_plugin.cma +usr/lib/coq/plugins/cc/cc_plugin.cma +usr/lib/coq/plugins/decl_mode/decl_mode_plugin.cma +usr/lib/coq/plugins/btauto/btauto_plugin.cma +usr/lib/coq/plugins/fourier/fourier_plugin.cma +usr/lib/coq/plugins/funind/recdef_plugin.cma +usr/lib/coq/plugins/derive/derive_plugin.cma +usr/lib/coq/plugins/setoid_ring/newring_plugin.cma +usr/lib/coq/plugins/nsatz/nsatz_plugin.cma +usr/lib/coq/plugins/micromega/micromega_plugin.cma +usr/lib/coq/plugins/romega/romega_plugin.cma +usr/lib/coq/plugins/omega/omega_plugin.cma +usr/lib/coq/plugins/firstorder/ground_plugin.cma +usr/lib/coq/plugins/syntax/numbers_syntax_plugin.cma +usr/lib/coq/plugins/syntax/r_syntax_plugin.cma +usr/lib/coq/plugins/syntax/nat_syntax_plugin.cma +usr/lib/coq/plugins/syntax/ascii_syntax_plugin.cma +usr/lib/coq/plugins/syntax/string_syntax_plugin.cma +usr/lib/coq/plugins/syntax/z_syntax_plugin.cma +usr/lib/coq/toploop/proofworkertop.cma +usr/lib/coq/toploop/tacworkertop.cma +usr/lib/coq/toploop/queryworkertop.cma +DYN: usr/lib/coq/toploop/proofworkertop.cmxs +DYN: usr/lib/coq/toploop/tacworkertop.cmxs +DYN: usr/lib/coq/toploop/queryworkertop.cmxs +DYN: usr/lib/coq/plugins/quote/quote_plugin.cmxs +DYN: usr/lib/coq/plugins/rtauto/rtauto_plugin.cmxs +DYN: usr/lib/coq/plugins/extraction/extraction_plugin.cmxs +DYN: usr/lib/coq/plugins/cc/cc_plugin.cmxs +DYN: usr/lib/coq/plugins/decl_mode/decl_mode_plugin.cmxs +DYN: usr/lib/coq/plugins/btauto/btauto_plugin.cmxs +DYN: usr/lib/coq/plugins/fourier/fourier_plugin.cmxs +DYN: usr/lib/coq/plugins/funind/recdef_plugin.cmxs +DYN: usr/lib/coq/plugins/derive/derive_plugin.cmxs +DYN: usr/lib/coq/plugins/setoid_ring/newring_plugin.cmxs +DYN: usr/lib/coq/plugins/nsatz/nsatz_plugin.cmxs +DYN: usr/lib/coq/plugins/micromega/micromega_plugin.cmxs +DYN: usr/lib/coq/plugins/romega/romega_plugin.cmxs +DYN: usr/lib/coq/plugins/omega/omega_plugin.cmxs +DYN: usr/lib/coq/plugins/firstorder/ground_plugin.cmxs +DYN: usr/lib/coq/plugins/syntax/nat_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/numbers_syntax_plugin.cmxs +DYN: usr/lib/coq/plugins/syntax/ascii_syntax_plugin.cmxs +DYN: usr/lib/coq/plugins/syntax/string_syntax_plugin.cmxs diff --git a/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch b/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch new file mode 100644 index 00000000..198188e7 --- /dev/null +++ b/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch @@ -0,0 +1,30 @@ +From: Stephane Glondu <steph@glondu.net> +Date: Sun, 15 Jan 2012 12:34:19 +0100 +Subject: test-suite/success/Nsatz.v: comment out Ceva + +This lemma uses too much memory for many buildds... +--- + test-suite/success/Nsatz.v | 2 ++ + 1 file changed, 2 insertions(+) + +diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v +index d316e4a..d783b2a 100644 +--- a/test-suite/success/Nsatz.v ++++ b/test-suite/success/Nsatz.v +@@ -461,6 +461,7 @@ idtac "chords". + (*Finished transaction in 4. secs (3.959398u,0.s)*) + Qed. + ++(* + Lemma Ceva: forall A B C D E F M:point, + collinear M A D -> collinear M B E -> collinear M C F -> + collinear B C D -> collinear E A C -> collinear F A B -> +@@ -472,6 +473,7 @@ idtac "Ceva". + Time nsatz. + (*Finished transaction in 105. secs (104.121171u,0.474928s)*) + Qed. ++*) + + Lemma bissectrices: forall A B C M:point, + equaltangente C A M M A B -> +-- diff --git a/debian/patches/series b/debian/patches/series new file mode 100644 index 00000000..53d51a16 --- /dev/null +++ b/debian/patches/series @@ -0,0 +1 @@ +0001-test-suite-success-Nsatz.v-comment-out-Ceva.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..367b34e0 --- /dev/null +++ b/debian/rules @@ -0,0 +1,113 @@ +#!/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 := 8.5beta1 +COQ_ABI := $(COQ_VERSION)+$(OCAML_ABI) + +CONFIGUREOPTS := -arch Linux -prefix /usr -mandir /usr/share/man \ + -configdir /etc/xdg/coq \ + -emacslib /usr/share/emacs/site-lisp/coq \ + -browser "/usr/bin/x-www-browser %s &" \ + -with-doc no \ + -debug + +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) + # uncomment to create the cache + #mkdir ../coq.cache + #rsync -a --exclude=debian --exclude=.git . ../coq.cache/ +else + rsync -a --exclude=debian --exclude=.git $(BUILDCACHE)/ . +endif +# Check that $(COQ_VERSION) has the right value + ACTUAL_COQ_VERSION="$$(./bin/coqc --version | awk '/version/{print $$6}')"; \ + if [ "$$ACTUAL_COQ_VERSION" != "$(COQ_VERSION)" ]; then \ + echo "Please set COQ_VERSION to $$ACTUAL_COQ_VERSION in debian/rules"; \ + exit 2; \ + fi + +.PHONY: override_dh_auto_test +override_dh_auto_test: + # disabled since beta1 does not pass all tests + #$(MAKE) test-suite COMPLEXITY= + +.PHONY: override_dh_auto_install +override_dh_auto_install: + $(MAKE) $(ADDPREF) install + find debian/tmp -regextype posix-awk \ + -regex '.*\.(cmi|cmx|cmxa|[ao])$$' \ + | grep -v toploop/ | grep -v coq-native \ + >> debian/libcoq-ocaml-dev.install + find debian/tmp -name '*.vo' -printf '%P\n' \ + >> debian/coq-theories.install + find debian/tmp -name '*.v' -printf '%P\n' \ + >> debian/coq-theories.install + find debian/tmp -name '*.glob' -printf '%P\n' \ + >> debian/coq-theories.install + find debian/tmp -name '.coq-native' -printf '%P\n' \ + >> debian/coq-theories.install + +.PHONY: override_dh_install +override_dh_install: + chmod a-x debian/tmp/usr/lib/coq/toploop/*cma + dh_install --fail-missing + cp debian/coq.xpm debian/coqide/usr/share/pixmaps/coqide.xpm + +.PHONY: override_dh_ocaml +override_dh_ocaml: + dh_ocaml --nodefined-map coqide:Xmlprotocol,Ide_slave + for f in debian/*substvars; do echo $$f; cat $$f; done + +.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..5d9c70de --- /dev/null +++ b/debian/watch @@ -0,0 +1,4 @@ +version=3 +opts=dversionmangle=s/\+?(debian|dfsg|ds|deb)\d*$// \ +http://coq.inria.fr/download .*/coq-(\d.*)\.(?:tgz|tbz2|txz|tar\.(?:gz|bz2|xz)) +# Bart Martens <bartm@debian.org> Sun, 30 Dec 2012 20:22:30 +0000 |