Ssreflect Users Discussion List

[Yves Bertot <>]

Here is my analysis of the situation.

I believe that compiling the current head of the master branch of math-comp
with coq-8.6 cannot work because the whole content of ssreflect.v has been
removed (under the assumption that the content of this file is now part of
the coq distribution, something that only is true in the current master
development branch of Coq and will be true in the next released version).

The question I asked earlier today was concerned with finding what version
of math-comp is compatible with 8.6 along the master branch.  It is hard
to find this information, but looking at the files in Clement's home 
directory,
it seems that the vo files that in his opam/lib/coq/user-contrib/mathcomp 
directory
are identical to the files that can be found in a compiled version
of math-comp1.6 available somewhere else (funny enough, the source files 
differ,
but maybe only in comments).

I will proceed from there, but it should be noted that the current version
of math-comp on the master file does not compile with coq-8.6, and this
is not documented.

With my best,

Yves

----- Mail original -----
> De: "Enrico Tassi" 
> <>
> À: 
> 
> Envoyé: Mercredi 12 Juillet 2017 14:59:27
> Objet: Re: [ssreflect] Install the master branch of ssreflect with coq-8.6
> 
> On Wed, Jul 12, 2017 at 02:33:47PM +0200, Maxime Dénès wrote:
> > I see. But this is in fact unrelated to the branch renaming. In fact, a
> > fresh install of Coq master now prints 8.7.0~alpha, which is what the
> > grep should be looking for.
> > 
> > Note that after I merge my PR with more precise version numbers, they
> > will start with the 8.7.0~alpha, but will be something like
> > 8.7.0~alpha-nnn-sha1, so the detection script should be robust to that.
> > 
> > --print-version will return similar information AFAIK.
> 
> I agree.
> 
> Going back to Yves' question, he could simply set by hand the
> BRANCH_coq variable to trunk or v8.6 and see if this fixes his
> compilation issues or not.
> 
> Ciao
> --
> Enrico Tassi
>