diff options
39 files changed, 4483 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..2cadf798 --- /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 + package. + + -- Benjamin Barenblat <bbaren@debian.org>, Mon, 24 Dec 2018 15:11:23 -0500 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..ff8582b8 --- /dev/null +++ b/debian/changelog @@ -0,0 +1,848 @@ +coq (8.8.2-2) UNRELEASED; urgency=medium + + * Use freely licensed files from upstream to restore ssrmatching and reverse + dependencies. + + -- Benjamin Barenblat <bbaren@debian.org> Thu, 17 Jan 2019 17:10:25 -0500 + +coq (8.8.2-1) unstable; urgency=medium + + * New upstream release (Closes: #910840) + * Add Benjamin Barenblat to uploaders + * Update debian/watch for upstream's transition to GitHub (Closes: #902903) + * Stop distributing CoqIDE (Closes: #916369) + * coqmktop(1) has been deleted; users should migrate to ocamlfind(1) + + -- Benjamin Barenblat <bbaren@debian.org> Sun, 06 Jan 2019 23:07:04 -0500 + +coq (8.6-5) unstable; urgency=medium + + * Recompile with OCaml 4.05.0 + * Remove unused Lintian overrides + * Remove menu files + * Update Vcs-* + + -- Stéphane Glondu <glondu@debian.org> Tue, 26 Sep 2017 11:08:52 +0200 + +coq (8.6-4) unstable; urgency=medium + + * coq_makefile needs ocamlfind in order to work + + -- Enrico Tassi <gareuselesinge@debian.org> Thu, 29 Dec 2016 23:45:47 +0100 + +coq (8.6-3) unstable; urgency=medium + + * 5127.v fails on mips, disabling + + -- Enrico Tassi <gareuselesinge@debian.org> Thu, 29 Dec 2016 08:58:35 +0100 + +coq (8.6-2) unstable; urgency=medium + + * Disable some tests with hardcoded timeout to fix FTBFS on + slow machines + + -- Enrico Tassi <gareuselesinge@debian.org> Wed, 28 Dec 2016 18:19:29 +0100 + +coq (8.6-1) unstable; urgency=medium + + * New upstream release + + -- Enrico Tassi <gareuselesinge@debian.org> Tue, 27 Dec 2016 16:53:39 +0100 + +coq (8.5-2) unstable; urgency=medium + + * patch: disable test 4429 (timeout too strict for slow architectures) + + -- Enrico Tassi <gareuselesinge@debian.org> Thu, 28 Jan 2016 11:47:07 +0100 + +coq (8.5-1) unstable; urgency=medium + + * New upstream release + * patch: disable test 4366 (timeout too strict for slow architectures) + + -- Enrico Tassi <gareuselesinge@debian.org> Tue, 26 Jan 2016 16:59:05 +0100 + +coq (8.5~beta3+dfsg-2) experimental; urgency=medium + + * Option -no-native-compiler now called -native-compiler no + + -- Enrico Tassi <gareuselesinge@debian.org> Sat, 14 Nov 2015 14:59:04 +0100 + +coq (8.5~beta3+dfsg-1) experimental; urgency=medium + + * New upstream release + + -- Enrico Tassi <gareuselesinge@debian.org> Fri, 13 Nov 2015 11:27:35 +0100 + +coq (8.5~beta2+dfsg-2) experimental; urgency=medium + + * Enable native compiler only on amd64 and i386 + * Enable 'make test-suite' target + + -- Enrico Tassi <gareuselesinge@debian.org> Mon, 20 Jul 2015 09:51:21 +0200 + +coq (8.5~beta2+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* and plugins/*cmxs files + (hardening-no-relro) + * Build depend on liblablgtksourceview2-ocaml-dev + + -- Enrico Tassi <gareuselesinge@debian.org> Wed, 15 Jul 2015 11:36:30 +0200 + +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..f599e28b --- /dev/null +++ b/debian/compat @@ -0,0 +1 @@ +10 diff --git a/debian/control b/debian/control new file mode 100644 index 00000000..29f85268 --- /dev/null +++ b/debian/control @@ -0,0 +1,110 @@ +Source: coq +Section: math +Priority: optional +Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org> +Uploaders: + Benjamin Barenblat <bbaren@debian.org>, + Ralf Treinen <treinen@debian.org>, + Samuel Mimram <smimram@debian.org>, + Stéphane Glondu <glondu@debian.org>, + Enrico Tassi <gareuselesinge@debian.org> +Standards-Version: 4.3.0 +Build-Depends: + debhelper (>= 10), + dh-exec, + dh-ocaml (>= 0.9.5~), + dh-python, + ocaml-nox (>= 4), + ocaml-best-compilers, + ocaml-findlib (>= 1.4), + camlp5 (>= 5.12-2~), + liblablgtk2-ocaml-dev (>= 2.14), + liblablgtksourceview2-ocaml-dev, + python3, + rsync, + texlive-latex-extra, + hevea (>= 1.10-7) +Homepage: http://coq.inria.fr/ +Vcs-Browser: https://salsa.debian.org/ocaml-team/coq +Vcs-Git: https://salsa.debian.org/ocaml-team/coq.git + +Package: coq +Architecture: any +Depends: + coq-theories (= ${binary:Version}), + emacsen-common, + ${ocaml:Depends}, + ${python3:Depends}, + ${shlibs:Depends}, + ${misc:Depends}, + ocaml-best-compilers, + ocaml-findlib +Provides: coq-${F:CoqABI} +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. + . + The proofgeneral package allows proofs to be edited using Emacs and + XEmacs. + +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 and libraries needed to develop OCaml-side + extensions to Coq. diff --git a/debian/copyright b/debian/copyright new file mode 100644 index 00000000..171d8dd0 --- /dev/null +++ b/debian/copyright @@ -0,0 +1,134 @@ +Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/ +Upstream-Name: Coq +Source: https://github.com/coq/coq, modified to remove non-free parts +License: LGPL-2.1 + +Files: * +Copyright: 1999-2018 The Coq Development Team, INRIA, CNRS and contributors +License: LGPL-2.1 + +Files: config/* dev/* ide/* interp/* intf/* kernel/* lib/* library/* parsing/* + pretyping/* proofs/* tactics/* test-suite/* theories/* tools/* toplevel/* +Copyright: 1999-2017 The Coq development team, INRIA, CNRS, LIX, LRI, PPS +License: LGPL-2.1 + +Files: clib/predicate.ml +Copyright: 1996 Institut National de Recherche en Informatique et en Automatique +License: LGPL-2+ + +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> + 2018 Benjamin Barenblat <bbaren@debian.org> +License: LGPL-2.1 + +Files: dev/build/windows/* +Copyright: 2016 Intel Deutschland GmbH +License: LGPL-2.1+ + +Files: dev/tools/coqdev.el +Copyright: 2018 The Coq Development Team +License: LGPL-2.1 + +Files: ide/utils/* +Copyright: 2005 Institut National de Recherche en Informatique et en Automatique +License: LGPL-2+ + +Files: ide/xml_lexer.mli ide/xml_lexer.mll ide/xml_parser.mli +Copyright: 2003 Nicolas Cannasse <ncannasse@motion-twin.com> +License: LGPL-2.1+ + +Files: ide/xml_lexer.mli ide/xml_lexer.mll ide/xml_parser.ml +Copyright: 2003 Nicolas Cannasse <ncannasse@motion-twin.com> + 2003 Jacques Garrigue +License: LGPL-2.1+ + +Files: plugins/micromega/sos.ml plugins/micromega/sos_lib.ml +Copyright: 1998 University of Cambridge + 1998-2006 John Harrison +License: HOLLight + +Files: test-suite/bugs/closed/1918.v +Copyright: Ralph Matthes, I.R.I.T., C.N.R.S. & University of Toulouse +License: LGPL-2.1 + +Files: test-suite/interactive/ParalITP_smallproofs.v + test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v +Copyright: 1999-2017 The Coq development team, INRIA, CNRS, LIX, LRI, PPS +License: LGPL-2.1+ + +License: HOLLight + HOL Light version 2.20, hereinafter referred to as "the software", is a + computer theorem proving system written by John Harrison. Much of the software + was developed at the University of Cambridge Computer Laboratory, New Museums + Site, Pembroke Street, Cambridge, CB2 3QG, England. The software is copyright, + University of Cambridge 1998 and John Harrison 1998-2006. + . + Permission to use, copy, modify, and distribute the software and its + documentation for any purpose and without fee is hereby granted. In the case of + further distribution of the software the present text, including copyright + notice, licence and disclaimer of warranty, must be included in full and + unmodified form in any release. Distribution of derivative software obtained by + modifying the software, or incorporating it into other software, is permitted, + provided the inclusion of the software is acknowledged and that any changes + made to the software are clearly documented. + . + John Harrison and the University of Cambridge disclaim all warranties with + regard to the software, including all implied warranties of merchantability and + fitness. In no event shall John Harrison or the University of Cambridge be + liable for any special, indirect, incidental or consequential damages or any + damages whatsoever, including, but not limited to, those arising from computer + failure or malfunction, work stoppage, loss of profit or loss of contracts. + +License: LGPL-2+ + This library is free software; you can redistribute it and/or modify it under + the terms of the GNU Library General Public License as published by the Free + Software Foundation; either version 2 of the License, or (at your option) any + later version. + . + This library is distributed in the hope that it will be useful, but WITHOUT ANY + WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A + PARTICULAR PURPOSE. See the GNU Library General Public License for more + details. + . + You should have received a copy of the GNU Library General Public License along + with this library; if not, write to the Free Software Foundation, Inc., 51 + Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA + . + On Debian systems, the complete text of the GNU Library General Public License + version 2 can be found in "/usr/share/common-licenses/LGPL-2". + +License: LGPL-2.1 + This library is free software; you can redistribute it and/or modify it under + the terms of the GNU Lesser General Public License, version 2.1, as published + by the Free Software Foundation. + . + This library is distributed in the hope that it will be useful, but WITHOUT ANY + WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A + PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. + . + You should have received a copy of the GNU Lesser General Public License along + with this library; if not, write to the Free Software Foundation, Inc., 51 + Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA + . + On Debian systems, the complete text of the GNU Lesser General Public License + version 2.1 can be found in "/usr/share/common-licenses/LGPL-2.1". + +License: LGPL-2.1+ + This library is free software; you can redistribute it and/or modify it under + the terms of the GNU Lesser General Public License as published by the Free + Software Foundation; either version 2.1 of the License, or (at your option) any + later version. + . + This library is distributed in the hope that it will be useful, but WITHOUT ANY + WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A + PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. + . + You should have received a copy of the GNU Lesser General Public License along + with this library; if not, write to the Free Software Foundation, Inc., 51 + Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA + . + On Debian systems, the complete text of the GNU Lesser General Public License + version 2.1 can be found in "/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.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..f2f5339f --- /dev/null +++ b/debian/coq.install.in @@ -0,0 +1,30 @@ +#!/usr/bin/dh-exec +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/CoqMakefile.in +usr/lib/coq/tools/TimeFileMaker.py +usr/lib/coq/tools/coqdoc/coqdoc.css +usr/lib/coq/tools/coqdoc/coqdoc.sty +usr/lib/coq/tools/make-both-single-timing-files.py => usr/lib/coq/tools/make-both-single-timing-files +usr/lib/coq/tools/make-both-time-files.py => usr/lib/coq/tools/make-both-time-files +usr/lib/coq/tools/make-one-time-file.py => usr/lib/coq/tools/make-one-time-file +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/texmf/tex/latex/misc/coqdoc.sty +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.lintian-overrides b/debian/coq.lintian-overrides new file mode 100644 index 00000000..1c84a5d0 --- /dev/null +++ b/debian/coq.lintian-overrides @@ -0,0 +1,2 @@ +# False positive spelling error. +coq binary: spelling-error-in-binary usr/bin/coqwc tage stage 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/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..cee3c113 --- /dev/null +++ b/debian/docs @@ -0,0 +1,3 @@ +CHANGES +README.md +CREDITS diff --git a/debian/gbp.conf b/debian/gbp.conf new file mode 100644 index 00000000..e7255ba1 --- /dev/null +++ b/debian/gbp.conf @@ -0,0 +1,47 @@ +[DEFAULT] +pristine-tar = True +filter-pristine-tar = True +filter = [ + # Source from the Nullsoft Scriptable Install System wiki, which is not + # licensed. + "dev/build/windows/patches_coq/ReplaceInFile.nsh", + "dev/build/windows/patches_coq/StrRep.nsh", + "dev/nsis/FileAssociation.nsh", + + # Material connected to the reference manual, licensed under the non-free + # Open Publication License. + "doc/common/styles/html/coqremote/cover.html", + "doc/common/styles/html/coqremote/hevea.css", + "doc/common/styles/html/coqremote/modules", + "doc/common/styles/html/coqremote/sites", + "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/sphinx", + "doc/tools/coqrst/regen_readme.py", + "doc/tools/latex_filter", + "doc/tools/show_latex_messages", + "doc/tools/Translator.tex", + "interp/doc.tex", + "kernel/doc.tex", + "lib/doc.tex", + "library/doc.tex", + "pretyping/doc.tex", + "proofs/doc.tex", + "tactics/doc.tex", + "vernac/doc.tex", + + # Fonts licensed under the non-free Ubuntu Font Licence. + "doc/tools/coqrst/notations/CoqNotations.ttf", + "doc/tools/coqrst/notations/UbuntuMono-B.ttf", + + # Code with CeCILL-B license headers. bbaren believes CeCILL-B to be + # nonfree; see + # https://lists.debian.org/msgid-search/875zvih02a.jfx@benwick.benjamin.barenblat.name. + "plugins/ssrmatching/g_ssrmatching.mli", + + # This tries to build upstream's CI on Salsa, which doesn't work. + ".travis.yml" ] diff --git a/debian/libcoq-ocaml-dev.install.in b/debian/libcoq-ocaml-dev.install.in new file mode 100644 index 00000000..77c14527 --- /dev/null +++ b/debian/libcoq-ocaml-dev.install.in @@ -0,0 +1,19 @@ +usr/lib/coq/clib/clib.cma +usr/lib/coq/engine/engine.cma +usr/lib/coq/grammar/grammar.cma +usr/lib/coq/interp/interp.cma +usr/lib/coq/intf/intf.cma +usr/lib/coq/kernel/kernel.cma +usr/lib/coq/lib/lib.cma +usr/lib/coq/library/library.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/tactics.cma +usr/lib/coq/toplevel/toplevel.cma +usr/lib/coq/vernac/vernac.cma +usr/lib/coq/META +# 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..44d87c81 --- /dev/null +++ b/debian/libcoq-ocaml.install.in @@ -0,0 +1,55 @@ +usr/lib/coq/dllcoqrun.so @OCamlDllDir@ +usr/lib/coq/plugins/rtauto/rtauto_plugin.cmo +usr/lib/coq/plugins/extraction/extraction_plugin.cmo +usr/lib/coq/plugins/cc/cc_plugin.cmo +usr/lib/coq/plugins/btauto/btauto_plugin.cmo +usr/lib/coq/plugins/fourier/fourier_plugin.cmo +usr/lib/coq/plugins/funind/recdef_plugin.cmo +usr/lib/coq/plugins/derive/derive_plugin.cmo +usr/lib/coq/plugins/setoid_ring/newring_plugin.cmo +usr/lib/coq/plugins/ltac/ltac_plugin.cmo +usr/lib/coq/plugins/ltac/tauto_plugin.cmo +usr/lib/coq/plugins/nsatz/nsatz_plugin.cmo +usr/lib/coq/plugins/micromega/micromega_plugin.cmo +usr/lib/coq/plugins/romega/romega_plugin.cmo +usr/lib/coq/plugins/omega/omega_plugin.cmo +usr/lib/coq/plugins/firstorder/ground_plugin.cmo +usr/lib/coq/plugins/quote/quote_plugin.cmo +usr/lib/coq/plugins/syntax/int31_syntax_plugin.cmo +usr/lib/coq/plugins/syntax/r_syntax_plugin.cmo +usr/lib/coq/plugins/syntax/nat_syntax_plugin.cmo +usr/lib/coq/plugins/syntax/ascii_syntax_plugin.cmo +usr/lib/coq/plugins/syntax/string_syntax_plugin.cmo +usr/lib/coq/plugins/syntax/z_syntax_plugin.cmo +usr/lib/coq/plugins/ssr/ssreflect_plugin.cmo +usr/lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmo +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/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/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/ltac/ltac_plugin.cmxs +DYN: usr/lib/coq/plugins/ltac/tauto_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/quote/quote_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/int31_syntax_plugin.cmxs +DYN: usr/lib/coq/plugins/syntax/ascii_syntax_plugin.cmxs +DYN: usr/lib/coq/plugins/syntax/string_syntax_plugin.cmxs +DYN: usr/lib/coq/plugins/ssr/ssreflect_plugin.cmxs +DYN: usr/lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmxs diff --git a/debian/not-installed b/debian/not-installed new file mode 100644 index 00000000..8bc34b46 --- /dev/null +++ b/debian/not-installed @@ -0,0 +1,7 @@ +# CoqIDE is temporarily disabled. +usr/share/man/man1/coqide.1 +usr/lib/coq/toploop/coqidetop.cmxs + +# `make install` installs this to its expected location; `make install-byte` +# additionally installs it here. +usr/lib/coq/kernel/byterun/dllcoqrun.so 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..2cf6af5c --- /dev/null +++ b/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch @@ -0,0 +1,29 @@ +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 e38affd..040169e 100644 +--- a/test-suite/success/Nsatz.v ++++ b/test-suite/success/Nsatz.v +@@ -462,6 +462,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 -> +@@ -473,6 +474,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/0002-Remove-test-4429.patch b/debian/patches/0002-Remove-test-4429.patch new file mode 100644 index 00000000..9baee306 --- /dev/null +++ b/debian/patches/0002-Remove-test-4429.patch @@ -0,0 +1,46 @@ +From: Enrico Tassi <gareuselesinge@debian.org> +Date: Thu, 28 Jan 2016 10:11:08 +0100 +Subject: Remove test 4429 + +--- + test-suite/bugs/closed/4429.v | 31 ------------------------------- + 1 file changed, 31 deletions(-) + delete mode 100644 test-suite/bugs/closed/4429.v + +diff --git a/test-suite/bugs/closed/4429.v b/test-suite/bugs/closed/4429.v +deleted file mode 100644 +index bf0e570..0000000 +--- a/test-suite/bugs/closed/4429.v ++++ /dev/null +@@ -1,31 +0,0 @@ +-Require Import Arith.Compare_dec. +-Require Import Unicode.Utf8. +- +-Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A := +- match n with +- | O => x +- | S n' => f (my_nat_iter n' f x) +- end. +- +-Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat := +- match mn with +- | (0, 0) => 0 +- | (0, S n') => S n' +- | (S m', 0) => S m' +- | (S m', S n') => +- match le_gt_dec (S m') (S n') with +- | left _ => f (S m', S n' - S m') +- | right _ => f (S m' - S n', S n') +- end +- end. +- +-Axiom max_correct_l : ∀ m n : nat, m <= max m n. +-Axiom max_correct_r : ∀ m n : nat, n <= max m n. +- +-Hint Resolve max_correct_l max_correct_r : arith. +- +-Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')). +-Proof. +- intros. +- Timeout 3 eauto with arith. +-Qed. diff --git a/debian/patches/0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch b/debian/patches/0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch new file mode 100644 index 00000000..45acd396 --- /dev/null +++ b/debian/patches/0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch @@ -0,0 +1,1717 @@ +From: Enrico Tassi <gareuselesinge@debian.org> +Date: Wed, 28 Dec 2016 18:18:34 +0100 +Subject: Remove 3441.v and 4811.v due to timeout on small platforms +--- a/test-suite/bugs/closed/3441.v ++++ /dev/null +@@ -1,23 +0,0 @@ +-Axiom f : nat -> nat -> nat. +-Fixpoint do_n (n : nat) (k : nat) := +- match n with +- | 0 => k +- | S n' => do_n n' (f k k) +- end. +- +-Notation big := (_ = _). +-Axiom k : nat. +-Goal True. +-Timeout 1 let H := fresh "H" in +- let x := constr:(let n := 17 in do_n n = do_n n) in +- let y := (eval lazy in x) in +- pose proof y as H. (* Finished transaction in 1.102 secs (1.084u,0.016s) (successful) *) +-Timeout 1 let H := fresh "H" in +- let x := constr:(let n := 17 in do_n n = do_n n) in +- let y := (eval lazy in x) in +- pose y as H; clearbody H. (* Finished transaction in 0.412 secs (0.412u,0.s) (successful) *) +- +-Timeout 1 Time let H := fresh "H" in +- let x := constr:(let n := 17 in do_n n = do_n n) in +- let y := (eval lazy in x) in +- assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *) +--- a/test-suite/bugs/closed/4811.v ++++ /dev/null +@@ -1,1685 +0,0 @@ +-(* Test about a slowness of f_equal in 8.5pl1 *) +- +-(* Submitted by Jason Gross *) +- +-(* -*- mode: coq; coq-prog-args: ("-R" "src" "Crypto" "-R" "Bedrock" "Bedrock" "-R" "coqprime-8.5/Coqprime" "Coqprime" "-top" "GF255192") -*- *) +-(* File reduced by coq-bug-finder from original input, then from 162 lines to 23 lines, then from 245 lines to 95 lines, then from 198 lines to 101 lines, then from 654 lines to 452 lines, then from 591 lines to 505 lines, then from 1770 lines to 580 lines, then from 2238 lines to 1715 lines, then from 1776 lines to 1738 lines, then from 1750 lines to 1679 lines, then from 1693 lines to 1679 lines *) +-(* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3 +- coqtop version 8.5pl1 (April 2016) *) +-Require Coq.ZArith.ZArith. +- +-Import Coq.ZArith.ZArith. +- +-Axiom F : Z -> Set. +-Definition Let_In {A P} (x : A) (f : forall y : A, P y) +- := let y := x in f y. +-Local Open Scope Z_scope. +-Definition modulus : Z := 2^255 - 19. +-Axiom decode : list Z -> F modulus. +-Goal forall x9 x8 x7 x6 x5 x4 x3 x2 x1 x0 y9 y8 y7 y6 y5 y4 y3 y2 y1 y0 : Z, +- let Zmul := Z.mul in +- let Zadd := Z.add in +- let Zsub := Z.sub in +- let Zpow_pos := Z.pow_pos in +- @eq (F (Zsub (Zpow_pos (Zpos (xO xH)) (xI (xI (xI (xI (xI (xI (xI xH)))))))) (Zpos (xI (xI (xO (xO xH))))))) +- (@decode +- (@Let_In Z (fun _ : Z => list Z) +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) (Zmul (Zmul x7 y3) (Zpos (xO xH)))) +- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (fun z : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) (Zmul x5 y6)) +- (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) +- (fun z0 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z0 (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (fun z1 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z1 (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) (Zmul x5 y8)) +- (Zmul x4 y9))))) +- (fun z2 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z2 (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) +- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (fun z3 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z3 (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) (Zmul x1 y4)) +- (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) +- (fun z4 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z4 (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) +- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) +- (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) +- (fun z5 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z5 (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) +- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (fun z6 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z6 (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) +- (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) +- (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) +- (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) +- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) +- (fun z7 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z7 (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) +- (Zmul x5 y4)) (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) +- (Zmul x1 y8)) (Zmul x0 y9))) +- (fun z8 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Zmul (Zpos (xI (xI (xO (xO xH))))) (Z.shiftr z8 (Zpos (xI (xO (xO (xI xH))))))) +- (Z.land z +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) +- (fun z9 : Z => +- @cons Z +- (Z.land z9 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Zadd (Z.shiftr z9 (Zpos (xO (xI (xO (xI xH)))))) +- (Z.land z0 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land z1 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land z2 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land z3 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land z4 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land z5 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land z6 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land z7 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land z8 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@nil Z))))))))))))))))))))))) +- (@decode +- (@cons Z +- (Z.land +- (Zadd +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y1) +- (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul +- (Zmul x7 y3) +- (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) +- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x9 y2) (Zmul x8 y3)) +- (Zmul x7 y4)) +- (Zmul x6 y5)) +- (Zmul x5 y6)) +- (Zmul x4 y7)) (Zmul x3 y8)) +- (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) +- (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) +- (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) +- (Zmul x6 y7)) (Zmul x5 y8)) +- (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) +- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) +- (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) +- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) +- (Zmul x1 y4)) (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) +- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) +- (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) +- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) +- (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) +- (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) +- (Zmul x0 y8)) (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) (Zmul x5 y4)) +- (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) (Zmul x1 y8)) (Zmul x0 y9))) +- (Zpos (xI (xO (xO (xI xH))))))) +- (Z.land +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) +- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Zadd +- (Z.shiftr +- (Zadd +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y1) +- (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul +- (Zmul x7 y3) +- (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul +- (Zmul x5 y5) +- (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) +- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul x9 y2) +- (Zmul x8 y3)) +- (Zmul x7 y4)) +- (Zmul x6 y5)) +- (Zmul x5 y6)) +- (Zmul x4 y7)) +- (Zmul x3 y8)) +- (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zmul x2 y0) +- (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul (Zmul x9 y3) (Zpos (xO xH))) +- (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) +- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) +- (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) +- (Zmul x7 y6)) (Zmul x6 y7)) +- (Zmul x5 y8)) (Zmul x4 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) +- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) +- (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) +- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) +- (Zmul x2 y3)) (Zmul x1 y4)) (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) +- (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) +- (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) +- (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) +- (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) +- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) +- (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) +- (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) +- (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) +- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) +- (Zmul x5 y4)) (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) +- (Zmul x1 y8)) (Zmul x0 y9))) (Zpos (xI (xO (xO (xI xH))))))) +- (Z.land +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) (Zmul x5 y6)) +- (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) +- (Zmul x5 y6)) (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) +- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) +- (Zmul x5 y6)) (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) (Zmul x5 y8)) +- (Zmul x4 y9))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) +- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) +- (Zmul x6 y5)) (Zmul x5 y6)) (Zmul x4 y7)) +- (Zmul x3 y8)) (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) (Zmul x4 y8)) +- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) +- (Zmul x5 y8)) (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) +- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) +- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) +- (Zmul x6 y5)) (Zmul x5 y6)) +- (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) +- (Zmul x5 y8)) (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) +- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) +- (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) (Zmul x1 y4)) +- (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul (Zmul x9 y1) (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) +- (Zmul x7 y4)) (Zmul x6 y5)) +- (Zmul x5 y6)) (Zmul x4 y7)) +- (Zmul x3 y8)) (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) +- (Zmul x8 y4)) (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) +- (Zmul x6 y7)) (Zmul x5 y8)) (Zmul x4 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) +- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) +- (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) +- (Zmul x1 y4)) (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) +- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) +- (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y1) +- (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul +- (Zmul x7 y3) +- (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) +- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x9 y2) (Zmul x8 y3)) +- (Zmul x7 y4)) +- (Zmul x6 y5)) +- (Zmul x5 y6)) +- (Zmul x4 y7)) (Zmul x3 y8)) +- (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) +- (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) +- (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) +- (Zmul x6 y7)) (Zmul x5 y8)) +- (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) +- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) +- (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) +- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) +- (Zmul x1 y4)) (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) +- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) +- (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) +- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y1) +- (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul +- (Zmul x7 y3) +- (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul +- (Zmul x5 y5) +- (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul +- (Zmul x3 y7) +- (Zpos (xO xH)))) +- (Zmul x2 y8)) +- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul x9 y2) +- (Zmul x8 y3)) +- (Zmul x7 y4)) +- (Zmul x6 y5)) +- (Zmul x5 y6)) +- (Zmul x4 y7)) +- (Zmul x3 y8)) +- (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zmul x2 y0) +- (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y3) +- (Zpos (xO xH))) +- (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) +- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) +- (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) +- (Zmul x7 y6)) (Zmul x6 y7)) +- (Zmul x5 y8)) (Zmul x4 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) +- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) +- (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) +- (Zmul x8 y6)) (Zmul (Zmul x7 y7) (Zpos (xO xH)))) +- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) +- (Zmul x2 y3)) (Zmul x1 y4)) (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) +- (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) +- (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) +- (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) +- (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) +- (Zmul x4 y3)) (Zmul x3 y4)) (Zmul x2 y5)) +- (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) +- (Zmul x6 y2)) (Zmul (Zmul x5 y3) (Zpos (xO xH)))) +- (Zmul x4 y4)) (Zmul (Zmul x3 y5) (Zpos (xO xH)))) +- (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) +- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul +- (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y1) +- (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul +- (Zmul x7 y3) +- (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul +- (Zmul x5 y5) +- (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul +- (Zmul x3 y7) +- (Zpos (xO xH)))) +- (Zmul x2 y8)) +- (Zmul +- (Zmul x1 y9) +- (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul x9 y2) +- (Zmul x8 y3)) +- (Zmul x7 y4)) +- (Zmul x6 y5)) +- (Zmul x5 y6)) +- (Zmul x4 y7)) +- (Zmul x3 y8)) +- (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zmul x2 y0) +- (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y3) +- (Zpos (xO xH))) +- (Zmul x8 y4)) +- (Zmul +- (Zmul x7 y5) +- (Zpos (xO xH)))) +- (Zmul x6 y6)) +- (Zmul +- (Zmul x5 y7) +- (Zpos (xO xH)))) +- (Zmul x4 y8)) +- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) +- (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x9 y4) (Zmul x8 y5)) +- (Zmul x7 y6)) +- (Zmul x6 y7)) +- (Zmul x5 y8)) +- (Zmul x4 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x4 y0) +- (Zmul (Zmul x3 y1) (Zpos (xO xH)))) +- (Zmul x2 y2)) +- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) +- (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) +- (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) +- (Zmul x6 y8)) +- (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) +- (Zmul x2 y3)) (Zmul x1 y4)) +- (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) +- (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x6 y0) +- (Zmul (Zmul x5 y1) (Zpos (xO xH)))) +- (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) +- (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) +- (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) +- (Zmul x4 y3)) (Zmul x3 y4)) (Zmul x2 y5)) +- (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) +- (Zmul x6 y2)) (Zmul (Zmul x5 y3) (Zpos (xO xH)))) +- (Zmul x4 y4)) (Zmul (Zmul x3 y5) (Zpos (xO xH)))) +- (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) +- (Zmul x0 y8)) +- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) +- (Zmul x6 y3)) (Zmul x5 y4)) (Zmul x4 y5)) +- (Zmul x3 y6)) (Zmul x2 y7)) (Zmul x1 y8)) (Zmul x0 y9))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@nil Z)))))))))))). +- cbv beta zeta. +- intros. +- (timeout 1 (apply f_equal; reflexivity)) || fail 0 "too early". +- Undo. +- Time Timeout 1 f_equal. (* Finished transaction in 0. secs (0.3u,0.s) in 8.4 *) diff --git a/debian/patches/0004-5127-fails-on-mips.patch b/debian/patches/0004-5127-fails-on-mips.patch new file mode 100644 index 00000000..949c33a7 --- /dev/null +++ b/debian/patches/0004-5127-fails-on-mips.patch @@ -0,0 +1,30 @@ +From: Enrico Tassi <gareuselesinge@debian.org> +Date: Thu, 29 Dec 2016 08:56:45 +0100 +Subject: 5127 fails on mips + +--- + test-suite/bugs/closed/5127.v | 15 --------------- + 1 file changed, 15 deletions(-) + delete mode 100644 test-suite/bugs/closed/5127.v + +diff --git a/test-suite/bugs/closed/5127.v b/test-suite/bugs/closed/5127.v +deleted file mode 100644 +index 831e8fb..0000000 +--- a/test-suite/bugs/closed/5127.v ++++ /dev/null +@@ -1,15 +0,0 @@ +-Fixpoint arrow (n: nat) := +- match n with +- | S n => bool -> arrow n +- | O => bool +- end. +- +-Fixpoint apply (n : nat) : arrow n -> bool := +- match n return arrow n -> bool with +- | S n => fun f => apply _ (f true) +- | O => fun x => x +- end. +- +-Axiom f : arrow 10000. +-Definition v : bool := Eval compute in apply _ f. +-Definition w : bool := Eval vm_compute in v. diff --git a/debian/patches/0005-remove-tests-that-need-coqlib.patch b/debian/patches/0005-remove-tests-that-need-coqlib.patch new file mode 100644 index 00000000..48cd1b96 --- /dev/null +++ b/debian/patches/0005-remove-tests-that-need-coqlib.patch @@ -0,0 +1,633 @@ +From: Benjamin Barenblat <bbaren@debian.org> +Subject: Disable tests which require -coqlib to be set +Bug: https://github.com/coq/coq/issues/5975 +Forwarded: not-needed + +A number of tests (mostly for coq_makefile) assume that Coq is +installed when the test runs. This isn't true in an sbuild environment, +though, so disable those tests. +--- a/test-suite/misc/printers.sh ++++ /dev/null +@@ -1,3 +0,0 @@ +-printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | egrep "Error|Unbound" +-if [ $? = 0 ]; then exit 1; else exit 0; fi +- +--- a/test-suite/coq-makefile/arg/run.sh ++++ /dev/null +@@ -1,7 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +--- a/test-suite/coq-makefile/compat-subdirs/run.sh ++++ /dev/null +@@ -1,8 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-exec test -f "subdir/done" +--- a/test-suite/coq-makefile/coqdoc1/run.sh ++++ /dev/null +@@ -1,51 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-make html mlihtml +-make install DSTROOT="$PWD/tmp" +-make install-doc DSTROOT="$PWD/tmp" +-#make debug +-(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort -u > desired <<EOT +-. +-./test +-./test/test_plugin.cmi +-./test/test_plugin.cmx +-./test/test_plugin.cmxa +-./test/test_plugin.cmxs +-./test/test.glob +-./test/test.v +-./test/test.vo +-./test/sub +-./test/sub/testsub.glob +-./test/sub/testsub.v +-./test/sub/testsub.vo +-./test/mlihtml +-./test/mlihtml/index_exceptions.html +-./test/mlihtml/index.html +-./test/mlihtml/index_class_types.html +-./test/mlihtml/type_Test_aux.html +-./test/mlihtml/index_module_types.html +-./test/mlihtml/index_classes.html +-./test/mlihtml/type_Test.html +-./test/mlihtml/style.css +-./test/mlihtml/index_attributes.html +-./test/mlihtml/index_types.html +-./test/mlihtml/Test_aux.html +-./test/mlihtml/index_values.html +-./test/mlihtml/Test.html +-./test/mlihtml/index_extensions.html +-./test/mlihtml/index_methods.html +-./test/mlihtml/index_modules.html +-./test/html +-./test/html/index.html +-./test/html/test.sub.testsub.html +-./test/html/toc.html +-./test/html/coqdoc.css +-./test/html/test.test.html +-EOT +-exec diff -u desired actual +--- a/test-suite/coq-makefile/coqdoc2/run.sh ++++ /dev/null +@@ -1,51 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-make html mlihtml +-make install DSTROOT="$PWD/tmp" +-make install-doc DSTROOT="$PWD/tmp" +-#make debug +-(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort -u > desired <<EOT +-. +-./test +-./test/test_plugin.cmi +-./test/test_plugin.cmx +-./test/test_plugin.cmxa +-./test/test_plugin.cmxs +-./test/test.glob +-./test/test.v +-./test/test.vo +-./test/sub +-./test/sub/testsub.glob +-./test/sub/testsub.v +-./test/sub/testsub.vo +-./test/mlihtml +-./test/mlihtml/index_exceptions.html +-./test/mlihtml/index.html +-./test/mlihtml/index_class_types.html +-./test/mlihtml/type_Test_aux.html +-./test/mlihtml/index_module_types.html +-./test/mlihtml/index_classes.html +-./test/mlihtml/type_Test.html +-./test/mlihtml/style.css +-./test/mlihtml/index_attributes.html +-./test/mlihtml/index_types.html +-./test/mlihtml/Test_aux.html +-./test/mlihtml/index_values.html +-./test/mlihtml/Test.html +-./test/mlihtml/index_extensions.html +-./test/mlihtml/index_methods.html +-./test/mlihtml/index_modules.html +-./test/html +-./test/html/index.html +-./test/html/test.sub.testsub.html +-./test/html/toc.html +-./test/html/coqdoc.css +-./test/html/test.test.html +-EOT +-exec diff -u desired actual +--- a/test-suite/coq-makefile/emptyprefix/run.sh ++++ /dev/null +@@ -1,17 +0,0 @@ +-#!/usr/bin/env bash +- +-set -e +- +-. ../template/init.sh +- +-mv theories/sub theories2 +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +- +-cp ../_CoqProject.sub theories2/_CoqProject +-cd theories2 +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +--- a/test-suite/coq-makefile/extend-subdirs/run.sh ++++ /dev/null +@@ -1,8 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-exec test -f "subdir/done" +--- a/test-suite/coq-makefile/findlib-package/run.sh ++++ /dev/null +@@ -1,18 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-echo "let () = Foolib.foo ();;" >> src/test_aux.ml +-export OCAMLPATH=$OCAMLPATH:$PWD/findlib +-if which cygpath 2>/dev/null; then +- # the only way I found to pass OCAMLPATH on win is to have it contain +- # only one entry +- export OCAMLPATH=`cygpath -w $PWD/findlib` +-fi +-make -C findlib/foo clean +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-cat Makefile.local +-make -C findlib/foo +-make +-make byte +--- a/test-suite/coq-makefile/latex1/run.sh ++++ /dev/null +@@ -1,13 +0,0 @@ +-#!/usr/bin/env bash +- +-if which pdflatex; then +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-exec make all.pdf +- +-fi +-exit 0 # test skipped +--- a/test-suite/coq-makefile/merlin1/run.sh ++++ /dev/null +@@ -1,13 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make .merlin +-cat > desired <<EOT +-B src +-S src +-EOT +-tail -2 .merlin > actual +-exec diff -u desired actual +--- a/test-suite/coq-makefile/mlpack1/run.sh ++++ /dev/null +@@ -1,23 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-make html mlihtml +-make install DSTROOT="$PWD/tmp" +-#make debug +-(cd `find tmp -name user-contrib` && find .) | sort > actual +-sort > desired <<EOT +-. +-./test +-./test/test.glob +-./test/test_plugin.cmi +-./test/test_plugin.cmx +-./test/test_plugin.cmxa +-./test/test_plugin.cmxs +-./test/test.v +-./test/test.vo +-EOT +-exec diff -u desired actual +--- a/test-suite/coq-makefile/mlpack2/run.sh ++++ /dev/null +@@ -1,23 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-make html mlihtml +-make install DSTROOT="$PWD/tmp" +-#make debug +-(cd `find tmp -name user-contrib` && find .) | sort > actual +-sort > desired <<EOT +-. +-./test +-./test/test.glob +-./test/test_plugin.cmi +-./test/test_plugin.cmx +-./test/test_plugin.cmxa +-./test/test_plugin.cmxs +-./test/test.v +-./test/test.vo +-EOT +-exec diff -u desired actual +--- a/test-suite/coq-makefile/multiroot/run.sh ++++ /dev/null +@@ -1,56 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-cp -r theories theories2 +-mv src/test_plugin.mlpack src/test_plugin.mllib +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-make html mlihtml +-make install DSTROOT="$PWD/tmp" +-make install-doc DSTROOT="$PWD/tmp" +-#make debug +-(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort > desired <<EOT +-. +-./test +-./test/test.glob +-./test/test.cmi +-./test/test.cmx +-./test/test_aux.cmi +-./test/test_aux.cmx +-./test/test_plugin.cmxa +-./test/test_plugin.cmxs +-./test/test.v +-./test/test.vo +-./test2 +-./test2/test.glob +-./test2/test.v +-./test2/test.vo +-./orphan_test_test2_test +-./orphan_test_test2_test/html +-./orphan_test_test2_test/html/coqdoc.css +-./orphan_test_test2_test/html/index.html +-./orphan_test_test2_test/html/test2.test.html +-./orphan_test_test2_test/html/test.test.html +-./orphan_test_test2_test/html/toc.html +-./orphan_test_test2_test/mlihtml +-./orphan_test_test2_test/mlihtml/index_attributes.html +-./orphan_test_test2_test/mlihtml/index_classes.html +-./orphan_test_test2_test/mlihtml/index_class_types.html +-./orphan_test_test2_test/mlihtml/index_exceptions.html +-./orphan_test_test2_test/mlihtml/index_extensions.html +-./orphan_test_test2_test/mlihtml/index.html +-./orphan_test_test2_test/mlihtml/index_methods.html +-./orphan_test_test2_test/mlihtml/index_modules.html +-./orphan_test_test2_test/mlihtml/index_module_types.html +-./orphan_test_test2_test/mlihtml/index_types.html +-./orphan_test_test2_test/mlihtml/index_values.html +-./orphan_test_test2_test/mlihtml/style.css +-./orphan_test_test2_test/mlihtml/Test_aux.html +-./orphan_test_test2_test/mlihtml/Test.html +-./orphan_test_test2_test/mlihtml/type_Test_aux.html +-./orphan_test_test2_test/mlihtml/type_Test.html +-EOT +-exec diff -u desired actual +--- a/test-suite/coq-makefile/only/run.sh ++++ /dev/null +@@ -1,10 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make only TGTS="src/test.cmi src/test_aux.cmi" -j2 +-test -f src/test.cmi +-test -f src/test_aux.cmi +-! test -f src/test.cmo +--- a/test-suite/coq-makefile/plugin1/run.sh ++++ /dev/null +@@ -1,26 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-mv src/test_plugin.mlpack src/test_plugin.mllib +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-make html mlihtml +-make install DSTROOT="$PWD/tmp" +-#make debug +-(cd `find tmp -name user-contrib` && find .) | sort > actual +-sort > desired <<EOT +-. +-./test +-./test/test.glob +-./test/test.cmi +-./test/test.cmx +-./test/test_aux.cmi +-./test/test_aux.cmx +-./test/test_plugin.cmxa +-./test/test_plugin.cmxs +-./test/test.v +-./test/test.vo +-EOT +-exec diff -u desired actual +--- a/test-suite/coq-makefile/plugin2/run.sh ++++ /dev/null +@@ -1,26 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-mv src/test_plugin.mlpack src/test_plugin.mllib +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-make html mlihtml +-make install DSTROOT="$PWD/tmp" +-#make debug +-(cd `find tmp -name user-contrib` && find .) | sort > actual +-sort > desired <<EOT +-. +-./test +-./test/test.glob +-./test/test.cmi +-./test/test.cmx +-./test/test_aux.cmi +-./test/test_aux.cmx +-./test/test_plugin.cmxa +-./test/test_plugin.cmxs +-./test/test.v +-./test/test.vo +-EOT +-exec diff -u desired actual +--- a/test-suite/coq-makefile/plugin3/run.sh ++++ /dev/null +@@ -1,26 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-mv src/test_plugin.mlpack src/test_plugin.mllib +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-make html mlihtml +-make install DSTROOT="$PWD/tmp" +-#make debug +-(cd `find tmp -name user-contrib` && find .) | sort > actual +-sort > desired <<EOT +-. +-./test +-./test/test.glob +-./test/test.cmi +-./test/test.cmx +-./test/test_aux.cmi +-./test/test_aux.cmx +-./test/test_plugin.cmxa +-./test/test_plugin.cmxs +-./test/test.v +-./test/test.vo +-EOT +-exec diff -u desired actual +--- a/test-suite/coq-makefile/quick2vo/run.sh ++++ /dev/null +@@ -1,12 +0,0 @@ +-#!/usr/bin/env bash +-a=`uname` +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-# vio2vo is broken on Windows (#6720) +-if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then +- make quick2vo J=2 +- test -f theories/test.vo +- make validate +-fi +--- a/test-suite/coq-makefile/uninstall1/run.sh ++++ /dev/null +@@ -1,18 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-make html mlihtml +-make install DSTROOT="$PWD/tmp" +-make install-doc DSTROOT="$PWD/tmp" +-make uninstall DSTROOT="$PWD/tmp" +-make uninstall-doc DSTROOT="$PWD/tmp" +-#make debug +-(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort -u > desired <<EOT +-. +-EOT +-exec diff -u desired actual +--- a/test-suite/coq-makefile/uninstall2/run.sh ++++ /dev/null +@@ -1,18 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-make html mlihtml +-make install DSTROOT="$PWD/tmp" +-make install-doc DSTROOT="$PWD/tmp" +-make uninstall DSTROOT="$PWD/tmp" +-make uninstall-doc DSTROOT="$PWD/tmp" +-#make debug +-(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort -u > desired <<EOT +-. +-EOT +-exec diff -u desired actual +--- a/test-suite/coq-makefile/validate1/run.sh ++++ /dev/null +@@ -1,8 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-exec make validate +--- a/test-suite/coq-makefile/vio2vo/run.sh ++++ /dev/null +@@ -1,13 +0,0 @@ +-#!/usr/bin/env bash +-a=`uname` +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-make quick +-# vio2vo is broken on Windows (#6720) +-if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then +- make vio2vo J=2 +- test -f theories/test.vo +- make validate +-fi +--- a/test-suite/coq-makefile/timing/run.sh ++++ /dev/null +@@ -1,108 +0,0 @@ +-#!/usr/bin/env bash +- +-#set -x +-set -e +- +-. ../template/path-init.sh +- +-# reset MAKEFLAGS so that, e.g., `make -C test-suite -B coq-makefile` doesn't give us issues +- +-MAKEFLAGS= +- +-cd precomputed-time-tests +-./run.sh || exit $? +- +-cd ../error +-coq_makefile -f _CoqProject -o Makefile +-make cleanall +-if make pretty-timed TGTS="all" -j1; then +- echo "Error: make pretty-timed should have failed" +- exit 1 +-fi +- +-cd ../aggregate +-coq_makefile -f _CoqProject -o Makefile +-make cleanall +-make pretty-timed TGTS="all" -j1 || exit $? +- +-cd ../before +-coq_makefile -f _CoqProject -o Makefile +-make cleanall +-make make-pretty-timed-before TGTS="all" -j1 || exit $? +- +-cd ../after +-coq_makefile -f _CoqProject -o Makefile +-make cleanall +-make make-pretty-timed-after TGTS="all" -j1 || exit $? +-rm -f time-of-build-before.log +-make print-pretty-timed-diff TIMING_SORT_BY=diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log +-cp ../before/time-of-build-before.log ./ +-make print-pretty-timed-diff TIMING_SORT_BY=diff || exit $? +- +-INFINITY="∞" +-INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected the time to increase +- +-TO_SED_IN_BOTH=( +- -e s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" # Whether or not something shows up as ∞ depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent +- -e s':|\s*N/A\s*$:| '"${INFINITY_REPLACEMENT}"':g' # Whether or not something shows up as N/A depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent +- -e s'/ *$//g' # the number of trailing spaces depends on how many digits percentages end up being; since this varies across runs, we remove trailing spaces +- -e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out +- -e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators +- -e s'/+/-/g' # some code lines don't really change, but this can show up as either -0m00.01s or +0m00.01s, so we need to normalize the signs; additionally, some N/A's show up where we expect to get -∞ on the per-line file, and so the ∞-replacement gets the sign wrong, so we must correct it +-) +- +-TO_SED_IN_PER_FILE=( +- -e s'/[0-9]//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start +- -e s'/ */ /g' # unclear whether this is actually needed for per-file timing; it's been here from the start +- -e s'/\(Total.*\)-\(.*\)-/\1+\2+/g' # Overall time in the per-file timing diff should be around 0; if it comes out negative, we remove the sign +-) +- +-TO_SED_IN_PER_LINE=( +- -e s'/0//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start +- -e s'/ */ /g' # Sometimes 0 will show up as 0m00.s, sometimes it'll end up being more like 0m00.001s; we must strip out the spaces that result from left-aligning numbers of different widths based on how many digits Coq's [-time] gives +- ) +- +-for ext in "" .desired; do +- for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do +- cat ${file}${ext} | grep -v 'warning: undefined variable' | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed +- done +-done +-for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do +- echo "cat $file" +- cat "$file" +- echo +- diff -u $file.desired.processed $file.processed || exit $? +-done +- +-cd ../per-file-before +-coq_makefile -f _CoqProject -o Makefile +-make cleanall +-make all TIMING=before -j2 || exit $? +- +-cd ../per-file-after +-coq_makefile -f _CoqProject -o Makefile +-make cleanall +-make all TIMING=after -j2 || exit $? +- +-find ../per-file-before/ -name "*.before-timing" -exec 'cp' '{}' './' ';' +-make all.timing.diff -j2 || exit $? +-echo "cat A.v.before-timing" +-cat A.v.before-timing +-echo +-echo "cat A.v.after-timing" +-cat A.v.after-timing +-echo +-echo "cat A.v.timing.diff" +-cat A.v.timing.diff +-echo +- +-for ext in "" .desired; do +- for file in A.v.timing.diff; do +- cat ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" | sort > ${file}${ext}.processed +- done +-done +-for file in A.v.timing.diff; do +- diff -u $file.desired.processed $file.processed || exit $? +-done +- +-exit 0 diff --git a/debian/patches/0006-spelling.patch b/debian/patches/0006-spelling.patch new file mode 100644 index 00000000..149d11b4 --- /dev/null +++ b/debian/patches/0006-spelling.patch @@ -0,0 +1,320 @@ +From: Benjamin Barenblat <bbaren@google.com> +Subject: Correct some spelling errors +Origin: backport, https://github.com/coq/coq/commit/06cd051d140a183229cd43f0bbae152d6ad8d6ca +Reviewed-by: Benjamin Barenblat <bbaren@debian.org> + +Lintian found some spelling errors in the Debian packaging for coq. Fix +them most places they appear in the current source. (Don't change +documentation anchor names, as that would invalidate external +deeplinks.) + +This also fixes a bug in coqdoc: prior to this commit, coqdoc would +highlight `instanciate` but not `instantiate`. +--- a/ide/nanoPG.ml ++++ b/ide/nanoPG.ml +@@ -189,7 +189,7 @@ + run "Edit" "Cut"; + { s with kill = Some(txt,false); sel = false } + else s)); +- mkE _k "k" "Kill untill the end of line" (Edit(fun s b i _ -> ++ mkE _k "k" "Kill until the end of line" (Edit(fun s b i _ -> + let already_killed = match s.kill with Some (k,true) -> k | _ -> "" in + let k = + if i#ends_line then begin +--- a/kernel/clambda.ml ++++ b/kernel/clambda.ml +@@ -767,7 +767,7 @@ + and such, which can't be done at this time. + for instance, for int31: if one of the digit is + not closed, it's not impossible that the number +- gets fully instanciated at run-time, thus to ensure ++ gets fully instantiated at run-time, thus to ensure + uniqueness of the representation in the vm + it is necessary to try and build a caml integer + during the execution *) +--- a/lib/future.ml ++++ b/lib/future.ml +@@ -49,7 +49,7 @@ + module UUIDMap = Map.Make(UUID) + module UUIDSet = Set.Make(UUID) + +-type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] ++type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] + + (* Val is not necessarily a final state, so the + computation restarts from the state stocked into Val *) +@@ -103,7 +103,7 @@ + let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn + + let create_delegate ?(blocking=true) ~name fix_exn = +- let assignement signal ck = fun v -> ++ let assignment signal ck = fun v -> + let _, _, fix_exn, c = get ck in + assert (match !c with Delegated _ -> true | _ -> false); + begin match v with +@@ -118,7 +118,7 @@ + (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock), + (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in + let ck = create ~name fix_exn (Delegated wait) in +- ck, assignement signal ck ++ ck, assignment signal ck + + (* TODO: get rid of try/catch to be stackless *) + let rec compute ck : 'a value = +--- a/lib/future.mli ++++ b/lib/future.mli +@@ -70,10 +70,10 @@ + (* Run remotely, returns the function to assign. + If not blocking (the default) it raises NotReady if forced before the + delegate assigns it. *) +-type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] ++type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] + val create_delegate : + ?blocking:bool -> name:string -> +- fix_exn -> 'a computation * ('a assignement -> unit) ++ fix_exn -> 'a computation * ('a assignment -> unit) + + (* Given a computation that is_exn, replace it by another one *) + val replace : 'a computation -> 'a computation -> unit +--- a/plugins/funind/functional_principles_proofs.ml ++++ b/plugins/funind/functional_principles_proofs.ml +@@ -638,11 +638,11 @@ + (* observe (str "using snd tac since : " ++ CErrors.print e); *) + tac2 g + +-let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = ++let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = + let args = Array.of_list (List.map mkVar args_id) in +- let instanciate_one_hyp hid = ++ let instantiate_one_hyp hid = + my_orelse +- ( (* we instanciate the hyp if possible *) ++ ( (* we instantiate the hyp if possible *) + fun g -> + let prov_hid = pf_get_new_id hid g in + let c = mkApp(mkVar hid,args) in +@@ -678,7 +678,7 @@ + tclTHENLIST + [ + tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps; +- tclMAP instanciate_one_hyp hyps; ++ tclMAP instantiate_one_hyp hyps; + (fun g -> + let all_g_hyps_id = + List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty +@@ -722,11 +722,11 @@ + tclTHENLIST [Proofview.V82.of_tactic (Simple.case t); + (fun g' -> + let g'_nb_prod = nb_prod (project g') (pf_concl g') in +- let nb_instanciate_partial = g'_nb_prod - g_nb_prod in ++ let nb_instantiate_partial = g'_nb_prod - g_nb_prod in + observe_tac "treat_new_case" + (treat_new_case + ptes_infos +- nb_instanciate_partial ++ nb_instantiate_partial + (build_proof do_finalize) + t + dyn_infos) +@@ -760,7 +760,7 @@ + nb_rec_hyps = List.length new_hyps + } + in +-(* observe_tac "Lambda" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' ++(* observe_tac "Lambda" *) (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' + (* build_proof do_finalize new_infos g' *) + ) g + | _ -> +@@ -1118,7 +1118,7 @@ + in + (full_params, (* real params *) + princ_params, (* the params of the principle which are not params of the function *) +- substl (* function instanciated with real params *) ++ substl (* function instantiated with real params *) + (List.map var_of_decl full_params) + f_body + ) +@@ -1128,7 +1128,7 @@ + let f_body = compose_lam f_ctxt_other f_body in + (princ_info.params, (* real params *) + [],(* all params are full params *) +- substl (* function instanciated with real params *) ++ substl (* function instantiated with real params *) + (List.map var_of_decl princ_info.params) + f_body + ) +@@ -1319,7 +1319,7 @@ + (* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *) + + (* ); *) +- (* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac ++ (* observe_tac "instancing" *) (instantiate_hyps_with_args prove_tac + (List.rev_map id_of_decl princ_info.branches) + (List.rev args_id)) + ] +@@ -1369,7 +1369,7 @@ + do_prove + dyn_infos + in +- instanciate_hyps_with_args prove_tac ++ instantiate_hyps_with_args prove_tac + (List.rev_map id_of_decl princ_info.branches) + (List.rev args_id) + ] +@@ -1726,8 +1726,8 @@ + ptes_info + (body_info rec_hyps) + in +- (* observe_tac "instanciate_hyps_with_args" *) +- (instanciate_hyps_with_args ++ (* observe_tac "instantiate_hyps_with_args" *) ++ (instantiate_hyps_with_args + make_proof + (List.map (get_name %> Nameops.Name.get_id) princ_info.branches) + (List.rev args_ids) +--- a/plugins/funind/recdef.ml ++++ b/plugins/funind/recdef.ml +@@ -1318,7 +1318,7 @@ + | None -> + try add_suffix current_proof_name "_subproof" + with e when CErrors.noncritical e -> +- anomaly (Pp.str "open_new_goal with an unamed theorem.") ++ anomaly (Pp.str "open_new_goal with an unnamed theorem.") + in + let na = next_global_ident_away name Id.Set.empty in + if Termops.occur_existential sigma gls_type then +--- a/plugins/omega/PreOmega.v ++++ b/plugins/omega/PreOmega.v +@@ -181,7 +181,7 @@ + let t := eval compute in (Z.of_nat (S a)) in + change (Z.of_nat (S a)) with t in H + | _ => rewrite (Nat2Z.inj_succ a) in H +- | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), ++ | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), + hide [Z.of_nat (S a)] in this one hypothesis *) + change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H + end +@@ -192,7 +192,7 @@ + let t := eval compute in (Z.of_nat (S a)) in + change (Z.of_nat (S a)) with t + | _ => rewrite (Nat2Z.inj_succ a) +- | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), ++ | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), + hide [Z.of_nat (S a)] in the goal *) + change (Z.of_nat (S a)) with (Z_of_nat' (S a)) + end +--- a/plugins/omega/omega.ml ++++ b/plugins/omega/omega.ml +@@ -178,7 +178,7 @@ + | DIVIDE_AND_APPROX (e1,e2,k,d) -> + Printf.printf + "Inequation E%d is divided by %s and the constant coefficient is \ +- rounded by substracting %s.\n" e1.id (sbi k) (sbi d) ++ rounded by subtracting %s.\n" e1.id (sbi k) (sbi d) + | NOT_EXACT_DIVIDE (e,k) -> + Printf.printf + "Constant in equation E%d is not divisible by the pgcd \ +--- a/stm/stm.ml ++++ b/stm/stm.ml +@@ -1343,7 +1343,7 @@ + t_stop : Stateid.t; + t_drop : bool; + t_states : competence; +- t_assign : Proof_global.closed_proof_output Future.assignement -> unit; ++ t_assign : Proof_global.closed_proof_output Future.assignment -> unit; + t_loc : Loc.t option; + t_uuid : Future.UUID.t; + t_name : string } +@@ -1381,7 +1381,7 @@ + t_stop : Stateid.t; + t_drop : bool; + t_states : competence; +- t_assign : Proof_global.closed_proof_output Future.assignement -> unit; ++ t_assign : Proof_global.closed_proof_output Future.assignment -> unit; + t_loc : Loc.t option; + t_uuid : Future.UUID.t; + t_name : string } +@@ -1819,7 +1819,7 @@ + type task = { + t_state : Stateid.t; + t_state_fb : Stateid.t; +- t_assign : output Future.assignement -> unit; ++ t_assign : output Future.assignment -> unit; + t_ast : int * aast; + t_goal : Goal.goal; + t_kill : unit -> unit; +@@ -1836,7 +1836,7 @@ + type task = { + t_state : Stateid.t; + t_state_fb : Stateid.t; +- t_assign : output Future.assignement -> unit; ++ t_assign : output Future.assignment -> unit; + t_ast : int * aast; + t_goal : Goal.goal; + t_kill : unit -> unit; +--- a/test-suite/success/univers.v ++++ b/test-suite/success/univers.v +@@ -60,7 +60,7 @@ + + Record U : Type := { A:=Type; a:A }. + +-(** Check assignement of sorts to inductives and records. *) ++(** Check assignment of sorts to inductives and records. *) + + Variable sh : list nat. + +--- a/tools/coq_makefile.ml ++++ b/tools/coq_makefile.ml +@@ -59,7 +59,7 @@ + \n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\ + \n as a dependencies of an already defined target \"foo\".\ + \n[-I dir]: look for Objective Caml dependencies in \"dir\"\ +-\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\ ++\n[-R physicalpath logicalpath]: look for Coq dependencies recursively\ + \n starting from \"physicalpath\". The logical path associated to the\ + \n physical path is \"logicalpath\".\ + \n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\ +--- a/tools/coqdoc/output.ml ++++ b/tools/coqdoc/output.ml +@@ -76,7 +76,7 @@ + [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; + "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; + "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct"; +- "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto"; ++ "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instantiate"; "info_auto"; "info_eauto"; + "quote"; "eexact"; "autorewrite"; + "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; + "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; +--- a/tools/coqworkmgr.ml ++++ b/tools/coqworkmgr.ml +@@ -169,7 +169,7 @@ + "-j",Arg.Set_int max_tokens, "max number of concurrent jobs"; + "-d",Arg.Set debug, "do not detach (debug)"] in + let usage = +- "Prints on stdout an env variable assignement to be picked up by coq\n"^ ++ "Prints on stdout an env variable assignment to be picked up by coq\n"^ + "instances in order to limit the maximum number of concurrent workers.\n"^ + "The default value is 2.\n"^ + "Usage:" in +--- a/vernac/comProgramFixpoint.ml ++++ b/vernac/comProgramFixpoint.ml +@@ -254,7 +254,7 @@ + interp_recursive ~cofix ~program_mode:true fixl ntns + in + (* Program-specific code *) +- (* Get the interesting evars, those that were not instanciated *) ++ (* Get the interesting evars, those that were not instantiated *) + let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in + (* Solve remaining evars *) + let evd = nf_evar_map_undefined evd in +--- a/vernac/obligations.ml ++++ b/vernac/obligations.ml +@@ -338,7 +338,7 @@ + let _ = + declare_bool_option + { optdepr = false; +- optname = "Hidding of Program obligations"; ++ optname = "Hiding of Program obligations"; + optkey = ["Hide";"Obligations"]; + optread = get_hide_obligations; + optwrite = set_hide_obligations; } diff --git a/debian/patches/0007-avoid-usr-bin-env.patch b/debian/patches/0007-avoid-usr-bin-env.patch new file mode 100644 index 00000000..132ed7aa --- /dev/null +++ b/debian/patches/0007-avoid-usr-bin-env.patch @@ -0,0 +1,32 @@ +From: Benjamin Barenblat <bbaren@debian.org> +Subject: Avoid invoking /usr/bin/env +Forwarded: not-needed + +Per Debian Python policy [1], use `/usr/bin/python3` rather than +`/usr/bin/env python` to refer to the system Python (3) interpreter. + +[1] https://www.debian.org/doc/packaging-manuals/python-policy/python.html#interpreter_loc +--- a/tools/make-both-single-timing-files.py ++++ b/tools/make-both-single-timing-files.py +@@ -1,4 +1,4 @@ +-#!/usr/bin/env python ++#!/usr/bin/python3 + import sys + from TimeFileMaker import * + +--- a/tools/make-both-time-files.py ++++ b/tools/make-both-time-files.py +@@ -1,4 +1,4 @@ +-#!/usr/bin/env python ++#!/usr/bin/python3 + import sys + from TimeFileMaker import * + +--- a/tools/make-one-time-file.py ++++ b/tools/make-one-time-file.py +@@ -1,4 +1,4 @@ +-#!/usr/bin/env python ++#!/usr/bin/python3 + import sys + from TimeFileMaker import * + diff --git a/debian/patches/0008-python-scripts-libraries.patch b/debian/patches/0008-python-scripts-libraries.patch new file mode 100644 index 00000000..66a4a9e9 --- /dev/null +++ b/debian/patches/0008-python-scripts-libraries.patch @@ -0,0 +1,20 @@ +From: Benjamin Barenblat <bbaren@debian.org> +Subject: Differentiate between Python scripts and libraries +Forwarded: not-needed + +Eliminate the .py extension from executable Python scripts. +--- a/tools/CoqMakefile.in ++++ b/tools/CoqMakefile.in +@@ -91,9 +91,9 @@ + COQMKFILE ?= "$(COQBIN)coq_makefile" + + # Timing scripts +-COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" +-COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" +-COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" ++COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file" ++COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files" ++COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files" + BEFORE ?= + AFTER ?= + diff --git a/debian/patches/0009-skip-dot-pc.patch b/debian/patches/0009-skip-dot-pc.patch new file mode 100644 index 00000000..ce85adf8 --- /dev/null +++ b/debian/patches/0009-skip-dot-pc.patch @@ -0,0 +1,13 @@ +From: Benjamin Barenblat <bbaren@debian.org> +Subject: Ignore .pc directory when building +Forwarded: no +--- a/Makefile ++++ b/Makefile +@@ -53,6 +53,7 @@ + -name '.git' -o \ + -name '.bzr' -o \ + -name 'debian' -o \ ++ -name '.pc' -o \ + -name "$${GIT_DIR}" -o \ + -name '_build' -o \ + -name '_build_ci' -o \ diff --git a/debian/patches/series b/debian/patches/series new file mode 100644 index 00000000..d2f569c1 --- /dev/null +++ b/debian/patches/series @@ -0,0 +1,9 @@ +0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch +0002-Remove-test-4429.patch +0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch +0004-5127-fails-on-mips.patch +0005-remove-tests-that-need-coqlib.patch +0006-spelling.patch +0007-avoid-usr-bin-env.patch +0008-python-scripts-libraries.patch +0009-skip-dot-pc.patch diff --git a/debian/rules b/debian/rules new file mode 100755 index 00000000..8ffcd917 --- /dev/null +++ b/debian/rules @@ -0,0 +1,123 @@ +#!/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.8.2 +COQ_ABI := $(COQ_VERSION)+$(OCAML_ABI) + +ARCH := $(shell dpkg-architecture -q DEB_TARGET_ARCH) +ifeq ($(ARCH),$(filter $(ARCH),amd64 i386)) +NATIVE_COMPUTE := +else +NATIVE_COMPUTE := -native-compiler no +endif + +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 &" \ + -coqide no \ + -with-doc no \ + $(NATIVE_COMPUTE) + +export OCAMLINIT_SED += \ + -e 's%@CoqVersion@%$(COQ_VERSION)%' \ + -e 's%@CoqABI@%$(COQ_ABI)%' + +%: + +dh $@ --with ocaml,python3 + +# 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,python3 + +.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) + +# Don't combine `make world` and `make byte`--doing so triggers a race +# in the build system. See upstream's CHANGES. + $(MAKE) world STRIP=true + $(MAKE) byte STRIP=true + $(MAKE) DOC_TARGETS=$(HTMLDOC) $(HTMLDOC) +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: +ifeq (,$(filter nocheck,$(DEB_BUILD_OPTIONS))) + CAML_LD_LIBRARY_PATH=$(shell pwd)/kernel/byterun COQLIB=$(shell pwd) \ + $(MAKE) test-suite COMPLEXITY= +endif + +.PHONY: override_dh_auto_install +override_dh_auto_install: + $(MAKE) $(ADDPREF) install install-byte + 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 + chmod +x debian/coq.install + dh_install --fail-missing + +.PHONY: override_dh_ocaml +override_dh_ocaml: + dh_ocaml + 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..0d3a7a07 --- /dev/null +++ b/debian/watch @@ -0,0 +1,3 @@ +version=4 +opts=filenamemangle=s/.+\/[vV]?(\d\S+)\.tar\.gz/coq-$1\.tar\.gz/ \ + https://github.com/coq/coq/releases .*/[vV]?(\d[^\s+]+)\.tar\.gz |