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

Dan Frumin dfrumin at cs.ru.nl
Wed Nov 16 21:07:35 CET 2016


Hi all,

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?)

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