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

Bug#951632: marked as done (ITP: coq-menhirlib -- Support library for verified Coq parsers produced by Menhir)

Your message dated Fri, 15 Jul 2022 20:55:15 +0200
with message-id <ae2612f8eb04874d78cb18e0080dc389948455aa.camel@gmail.com>
and subject line Coq-menhirlib is now in Debian
has caused the Debian Bug report #951632,
regarding ITP: coq-menhirlib -- Support library for verified Coq parsers produced by Menhir
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.)


-- 
951632: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=951632
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message --- 
Package: wnpp
Severity: wishlist
Owner: Ralf Treinen <treinen@debian.org>

* Package name    : coq-menhirlib
  Version         : 20200123-1
  Upstream Author : Jacques-Henri Jourdan <jacques-henri.jourdan@lri.fr>
* URL             : http://gallium.inria.fr/~fpottier/menhir/
* License         : LGPL3+
  Programming Lang: Coq
  Description     : Support library for verified Coq parsers produced by Menhir

 The Menhir parser generator, when invoked with the --coq option, produces
 parser code in the Coq language.
 .
 These parsers must be linked against this library, which provides
 both an interpreter (which allows running the generated parser) and
 a validator (which allows verifying, at parser construction time,
 that the generated parser is correct and complete with respect to
 the grammar).

This package will be maintained by ocaml-team.

Rationale: this is currently part of the menhir package. The plan is to
split the menhir source package into two source packages: menhir, and
the new coq-menhirlib, with the objective to drop the build-dependency
on coq from the menhir package. This will resolve two problems:
- having menhir build-depend on coq increases considerably the depth
  of the dependency graph for ocaml-related packages. Removing this 
  build-dependency for menhir itself will make things easier, in particular
  for transitions to new versions of ocaml or coq.
- coq does not build on all architectures, and the situation for building
  coq has become worse starting with 8.11. Menhir however is a parser 
  generator, like bison, and should be available on all architectures.

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

I just found out about your ITP on coq-menhirlib... which I packaged
with another ITP without seeing yours:
  https://tracker.debian.org/pkg/coq-menhirlib
I'm closing this first ITP too.

Sorry to have stepped on your toes,

J.Puydt

--- End Message ---
Reply to: