Package: coq / 8.20.1+dfsg-1

Metadata

Package Version Patches format
coq 8.20.1+dfsg-1 3.0 (quilt)

Patch series

view the series file
Patch File delta Description
fix_debian_paths.patch | (download)

dev/bench/bench.sh | 2 1 + 1 - 0 !
dev/bench/sort-by-deps | 2 1 + 1 - 0 !
dev/bench/sort-by-deps.sh | 2 1 + 1 - 0 !
dev/ci/ci-aac_tactics.sh | 2 1 + 1 - 0 !
dev/ci/ci-argosy.sh | 2 1 + 1 - 0 !
dev/ci/ci-basic-overlay.sh | 2 1 + 1 - 0 !
dev/ci/ci-bbv.sh | 2 1 + 1 - 0 !
dev/ci/ci-bedrock2.sh | 2 1 + 1 - 0 !
dev/ci/ci-bignums.sh | 2 1 + 1 - 0 !
dev/ci/ci-color.sh | 2 1 + 1 - 0 !
dev/ci/ci-common.sh | 2 1 + 1 - 0 !
dev/ci/ci-coq_dpdgraph.sh | 2 1 + 1 - 0 !
dev/ci/ci-coq_performance_tests.sh | 2 1 + 1 - 0 !
dev/ci/ci-coq_tools.sh | 2 1 + 1 - 0 !
dev/ci/ci-coqhammer.sh | 2 1 + 1 - 0 !
dev/ci/ci-coqprime.sh | 2 1 + 1 - 0 !
dev/ci/ci-coqtail.sh | 2 1 + 1 - 0 !
dev/ci/ci-coquelicot.sh | 2 1 + 1 - 0 !
dev/ci/ci-corn.sh | 2 1 + 1 - 0 !
dev/ci/ci-cross_crypto.sh | 2 1 + 1 - 0 !
dev/ci/ci-deriving.sh | 2 1 + 1 - 0 !
dev/ci/ci-engine_bench.sh | 2 1 + 1 - 0 !
dev/ci/ci-equations.sh | 2 1 + 1 - 0 !
dev/ci/ci-ext_lib.sh | 2 1 + 1 - 0 !
dev/ci/ci-fiat_crypto.sh | 2 1 + 1 - 0 !
dev/ci/ci-fiat_crypto_legacy.sh | 2 1 + 1 - 0 !
dev/ci/ci-fiat_crypto_ocaml.sh | 2 1 + 1 - 0 !
dev/ci/ci-fiat_parsers.sh | 2 1 + 1 - 0 !
dev/ci/ci-flocq.sh | 2 1 + 1 - 0 !
dev/ci/ci-fourcolor.sh | 2 1 + 1 - 0 !
dev/ci/ci-hott.sh | 2 1 + 1 - 0 !
dev/ci/ci-iris.sh | 2 1 + 1 - 0 !
dev/ci/ci-math_classes.sh | 2 1 + 1 - 0 !
dev/ci/ci-mathcomp.sh | 2 1 + 1 - 0 !
dev/ci/ci-mczify.sh | 2 1 + 1 - 0 !
dev/ci/ci-menhir.sh | 2 1 + 1 - 0 !
dev/ci/ci-metacoq.sh | 2 1 + 1 - 0 !
dev/ci/ci-mtac2.sh | 2 1 + 1 - 0 !
dev/ci/ci-oddorder.sh | 2 1 + 1 - 0 !
dev/ci/ci-paramcoq.sh | 2 1 + 1 - 0 !
dev/ci/ci-perennial.sh | 2 1 + 1 - 0 !
dev/ci/ci-quickchick.sh | 2 1 + 1 - 0 !
dev/ci/ci-reduction_effects.sh | 2 1 + 1 - 0 !
dev/ci/ci-relation_algebra.sh | 2 1 + 1 - 0 !
dev/ci/ci-rewriter.sh | 2 1 + 1 - 0 !
dev/ci/ci-sf.sh | 2 1 + 1 - 0 !
dev/ci/ci-simple_io.sh | 2 1 + 1 - 0 !
dev/ci/ci-stdlib2.sh | 2 1 + 1 - 0 !
dev/ci/ci-tlc.sh | 2 1 + 1 - 0 !
dev/ci/ci-unicoq.sh | 2 1 + 1 - 0 !
dev/ci/ci-unimath.sh | 2 1 + 1 - 0 !
dev/ci/ci-verdi_raft.sh | 2 1 + 1 - 0 !
dev/ci/ci-vscoq.sh | 2 1 + 1 - 0 !
dev/ci/ci-vst.sh | 2 1 + 1 - 0 !
dev/ci/ci-wrapper.sh | 2 1 + 1 - 0 !
dev/ci/nix/shell | 2 1 + 1 - 0 !
dev/dune-dbg.in | 2 1 + 1 - 0 !
dev/lint-commits.sh | 2 1 + 1 - 0 !
dev/lint-repository.sh | 2 1 + 1 - 0 !
dev/shim/dune | 8 4 + 4 - 0 !
dev/tools/backport-pr.sh | 2 1 + 1 - 0 !
dev/tools/check-eof-newline.sh | 2 1 + 1 - 0 !
dev/tools/check-overlays.sh | 2 1 + 1 - 0 !
dev/tools/create_overlays.sh | 2 1 + 1 - 0 !
dev/tools/generate-release-changelog.sh | 2 1 + 1 - 0 !
dev/tools/list-contributors.sh | 2 1 + 1 - 0 !
dev/tools/make_git_revision.sh | 2 1 + 1 - 0 !
dev/tools/merge-pr.sh | 2 1 + 1 - 0 !
dev/tools/notify-upstream-pins.sh | 2 1 + 1 - 0 !
dev/tools/pin-ci.sh | 2 1 + 1 - 0 !
dev/tools/update-compat.py | 4 2 + 2 - 0 !
doc/stdlib/make-library-index | 2 1 + 1 - 0 !
doc/tools/coqrst/notations/fontsupport.py | 2 1 + 1 - 0 !
doc/tools/coqrst/regen_readme.py | 2 1 + 1 - 0 !
test-suite/coq-makefile/camldep/run.sh | 2 1 + 1 - 0 !
test-suite/coq-makefile/findlib-package-unpacked/run.sh | 2 1 + 1 - 0 !
test-suite/coq-makefile/local-late-extension/run.sh | 2 1 + 1 - 0 !
test-suite/coq-makefile/missing-install/run.sh | 2 1 + 1 - 0 !
test-suite/coq-makefile/native1/run.sh | 2 1 + 1 - 0 !
test-suite/coq-makefile/native2/run.sh | 2 1 + 1 - 0 !
test-suite/coq-makefile/native3/run.sh | 2 1 + 1 - 0 !
test-suite/coq-makefile/native4/run.sh | 2 1 + 1 - 0 !
test-suite/misc/11170.sh | 2 1 + 1 - 0 !
test-suite/misc/13330.sh | 2 1 + 1 - 0 !
test-suite/misc/7704.sh | 2 1 + 1 - 0 !
test-suite/misc/changelog.sh | 2 1 + 1 - 0 !
test-suite/misc/coq_environment.sh | 2 1 + 1 - 0 !
test-suite/misc/coq_makefile_destination_of.sh | 2 1 + 1 - 0 !
test-suite/misc/coqc_dash_o.sh | 2 1 + 1 - 0 !
test-suite/misc/coqtop_print-mod-uid.sh | 2 1 + 1 - 0 !
test-suite/misc/non-marshalable-state.sh | 2 1 + 1 - 0 !
test-suite/misc/poly-capture-global-univs.sh | 2 1 + 1 - 0 !
test-suite/misc/quotation_token.sh | 2 1 + 1 - 0 !
test-suite/misc/redirect_printing.sh | 2 1 + 1 - 0 !
test-suite/misc/side-eff-leak-univs.sh | 2 1 + 1 - 0 !
test-suite/misc/universes/build_all_stdlib.sh | 2 1 + 1 - 0 !
test-suite/report.sh | 2 1 + 1 - 0 !
test-suite/tools/update-compat/run.sh | 2 1 + 1 - 0 !
tools/make-both-single-timing-files.py | 2 1 + 1 - 0 !
tools/make-both-time-files.py | 2 1 + 1 - 0 !
tools/make-one-time-file.py | 2 1 + 1 - 0 !
101 files changed, 105 insertions(+), 105 deletions(-)

 
 use debian paths everywhere
remove heavy tests.patch | (download)

test-suite/success/Nia.v | 673 0 + 673 - 0 !
test-suite/success/Nsatz.v | 2 2 + 0 - 0 !
2 files changed, 2 insertions(+), 673 deletions(-)

 
 remove heavyweight tests
 Remove tests that use too much RAM or time to run on a buildd. (The MIPS
 buildd is frequently the culprit, as MIPS lacks an OCaml native
 compiler.)
remove tests that need coqlib.patch | (download)

test-suite/coq-makefile/arg/run.sh | 7 0 + 7 - 0 !
test-suite/coq-makefile/coqdoc1/run.sh | 76 0 + 76 - 0 !
test-suite/coq-makefile/coqdoc2/run.sh | 74 0 + 74 - 0 !
test-suite/coq-makefile/emptyprefix/run.sh | 17 0 + 17 - 0 !
test-suite/coq-makefile/extend-subdirs/run.sh | 8 0 + 8 - 0 !
test-suite/coq-makefile/findlib-package/run.sh | 21 0 + 21 - 0 !
test-suite/coq-makefile/latex1/run.sh | 13 0 + 13 - 0 !
test-suite/coq-makefile/merlin1/run.sh | 13 0 + 13 - 0 !
test-suite/coq-makefile/mlpack1/run.sh | 36 0 + 36 - 0 !
test-suite/coq-makefile/mlpack2/run.sh | 36 0 + 36 - 0 !
test-suite/coq-makefile/multiroot/run.sh | 78 0 + 78 - 0 !
test-suite/coq-makefile/only/run.sh | 10 0 + 10 - 0 !
test-suite/coq-makefile/plugin1/run.sh | 39 0 + 39 - 0 !
test-suite/coq-makefile/plugin2/run.sh | 39 0 + 39 - 0 !
test-suite/coq-makefile/plugin3/run.sh | 39 0 + 39 - 0 !
test-suite/coq-makefile/uninstall1/run.sh | 26 0 + 26 - 0 !
test-suite/coq-makefile/uninstall2/run.sh | 26 0 + 26 - 0 !
test-suite/coq-makefile/validate1/run.sh | 8 0 + 8 - 0 !
test-suite/misc/printers.sh | 14 0 + 14 - 0 !
19 files changed, 580 deletions(-)

 
 disable tests which require -coqlib to be set
remove bytecode failing tests.patch | (download)

test-suite/coq-makefile/findlib-package-unpacked/run.sh | 22 0 + 22 - 0 !
1 file changed, 22 deletions(-)

 
 disable tests which require ocamlopt
MIME-Version: 1.0
Content-Type: text/plain; charset="utf-8"
Content-Transfer-Encoding: 8bit
find_timing_scripts.patch | (download)

tools/CoqMakefile.in | 6 3 + 3 - 0 !
tools/make-both-single-timing-files.py | 3 3 + 0 - 0 !
tools/make-both-time-files.py | 2 2 + 0 - 0 !
tools/make-one-time-file.py | 1 1 + 0 - 0 !
4 files changed, 9 insertions(+), 3 deletions(-)

 
 move the timing scripts to a saner location under saner names