[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
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
>
More information about the Iris-Club
mailing list