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

Ralf Jung jung at mpi-sws.org
Wed Nov 16 21:49:03 CET 2016

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

Kind regards,

> 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

More information about the Iris-Club mailing list