Ssreflect Users Discussion List

[Yves Bertot <>]

After "make clean && make", I came by more information about the compilation 
failure:

The trace of re-compilation actually starts with:


option -r does not exist on my version of macos X.  I would like to patch the
file .../ssreflect/Makefile.coq-makefile to set the variable LN to "-sf" 
instead
of 

ln: illegal option -- r
usage: ln [-Ffhinsv] source_file [target_file]
       ln [-Ffhinsv] source_file ... target_dir
       link source_file target_file


So option -r does not exist for ln on my operating system.  I understand that 
the fix should
be a correction in file .../ssreflect/Makefile.coq-makefile, but I do not 
know what should
be the correction, because I do not know where the OS variable comes from, 
whether it is 
set on macos, and what is its value.  I tried to have it printed but the 
value is naught.

With my best,

Yves

----- Mail original -----
> De: "Enrico Tassi" 
> <>
> À: 
> 
> Envoyé: Mercredi 12 Juillet 2017 21:27:16
> Objet: Re: [ssreflect] Install the master branch of ssreflect with coq-8.6
> 
> On Wed, Jul 12, 2017 at 06:08:15PM +0200, Yves Bertot wrote:
> > 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 way the build system works is that, once the coq version has been
> detected, all missing piece of data are put in place.  In
> ssreflect/plugin/$VERSION/ you can find what is missing in
> Coq $VERSION in order to compile the thing.  e.g. .../trunk/ is empty,
> .../8.6/ contains the ssreflect.ml4 + the few .v that were merged in,
> .../8.5/ contains ssreflect.ml4, ssrmatching.ml4, and the .v files.
> 
> The Makefile in ssreflect/Makefile.coq-makefile is in charge of putting
> back what is missing.  So detecting the right version of Coq is crucial.
> 
> Note that the makefile uses $COQBIN/coqtop to find out which version of
> coq you are using (if COQBIN is set) or the coqtop in the PATH.
> 
> Hope it helps.
> 
> Ciao
> --
> Enrico Tassi
>