coqutil icon indicating copy to clipboard operation
coqutil copied to clipboard

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

Open JasonGross opened this issue 5 years ago • 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 https://github.com/coq/coq/issues/12066 that coqutil hits because it's using absolute paths.

JasonGross avatar Apr 10 '20 04:04 JasonGross