Package: coq
Version: 8.5-2
Severity: wishlist
Tags: jessie fixed-upstream security
It's great that Debian provides pre-compiled packages for Coq in the
official repositories. Yet currently projects face an unfortunate choice
between depending on an outdated version of Coq and not being able to
build on Debian.
In addition to adding features, Coq 8.5 fixes numerous nasty bugs that
are present in all patch levels of Coq 8.4. For example, 8.4 has a very
hard time with dependent subgoals, and checking an untrusted proof in
Coq 8.4 can result in arbitrary code execution[1]. A backport of the
Coq version in stretch (8.5-2) to stable would thus be very desirable.
I am filing this issue because I believe the backport would be best
maintained by the maintainers of the package itself (the porting itself
should be quite straightforward). Since Coq is moving to a release cycle
faster than Debian's (8 months, IIRC), it is likely that the wish for a
backport of the latest stable release of Coq to the latest stable
release of Debian will occur again.
Thanks,
Andres
[1]: https://coq.inria.fr/bugs/show_bug.cgi?id=4590
