| 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/bench/timelog2html |
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-elpi.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-gappa.sh |
2 1 + 1 - 0 !
dev/ci/ci-geocoq.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/check-owners-pr.sh |
2 1 + 1 - 0 !
dev/tools/check-owners.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/github-check-prs.py |
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/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/run.sh |
2 1 + 1 - 0 !
test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/run.sh |
2 1 + 1 - 0 !
test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/run.sh |
2 1 + 1 - 0 !
test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/run.sh |
2 1 + 1 - 0 !
test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/run.sh |
2 1 + 1 - 0 !
test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/run.sh |
2 1 + 1 - 0 !
test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/run.sh |
2 1 + 1 - 0 !
test-suite/coq-makefile/timing/precomputed-time-tests/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/misc/vio_checking.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 !
117 files changed, 121 insertions(+), 121 deletions(-) |
use debian paths everywhere
|
| testsuite bytecode | (download) |
Makefile.build |
2 1 + 1 - 0 !
1 file changed, 1 insertion(+), 1 deletion(-) |
fix export of byte architecture flag to test-suite.
|
| remove heavy tests.patch | (download) |
test-suite/success/Nia.v |
919 0 + 919 - 0 !
test-suite/success/Nsatz.v |
2 2 + 0 - 0 !
2 files changed, 2 insertions(+), 919 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/quick2vo/run.sh |
12 0 + 12 - 0 !
test-suite/coq-makefile/timing/run.sh |
117 0 + 117 - 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/coq-makefile/vio2vo/run.sh |
13 0 + 13 - 0 !
test-suite/misc/printers.sh |
14 0 + 14 - 0 !
22 files changed, 722 deletions(-) |
disable tests which require -coqlib to be set
|
| remove bytecode failing tests.patch | (download) |
test-suite/Makefile |
2 1 + 1 - 0 !
test-suite/coq-makefile/findlib-package-unpacked/run.sh |
22 0 + 22 - 0 !
2 files changed, 1 insertion(+), 23 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
|
