mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps
MIT License
42 stars 24 forks source link

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

Open JasonGross opened 4 years ago

JasonGross commented 4 years ago

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.