[Iris-Club] Iris on OS X fails to compile
Ralf Jung
jung at mpi-sws.org
Thu Nov 17 09:54:32 CET 2016
Hi,
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,
Ralf
More information about the Iris-Club
mailing list