Package: coq / 8.9.1-1

Metadata

Package Version Patches format
coq 8.9.1-1 3.0 (quilt)

Patch series

view the series file
Patch File delta Description
remove heavy tests.patch | (download)

test-suite/bugs/closed/5127.v | 15 0 + 15 - 0 !
test-suite/success/Nsatz.v | 2 2 + 0 - 0 !
2 files changed, 2 insertions(+), 15 deletions(-)

 remove heavyweight tests

remove time sensitive tests.patch | (download)

test-suite/bugs/closed/3441.v | 23 0 + 23 - 0 !
test-suite/bugs/closed/4366.v | 15 0 + 15 - 0 !
test-suite/bugs/closed/4429.v | 31 0 + 31 - 0 !
test-suite/bugs/closed/4811.v | 1685 0 + 1685 - 0 !
4 files changed, 1754 deletions(-)

 remove time-sensitive tests

remove tests that need coqlib.patch | (download)

test-suite/coq-makefile/arg/run.sh | 7 0 + 7 - 0 !
test-suite/coq-makefile/compat-subdirs/run.sh | 8 0 + 8 - 0 !
test-suite/coq-makefile/coqdoc1/run.sh | 59 0 + 59 - 0 !
test-suite/coq-makefile/coqdoc2/run.sh | 57 0 + 57 - 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 | 19 0 + 19 - 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 | 23 0 + 23 - 0 !
test-suite/coq-makefile/mlpack2/run.sh | 23 0 + 23 - 0 !
test-suite/coq-makefile/multiroot/run.sh | 61 0 + 61 - 0 !
test-suite/coq-makefile/only/run.sh | 10 0 + 10 - 0 !
test-suite/coq-makefile/plugin1/run.sh | 26 0 + 26 - 0 !
test-suite/coq-makefile/plugin2/run.sh | 26 0 + 26 - 0 !
test-suite/coq-makefile/plugin3/run.sh | 26 0 + 26 - 0 !
test-suite/coq-makefile/quick2vo/run.sh | 12 0 + 12 - 0 !
test-suite/coq-makefile/timing/run.sh | 105 0 + 105 - 0 !
test-suite/coq-makefile/uninstall1/run.sh | 23 0 + 23 - 0 !
test-suite/coq-makefile/uninstall2/run.sh | 23 0 + 23 - 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 | 2 0 + 2 - 0 !
23 files changed, 582 deletions(-)

 disable tests which require -coqlib to be set

avoid usr bin env.patch | (download)

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 !
3 files changed, 3 insertions(+), 3 deletions(-)

 avoid invoking /usr/bin/env

python scripts libraries.patch | (download)

tools/CoqMakefile.in | 6 3 + 3 - 0 !
1 file changed, 3 insertions(+), 3 deletions(-)

 differentiate between python scripts and libraries

skip dot pc.patch | (download)

Makefile | 1 1 + 0 - 0 !
1 file changed, 1 insertion(+)

 ignore .pc directory when building

verbose build.patch | (download)

Makefile.build | 2 1 + 1 - 0 !
1 file changed, 1 insertion(+), 1 deletion(-)

 run tests verbosely

remove bytecode failing tests.patch | (download)

test-suite/Makefile | 2 1 + 1 - 0 !
1 file changed, 1 insertion(+), 1 deletion(-)

 disable tests which require ocamlopt
MIME-Version: 1.0
Content-Type: text/plain; charset="utf-8"
Content-Transfer-Encoding: 8bit

ssrmatching license.patch | (download)

plugins/ssrmatching/g_ssrmatching.mli | 26 26 + 0 - 0 !
1 file changed, 26 insertions(+)

 replace deleted non-free ssrmatching file with free one

0012 ocaml 4.08 does not allow dynamic loading of already.patch | (download)

Makefile.build | 2 1 + 1 - 0 !
1 file changed, 1 insertion(+), 1 deletion(-)

 ocaml 4.08 does not allow dynamic loading of already present
 pr_dump.cmo

0013 Remove test failing with OCaml 4.08.0.patch | (download)

test-suite/bugs/opened/3395.v | 231 0 + 231 - 0 !
1 file changed, 231 deletions(-)

 remove test failing with ocaml 4.08.0