Ssreflect Users Discussion List

[Enrico Tassi <>]

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