Skip to content

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

@JasonGross

Description

@JasonGross

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 rocq-prover/rocq#12066 that coqutil hits because it's using absolute paths.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions