There is no validate target, and if there were one, it would fail
JasonGross opened this issue · 0 comments
JasonGross commented
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.