Bug#815684: why can't be built from source

[Ralf Treinen <treinen@free.fr>]

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.