[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Bug#827861: marked as done (Please add coq-8.5 to jessie-backports)

Your message dated Sun, 20 Feb 2022 19:48:33 +0100
with message-id <87d6132e2091e10d2a37b249c3821742d8168a06.camel@gmail.com>
and subject line wontfix => done
has caused the Debian Bug report #827861,
regarding Please add coq-8.5 to jessie-backports
to be marked as done.

This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.

(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact owner@bugs.debian.org
immediately.)


-- 
827861: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=827861
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message --- 
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

--- End Message ---
--- Begin Message --- 
Hi,

this bug report no longer needs to be there, as it's pretty much
obsolete.

Cheers,

J.Puydt

--- End Message ---
Reply to: