Merge pull request #162 from math-comp/cleanup2

Cleanup from logging vernac
math-comp · Feb 24, 2021 · bc2b0bc · bc2b0bc
2 parents 148fd16 + 12c214b
commit bc2b0bc
Show file tree

Hide file tree

Showing 51 changed files with 299 additions and 247 deletions.
diff --git a/.gitignore b/.gitignore
@@ -34,6 +34,9 @@ nra.cache
 Makefile.coq
 Makefile.coq.conf
 .coqdeps.d
+Makefile.test-suite.coq
+Makefile.test-suite.coq.conf
+.coqdeps.test-suite
 
 _minted-*
 *.aux

diff --git a/Makefile.common b/Makefile.common
@@ -25,13 +25,13 @@ TGTS?=
 ######################################################################
 
 # local context: -----------------------------------------------------
-.PHONY: all config build only test-suite clean distclean doc doc-clean __always__
+.PHONY: all config build only test-suite clean distclean __always__
 .SUFFIXES:
 
 H:= $(if $(VERBOSE),,@)  # not used yet
 TOP     = $(dir $(lastword $(MAKEFILE_LIST)))
 COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS)
-COQMAKE_TESTSUITE = $(MAKE) -f Makefile.test-suite.coq VDFILE=".coqdeps.test-suite" $(COQMAKEOPTIONS)
+COQMAKE_TESTSUITE = $(MAKE) -f Makefile.test-suite.coq $(COQMAKEOPTIONS)
 BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \
 	      | wc -l | sed 's/ *//g')
 
@@ -46,7 +46,10 @@ COQV:= $(shell echo $(COQVVV) | cut -d"." -f1)
 COQVV:= $(shell echo $(COQVVV) | cut -d"." -f1-2)
 
 # all: ---------------------------------------------------------------
-all: config build
+all: 
+	$(MAKE) config
+	$(MAKE) build
+	$(MAKE) test-suite
 
 # Makefile.coq: ------------------------------------------------------
 .PHONY: pre-makefile
@@ -56,12 +59,8 @@ Makefile.coq: pre-makefile $(COQPROJECT) Makefile
 
 # Test suite ---------------------------------------------------------
 
-test_suite/hierarchy_test.v: build
-	mkdir -p test_suite
-	COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp -lib all.all > test_suite/hierarchy_test.v
-
-Makefile.test-suite.coq: test_suite/hierarchy_test.v
-	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f Make.test-suite -o Makefile.test-suite.coq
+Makefile.test-suite.coq: $(COQPROJECT).test-suite Makefile
+	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT).test-suite -o Makefile.test-suite.coq
 
 # Global config, build, clean and distclean --------------------------
 config: sub-config this-config
@@ -72,7 +71,7 @@ only: sub-only this-only
 
 test-suite: sub-test-suite this-test-suite
 
-clean: sub-clean this-clean doc-clean
+clean: sub-clean this-clean
 
 distclean: sub-distclean this-distclean
 
@@ -125,25 +124,5 @@ sub-%: __always__
 endif
 
 # Make of individual .vo ---------------------------------------------
-%.vo: __always__ Makefile.coq
+structures.vo : %.vo: __always__ Makefile.coq
 	+$(COQMAKE) $@
-
-doc: __always__ Makefile.coq
-	mkdir -p _build_doc/
-	cp -r $(COQFILES) -t _build_doc/ --parents
-	cp Make Makefile* _build_doc
-	mkdir -p _build_doc/htmldoc
-	. ../etc/utils/builddoc_lib.sh; \
-		cd _build_doc && mangle_sources $(COQFILES)
-	+cd _build_doc && $(COQMAKE)
-	cd _build_doc && if [ ! -f .Makefile.coq.d ] ; then cp .coqdeps.d .Makefile.coq.d ; fi #can be removed when coq-8.10 compatibility is dropped
-	cd _build_doc && grep -v vio: .Makefile.coq.d > depend
-	cd _build_doc && cat depend | ../../etc/buildlibgraph $(COQFILES) > htmldoc/depend.js
-	cd _build_doc && $(COQBIN)coqdoc -t "Mathematical Components" \
-		-g --utf8 -R . mathcomp \
-		--parse-comments \
-		--multi-index $(COQFILES) -d htmldoc
-	cp ../etc/artwork/coqdoc.css _build_doc/htmldoc
-
-doc-clean:
-	rm -rf _build_doc/
diff --git a/_CoqProject b/_CoqProject
@@ -1,60 +1,4 @@
 structures.v
 
-readme.v
-
-demo1/hierarchy_0.v
-demo1/hierarchy_1.v
-demo1/hierarchy_2.v
-demo1/hierarchy_3.v
-demo1/hierarchy_4.v
-demo1/hierarchy_5.v
-demo1/test_0_0.v
-demo1/test_1_0.v
-demo1/test_2_0.v
-demo1/test_3_0.v
-demo1/test_3_3.v
-demo1/test_4_0.v
-demo1/test_4_3.v
-demo1/test_5_0.v
-demo1/test_5_3.v
-
-demo2/classical.v
-demo2/stage10.v
-demo2/stage11.v
-
-demo3/hierarchy_0.v
-demo3/hierarchy_1.v
-demo3/hierarchy_2.v
-demo3/test_0_0.v
-demo3/test_1_0.v
-demo3/test_2_0.v
-
-demo4/hierarchy_0.v
-
-demo5/hierarchy_0.v
-
-FSCD2020_material/V1.v
-FSCD2020_material/V2.v
-FSCD2020_material/V3.v
-FSCD2020_material/V4.v
-
-FSCD2020_talk/V1.v
-FSCD2020_talk/V2.v
-FSCD2020_talk/V3.v
-
-Coq2020_material/CoqWS_demo.v
-Coq2020_material/CoqWS_abstract.v
-Coq2020_material/CoqWS_expansion/withHB.v
-Coq2020_material/CoqWS_expansion/withoutHB.v
-
-tests/type_of_exported_ops.v
-tests/duplicate_structure.v
-tests/instance_params_no_type.v
-tests/test_CS_db_filtering.v
-tests/subtype.v
-tests/exports.v
-tests/infer.v
-tests/display.v
-
--R . HB
 -arg -w -arg -elpi.add-const-for-axiom-or-sectionvar
+-Q . HB
diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite
@@ -0,0 +1,60 @@
+examples/readme.v
+
+examples/demo1/hierarchy_0.v
+examples/demo1/hierarchy_1.v
+examples/demo1/hierarchy_2.v
+examples/demo1/hierarchy_3.v
+examples/demo1/hierarchy_4.v
+examples/demo1/hierarchy_5.v
+examples/demo1/test_0_0.v
+examples/demo1/test_1_0.v
+examples/demo1/test_2_0.v
+examples/demo1/test_3_0.v
+examples/demo1/test_3_3.v
+examples/demo1/test_4_0.v
+examples/demo1/test_4_3.v
+examples/demo1/test_5_0.v
+examples/demo1/test_5_3.v
+
+examples/demo2/classical.v
+examples/demo2/stage10.v
+examples/demo2/stage11.v
+
+examples/demo3/hierarchy_0.v
+examples/demo3/hierarchy_1.v
+examples/demo3/hierarchy_2.v
+examples/demo3/test_0_0.v
+examples/demo3/test_1_0.v
+examples/demo3/test_2_0.v
+
+examples/demo4/hierarchy_0.v
+
+examples/demo5/hierarchy_0.v
+
+examples/FSCD2020_material/V1.v
+examples/FSCD2020_material/V2.v
+examples/FSCD2020_material/V3.v
+examples/FSCD2020_material/V4.v
+
+examples/FSCD2020_talk/V1.v
+examples/FSCD2020_talk/V2.v
+examples/FSCD2020_talk/V3.v
+
+examples/Coq2020_material/CoqWS_demo.v
+examples/Coq2020_material/CoqWS_abstract.v
+examples/Coq2020_material/CoqWS_expansion/withHB.v
+examples/Coq2020_material/CoqWS_expansion/withoutHB.v
+
+tests/type_of_exported_ops.v
+tests/duplicate_structure.v
+tests/instance_params_no_type.v
+tests/test_CS_db_filtering.v
+tests/subtype.v
+tests/infer.v
+tests/exports.v
+
+-R tests HB.tests
+-R examples HB.examples
+
+-Q . HB
+-arg -w -arg -elpi.add-const-for-axiom-or-sectionvar
diff --git a/coq-hierarchy-builder.opam b/coq-hierarchy-builder.opam
@@ -8,9 +8,11 @@ homepage: "https://github.com/math-comp/hierarchy-builder"
 bug-reports: "https://github.com/math-comp/hierarchy-builder/issues"
 dev-repo: "git+https://github.com/math-comp/hierarchy-builder"
 
-build: [ make ]
-install: [ make "install" "VFILES=structures.v" ]
 depends: [ "coq-elpi" {>= "1.6" & < "1.9~"} ]
+build: [ [ make "build"]
+         [ make "test-suite" ]  # {with-test} waiting https://github.com/coq-community/docker-coq-action/pull/48
+       ]
+install: [ make "install" ]
 synopsis: "High level commands to declare and evolve a hierarchy based on packed classes"
 description: """
 Hierarchy Builder is a high level language to build hierarchies of algebraic structures and make these

diff --git a/Coq2020_material/CoqWS_abstract.v → examples/Coq2020_material/CoqWS_abstract.v b/Coq2020_material/CoqWS_abstract.v → examples/Coq2020_material/CoqWS_abstract.v
diff --git a/Coq2020_material/CoqWS_demo.v → examples/Coq2020_material/CoqWS_demo.v b/Coq2020_material/CoqWS_demo.v → examples/Coq2020_material/CoqWS_demo.v
diff --git a/Coq2020_material/CoqWS_expansion/withHB.v → ...Coq2020_material/CoqWS_expansion/withHB.v b/Coq2020_material/CoqWS_expansion/withHB.v → ...Coq2020_material/CoqWS_expansion/withHB.v
diff --git a/Coq2020_material/CoqWS_expansion/withoutHB.v → ...2020_material/CoqWS_expansion/withoutHB.v b/Coq2020_material/CoqWS_expansion/withoutHB.v → ...2020_material/CoqWS_expansion/withoutHB.v
diff --git a/Coq2020_material/diagram.pdf → examples/Coq2020_material/diagram.pdf b/Coq2020_material/diagram.pdf → examples/Coq2020_material/diagram.pdf
diff --git a/Coq2020_material/diagram.svg → examples/Coq2020_material/diagram.svg b/Coq2020_material/diagram.svg → examples/Coq2020_material/diagram.svg
diff --git a/FSCD2020_material/V1.v → examples/FSCD2020_material/V1.v b/FSCD2020_material/V1.v → examples/FSCD2020_material/V1.v
diff --git a/FSCD2020_material/V2.v → examples/FSCD2020_material/V2.v b/FSCD2020_material/V2.v → examples/FSCD2020_material/V2.v
diff --git a/FSCD2020_material/V3.v → examples/FSCD2020_material/V3.v b/FSCD2020_material/V3.v → examples/FSCD2020_material/V3.v
diff --git a/FSCD2020_material/V4.v → examples/FSCD2020_material/V4.v b/FSCD2020_material/V4.v → examples/FSCD2020_material/V4.v
diff --git a/FSCD2020_talk/V1.v → examples/FSCD2020_talk/V1.v b/FSCD2020_talk/V1.v → examples/FSCD2020_talk/V1.v
diff --git a/FSCD2020_talk/V2.v → examples/FSCD2020_talk/V2.v b/FSCD2020_talk/V2.v → examples/FSCD2020_talk/V2.v
@@ -18,6 +18,6 @@ HB.structure Definition Monoid :=
   { M & monoid_of_semigroup M }.
 
 (* is_monoid does not exist anymore *)
-Fail HB.instance Definition Z_is_monoid : is_monoid Z :=
-  is_monoid.Build Z 0%Z Z.add
-    Z.add_assoc Z.add_0_l Z.add_0_r.
+Fail Check is_monoid.
+
+Fail HB.mixin Record xxxx P A := { F : bool }.
diff --git a/FSCD2020_talk/V3.v → examples/FSCD2020_talk/V3.v b/FSCD2020_talk/V3.v → examples/FSCD2020_talk/V3.v
diff --git a/demo1/README.md → examples/demo1/README.md b/demo1/README.md → examples/demo1/README.md
diff --git a/demo1/hierarchy_0.v → examples/demo1/hierarchy_0.v b/demo1/hierarchy_0.v → examples/demo1/hierarchy_0.v
diff --git a/demo1/hierarchy_1.v → examples/demo1/hierarchy_1.v b/demo1/hierarchy_1.v → examples/demo1/hierarchy_1.v
diff --git a/demo1/hierarchy_2.v → examples/demo1/hierarchy_2.v b/demo1/hierarchy_2.v → examples/demo1/hierarchy_2.v
diff --git a/demo1/hierarchy_3.v → examples/demo1/hierarchy_3.v b/demo1/hierarchy_3.v → examples/demo1/hierarchy_3.v
diff --git a/demo1/hierarchy_4.v → examples/demo1/hierarchy_4.v b/demo1/hierarchy_4.v → examples/demo1/hierarchy_4.v
diff --git a/demo1/hierarchy_5.v → examples/demo1/hierarchy_5.v b/demo1/hierarchy_5.v → examples/demo1/hierarchy_5.v
diff --git a/demo1/test_0_0.v → examples/demo1/test_0_0.v b/demo1/test_0_0.v → examples/demo1/test_0_0.v
diff --git a/demo1/test_1_0.v → examples/demo1/test_1_0.v b/demo1/test_1_0.v → examples/demo1/test_1_0.v
diff --git a/demo1/test_2_0.v → examples/demo1/test_2_0.v b/demo1/test_2_0.v → examples/demo1/test_2_0.v
diff --git a/demo1/test_3_0.v → examples/demo1/test_3_0.v b/demo1/test_3_0.v → examples/demo1/test_3_0.v
diff --git a/demo1/test_3_3.v → examples/demo1/test_3_3.v b/demo1/test_3_3.v → examples/demo1/test_3_3.v
diff --git a/demo1/test_4_0.v → examples/demo1/test_4_0.v b/demo1/test_4_0.v → examples/demo1/test_4_0.v
diff --git a/demo1/test_4_3.v → examples/demo1/test_4_3.v b/demo1/test_4_3.v → examples/demo1/test_4_3.v
diff --git a/demo1/test_5_0.v → examples/demo1/test_5_0.v b/demo1/test_5_0.v → examples/demo1/test_5_0.v
diff --git a/demo1/test_5_3.v → examples/demo1/test_5_3.v b/demo1/test_5_3.v → examples/demo1/test_5_3.v
diff --git a/demo1/user_0.v → examples/demo1/user_0.v b/demo1/user_0.v → examples/demo1/user_0.v
diff --git a/demo1/user_3.v → examples/demo1/user_3.v b/demo1/user_3.v → examples/demo1/user_3.v
diff --git a/demo2/classical.v → examples/demo2/classical.v b/demo2/classical.v → examples/demo2/classical.v
diff --git a/demo2/stage10.v → examples/demo2/stage10.v b/demo2/stage10.v → examples/demo2/stage10.v
@@ -1,6 +1,6 @@
 From Coq Require Import ssreflect ssrfun ssrbool ZArith QArith.
 From HB Require Import structures.
-From HB.demo2 Require Import classical.
+From HB Require Import demo2.classical.
 
 Declare Scope hb_scope.
 Delimit Scope hb_scope with G.
@@ -10,8 +10,6 @@ Local Open Scope hb_scope.
 
 Module Stage10.
 
-HB.structure Definition TYPE := { A of True }.
-
 HB.mixin Record AddAG_of_TYPE A := {
   zero : A;
   add : A -> A -> A;

diff --git a/demo2/stage11.v → examples/demo2/stage11.v b/demo2/stage11.v → examples/demo2/stage11.v
@@ -1,6 +1,6 @@
 From Coq Require Import ssreflect ssrfun ssrbool ZArith QArith.
 From HB Require Import structures.
-From HB.demo2 Require Import classical.
+From HB Require Import demo2.classical.
 
 Declare Scope hb_scope.
 Delimit Scope hb_scope with G.
@@ -10,8 +10,6 @@ Local Open Scope hb_scope.
 
 Module Stage11.
 
-HB.structure Definition TYPE := { A of True }.
-
 HB.mixin Record AddAG_of_TYPE A := {
   zero : A;
   add : A -> A -> A;

diff --git a/demo3/hierarchy_0.v → examples/demo3/hierarchy_0.v b/demo3/hierarchy_0.v → examples/demo3/hierarchy_0.v
diff --git a/demo3/hierarchy_1.v → examples/demo3/hierarchy_1.v b/demo3/hierarchy_1.v → examples/demo3/hierarchy_1.v
diff --git a/demo3/hierarchy_2.v → examples/demo3/hierarchy_2.v b/demo3/hierarchy_2.v → examples/demo3/hierarchy_2.v
diff --git a/demo3/test_0_0.v → examples/demo3/test_0_0.v b/demo3/test_0_0.v → examples/demo3/test_0_0.v
diff --git a/demo3/test_1_0.v → examples/demo3/test_1_0.v b/demo3/test_1_0.v → examples/demo3/test_1_0.v
diff --git a/demo3/test_2_0.v → examples/demo3/test_2_0.v b/demo3/test_2_0.v → examples/demo3/test_2_0.v
diff --git a/demo3/user_0.v → examples/demo3/user_0.v b/demo3/user_0.v → examples/demo3/user_0.v
diff --git a/demo4/hierarchy_0.v → examples/demo4/hierarchy_0.v b/demo4/hierarchy_0.v → examples/demo4/hierarchy_0.v
diff --git a/demo5/hierarchy_0.v → examples/demo5/hierarchy_0.v b/demo5/hierarchy_0.v → examples/demo5/hierarchy_0.v
@@ -1,8 +1,6 @@
 From Coq Require Import ssreflect ssrfun.
 From HB Require Import structures.
 
-HB.structure Definition TYPE := { A of True }.
-
 HB.mixin Record AddComoid_of_TYPE A := {
   zero : A;
   add : A -> A -> A;

diff --git a/readme.v → examples/readme.v b/readme.v → examples/readme.v