Merge pull request #319 from LPCIC/fast-eqb

Fast generation of Sound Equality Tests

Author: gares

Changelog.md

@@ -2,16 +2,23 @@
 
 ## UNRELEASED
 
-- API:
-  - Change `coq.env.module` and `coq.env.module-type` do not fail if the
-    module (type) contains a mutual inductive. The resulting `gref` is going
-    to me unusable with most APIs, though.
-  - Change `coq.env.module` returns a ADT describing the module contents
-  - Change `coq.gref->path` and `coq.gref->id` do work on `gref` which point
-    to mutual inductives.
-  - New `coq.env.term-dependencies` computing all the `grefs` occurring in a term.
-  - New `coq.redflag` and `coq.redflags` types for `@redflags!` option understood
-    by `coq.reduction.lazy.*` `and coq.reduction.cbv.norm`
+### API
+- Change `coq.env.module` and `coq.env.module-type` do not fail if the
+  module (type) contains a mutual inductive. The resulting `gref` is going
+  to me unusable with most APIs, though.
+- Change `coq.env.module` returns a ADT describing the module contents
+- Change `coq.gref->path` and `coq.gref->id` do work on `gref` which point
+  to mutual inductives.
+- New `coq.env.term-dependencies` computing all the `grefs` occurring in a term.
+- New `coq.redflag` and `coq.redflags` types for `@redflags!` option understood
+  by `coq.reduction.lazy.*` `and coq.reduction.cbv.norm`
+- New `coq.env.fresh-global-id`
+
+### APPS
+- Change `derive` usage.
+  One should now import `From elpi.apps Require Import derive.std`
+- Change derivations `eq` and `eqOK` move to `derive.legacy`
+- New derivations `eqb` and `eqbOK` subsuming the previous ones
 
 ## [1.15.6] - 27-08-2022
 

apps/derive/Makefile

@@ -17,6 +17,9 @@ build: Makefile.coq
 test: Makefile.test.coq
 	@$(MAKE) --no-print-directory -f Makefile.test.coq
 
+coverage:
+	@$(MAKE) --no-print-directory -f Makefile.coq coverage
+
 theories/%.vo: force
 	@$(MAKE) --no-print-directory -f Makefile.coq $@
 tests/%.vo: force build Makefile.test.coq

apps/derive/Makefile.coq.local

@@ -1,11 +1,25 @@
 
 coverage:
+	@printf "====== %-10s\n" "test suite"
+	@printf "inductives: %d\n" \
+		`grep -E "^ *(Inductive|Variant)" tests/test_derive_stdlib.v 2>/dev/null| wc -l`
+	@printf "records: %d\n" \
+		`grep -E "^ *(Record|Structure)" tests/test_derive_stdlib.v 2>/dev/null| wc -l`
+	@printf "definitions: %d\n" \
+		`grep -E "^ *(Fixpoint|Definition)" tests/test_derive_stdlib.v 2>/dev/null| wc -l`
 	@for F in $(wildcard theories/derive/*.v); do\
 		D=`basename $$F .v`;\
-		T="tests/test_$${D}.v";\
-		N=`grep -E "^(Fail )?Elpi derive.$$D" $$T 2>/dev/null| wc -l`;\
-		OK=`grep -E "^Elpi derive.$$D" $$T 2>/dev/null| wc -l`;\
-		printf "====== %-10s (%2d/%-2d)\n" $$D $$OK $$N;\
-		grep -E "^Fail Elpi derive.$$D" $$T 2>/dev/null;\
+		D_=`echo $$D | sed 's/_/./'`;\
+		F=`mktemp`;\
+		if [ -e tests/test_$${D}.v ]; then\
+		  (cat tests/test_$${D}.v | awk ' /Module Coverage/ { p = 1 } /End Coverage/ { p = 0 } { if(p == 1) { print }} ' ) > $$F ;\
+		  N=`grep -E "^(Fail )?Elpi derive.$$D_" $$F 2>/dev/null| wc -l`;\
+		  OK=`grep -E "^Elpi derive.$$D_" $$F 2>/dev/null| wc -l`;\
+		  printf "====== %-10s (%2d/%-2d)\n" tests/test_$${D}.v $$OK $$N;\
+		  grep -E "^Fail Elpi derive.$$D_" $$F | grep -vi expected 2>/dev/null;\
+		fi;\
 	done || true
 
+install-extra::
+	df="`$(COQMKFILE) -destination-of theories/derive/std.vo $(COQLIBS)`";\
+	install -m 0644 $(wildcard elpi/*.elpi) "$(COQLIBINSTALL)/$$df"