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