On Tue, Feb 23, 2016 at 06:34:42PM +0100, Matthias Klose wrote: > Package: src:why > Version: 2.24-3 > Severity: serious > > Tags: sid > > [Mehdi asked me to file RC issues ... I saw these while working on some > transitions in Ubuntu, and trying to keep creduce in unstable/testing] > > why doesn't work with the coq in unstable, and coq-float doesn't work with > the coq in unstable. Saw that coq-float is optional, tried to build it: > > coqc -R lib/coq Why lib/coq/WhyInt.v > coqc -R lib/coq Why lib/coq/WhyArrays.v > coqc -R lib/coq Why lib/coq/WhyBool.v > coqc -R lib/coq Why lib/coq/WhyTuples.v > File "./lib/coq/WhyTuples.v", line 26, characters 23-26: > Error: Cannot infer the implicit parameter A of fst whose type is "Type". > Makefile:974: recipe for target 'lib/coq/WhyTuples.vo' failed > make[1]: *** [lib/coq/WhyTuples.vo] Error 1 > > Then I just removed the libwhy-coq package so that why builds again. For > that I had to disable the testsuite, relying on coq.
Thanks. In fact, the build-dependency of why is already not satisfiable in sid, since coq-float is not installable with the current coq. For the moment I prefer to block on libfloat-coq, and get rid of this dependency only when this cannot be solved otherwise. -Ralf.