Re: Status of aac-tactics (and migration of coq)
Hi Stephane,
On Wed, Sep 23, 2020 at 09:48:44AM +0200, Stéphane Glondu wrote:
> Dear Ralf,
>
> I saw coq won't migrate to testing because of aac-tactics and coq-float.
>
> I gbp-pulled aac-tactics and saw that you imported a new upstream
> release (8.12.0) in upstream and pristine-tar branches, but master is
> still at 8.11.0-1. Are you planning to continue updating aac-tactics?
yes, but unfortunately that version doesn't compile either with coq 8.12.
The problem is the same with coq-float. The problem seems to be in the
debian packaging of coq, it seems that lac is not found when using the
debian package of coq 8.12. I haven't had time yet to investigate,
sorry. It may be the case that the coq makefile is broken and that
one has to compile and install coq using dune, this is what all the
young guys are using these days.
-Ralf.
--
Ralf Treinen
Institut de Recherche en Informatique Fondamentale
Pôle Preuves, Programmes et Systèmes
Université de Paris
http://www.irif.fr/~treinen/
Reply to: