[Iris-Club] Iris on OS X fails to compile

[Robbert Krebbers]

Maybe we should submit a feature report to have support for "make 
uninstall" in coq_makefile, or to have "make install" clean up the old 
installation. This patching up of the Makefile feels a bit fragile.

On 11/16/2016 09:49 PM, Ralf Jung wrote:
> Hi Dan,
>
>> I think that the latest changes to the Makefile break the compilation of Iris on Mac OS X (and possibly on other systems that don’t ship GNU sed?)
>
> Thanks a lot for this report!
> Indeed I used GNU-only extensions in that sed script. The trouble is I
> never worked on a non-GNU system, so I don't usually notice this... and
> I can't test it.
>
> I changed the Makefile to use awk instead. Could you test whether that
> works?
>
> Kind regards,
> Ralf
>
>>
>> Here is an error that I get:
>>
>> $ make
>> coq_makefile  -f _CoqProject | sed 's/$(COQCHK) $(COQCHKFLAGS) $(COQLIBS)/$(COQCHK) $(COQCHKFLAGS) $(subst -Q,-R,$(COQLIBS))/' \
>> 	  | sed '/^install:$/a \\tif [ -d "$(DSTROOT)"$(COQLIBINSTALL)/iris/ ]; then find "$(DSTROOT)"$(COQLIBINSTALL)/iris/ -name "*.vo" -print -delete; fi' > Makefile.coq
>> sed: 1: "/^install:$/a \\tif [ - ...": extra characters after \ at the end of a command
>> make: *** [Makefile.coq] Error 1
>>
>> Unfortunately I don’t know sed or Coq build systems well enough to make a patch, but analysis the changelog I came to the conclusion that this change to the makefile has to do with stale .vo files and `make install`. So I just removed the `sed` part from the make file and I am going to make sure that I do a clean build before doing an `install`.
>> Hth
>>
>> Best,
>> -Dan
>>
>