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/
