Ssreflect Users Discussion List

[Florent Hivert <>]

On Fri, Dec 18, 2015 at 11:33:58PM +0100, Florent Hivert wrote:
>       Dear all,
> 
> I tried to compile the brand new mathcomp-1.6 and I'm running into
> trouble. The output show a lot of error messages such as
> 
>    mkdir: cannot create directory ‘bkpcoqdep’: File exists
>    mv: cannot stat ‘bkpcoqdep/algebra/interval.v’: No such file or directory
>    find: ‘bkpcoqdep’: No such file or directory
> 
> I attached the output of make. Here is some context informations.  In case 
> you
> care: I'm running a Linux OpenSuSE 12.3 distribution on a 64bit machine. My
> coq is compiled from the source using the standard Ocaml in my distro:
> 
> siteswap-~ $ coqc --version
> The Coq Proof Assistant, version 8.4pl5 (July 2015)
> compiled on Jul 07 2015 23:22:59 with OCaml 4.02.2

siteswap-*th-comp/mathcomp $ coqc --version
The Coq Proof Assistant, version 8.4pl6 (December 2015)
compiled on Dec 19 2015 01:59:26 with OCaml 4.02.3

I realized reading more carefully install.md that coq version 8.4pl6 was
required. So I upgraded my coq. The problem remains.

Florent