Ssreflect Users Discussion List

[Yves Bertot <>]

For the record, setting OS to Windows_NT does solve the compilation problem.

Yves

> ----- Mail original -----
> > De: "Enrico Tassi" 
> > <>
> > À: 
> > 
> > Envoyé: Jeudi 13 Juillet 2017 10:14:05
> > Objet: Re: [ssreflect] Install the master branch of ssreflect with coq-8.6
> > 
> > On Thu, Jul 13, 2017 at 09:53:56AM +0200, Yves Bertot wrote:
> > > 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.
> > 
> > OS is there on cygwin (the only platform that was in need of an
> > exception).  Maybe I could use the string printed by `uname` instead.
> > 
> > IIRC -r is useful since such Makefile.coq-makefile can be run by
> > both Makefile and ssreflect/Makefile. If you are compiling the whole math
> > comp you can probably remove the -r.
> > 
> > I'm sorry but without having Darwin's `ln` at hand I'm not sure how to
> > fix the thing.  Maybe if you just `export OS=Windows_NT` it will work...
> > 
> > Ciao
> > --
> > Enrico Tassi
> > 
>