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

Ralf Jung jung at mpi-sws.org
Thu Nov 17 09:54:32 CET 2016


On 17.11.2016 08:48, Robbert Krebbers wrote:
> 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.

Yeah, we should do that.
Notice that coq_makefile *does* have a "make uninstall", but (a) it is
not called automatically on installation (well, we can argue about
whether that's desirable), (b) it works by generating a shell script
"uninstall_me" and calling it (WTF?), and (c) it only deletes the .vo
files that "make install" would install.  Also, last time I tried the
one generated by Coq 8.5, the uninstall script did not actually work.

Kind regards,

More information about the Iris-Club mailing list