Ssreflect Users Discussion List

[Maxime Dénès <>]

It could be worth adding some continuous testing of math comp, on all
supported architectures.

Maxime.

On 07/13/2017 10:14 AM, Enrico Tassi wrote:
> 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
>