coq 8.11.0-1 source package in Ubuntu
Changelog
coq (8.11.0-1) unstable; urgency=medium * New upstream release. * Updated patches: - remove-heavy-tests: also remove success/Nia.v - avoid-usr-bin-env.patch: also patch dev/tools/update-compat.py. Thanks to the Gianfranco Costamagna for the hint (closes: #952454) * Refreshed patches: - remove-tests-that-need-coqlib - python-scripts-libraries - skip-dot-pc - verbose-build - remove-bytecode-failing-tests * Removed patches: - ssrmatching-license: fixed by upstream - use-changelog-date: fixed by upstream * New patch: - restore_g_ssrmatching.mli - votour-linking: patch by Hugo Herbelin (thanks!) fixes linking of votour on bytecode architectures * invoke "make test" with PRINT_LOGS=1 as suggested by SkySkimmer (thanks) * disable building of the VM on s390x, as suggested by ejgallego (thanks) This should fix a test failure on s390x (https://github.com/coq/coq/issues/11395) * Dispatch into different binary packages: - simplify find invocation in debian/rules - add *.vos files, new *.cmo, *.cmxs files - add votour and doc_grammar binaries * Add an as-installed test for the compiler and the toplevel * Renamed debian/TODO.Debian to debian/TODO * Bump build-dependency on ocaml to >= 4.05, as indicated by INSTALL -- Ralf Treinen <email address hidden> Thu, 05 Mar 2020 21:37:30 +0100
Upload details
- Uploaded by:
- Debian OCaml Maintainers
- Uploaded to:
- Sid
- Original maintainer:
- Debian OCaml Maintainers
- Architectures:
- any
- Section:
- math
- Urgency:
- Medium Urgency
See full publishing history Publishing
Series | Published | Component | Section | |
---|---|---|---|---|
Focal | release | universe | devel |
Downloads
File | Size | SHA-256 Checksum |
---|---|---|
coq_8.11.0-1.dsc | 2.4 KiB | 3bae766caf927d8865d2a1fe94708f1498bb3af075a7f89a2c73fe45eebefbf6 |
coq_8.11.0.orig.tar.gz | 5.6 MiB | 578344b3f01c89af65b9f9902c4a07df8faa2b8f8ec080a53bd3f7848a91bfd9 |
coq_8.11.0-1.debian.tar.xz | 30.9 KiB | 8ac88e9f07ee7cb9c268457daf2a07f7f8276d3c71ac4449c13fdbbae611e961 |
Available diffs
No changes file available.
Binary packages built by this source
- coq: No summary available for coq in ubuntu groovy.
No description available for coq in ubuntu groovy.
- coq-dbgsym: No summary available for coq-dbgsym in ubuntu groovy.
No description available for coq-dbgsym in ubuntu groovy.
- coq-theories: No summary available for coq-theories in ubuntu groovy.
No description available for coq-theories in ubuntu groovy.
- coq-theories-dbgsym: debug symbols for coq-theories
- coqide: proof assistant for higher-order logic (gtk interface)
Coq is a proof assistant for higher-order logic, which allows the
development of computer programs consistent with their formal
specification. It is developed using Objective Caml and Camlp5.
.
This package provides CoqIde, a graphical user interface for
developing proofs.
- coqide-dbgsym: debug symbols for coqide
- libcoq-ocaml: No summary available for libcoq-ocaml in ubuntu groovy.
No description available for libcoq-ocaml in ubuntu groovy.
- libcoq-ocaml-dbgsym: debug symbols for libcoq-ocaml
- libcoq-ocaml-dev: No summary available for libcoq-ocaml-dev in ubuntu groovy.
No description available for libcoq-ocaml-dev in ubuntu groovy.