mit-plv/coqutil

There is no validate target, and if there were one, it would fail

JasonGross opened this issue · 0 comments

We can fix the first one with

diff --git a/Makefile b/Makefile
index d87b01a..a84f2b5 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,6 @@
 default_target: all

-.PHONY: clean force all install uninstall
+.PHONY: clean force all install uninstall validate

 # absolute paths so that emacs compile mode knows where to find error
 # use cygpath -m because Coq on Windows cannot handle cygwin paths
@@ -31,3 +31,6 @@ install::

 uninstall::
	$(MAKE) -f Makefile.coq.all uninstall
+
+validate:
+	$(MAKE) -f Makefile.coq.all validate

but the second is a bug in Coq coq/coq#12066 that coqutil hits because it's using absolute paths.