coq-hierarchy-builder-shim

math-comp · Feb 15, 2021 · b5aea20 · b5aea20
1 parent e410e0b
commit b5aea20
Show file tree

Hide file tree

Showing 55 changed files with 129 additions and 103 deletions.
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -53,8 +53,17 @@ jobs:
           mkdir /home/coq/workspace
           cp -ra . /home/coq/workspace
           cd /home/coq/workspace
-          COQ_ELPI_ATTRIBUTES=log_hb make -j2
-          make patch
-          make -j2
-          make reset
+          opam install ./coq-hierarchy-builder.opam
+          # This is what a user does to cut HB loose
+          COQ_ELPI_ATTRIBUTES=log_hb make test-suite -j2
+          hb patch `find . -name \*.v`
+          make clean
+          opam remove coq-hierarchy-builder.opam
+          opam install ./coq-hierarchy-builder-shim.opam
+          # Does it work?
+          sed -i "s/-Q . HB//" _CoqProject.test-suite
+          make test-suite -j2
+          # We also test the reset facility works (we rebuild hb locally)
+          make hb
+          ./hb reset `find . -name \*.v`
           git diff --exit-code
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
 *.v.hb
 *.v.hb.old
 hb

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,7 @@ COQV:= $(shell echo $(COQVVV) | cut -d"." -f1)
 COQVV:= $(shell echo $(COQVVV) | cut -d"." -f1-2)
 
 # all: ---------------------------------------------------------------
-all: config build
+all: config build test-suite
 
 # Makefile.coq: ------------------------------------------------------
 .PHONY: pre-makefile
@@ -56,12 +56,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 +68,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,33 +121,9 @@ sub-%: __always__
 endif
 
 # Make of individual .vo ---------------------------------------------
-%.vo: __always__ Makefile.coq
+structures.vo : %.vo: __always__ Makefile.coq
 	+$(COQMAKE) $@
-
 hb: __always__ Makefile.coq
 	+$(COQMAKE) $@
-
-reset: hb
-	./hb reset `find . -name \*.v`
-patch: hb
-	./hb patch `find . -name \*.v`
-
-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/
+$(wildcard examples/*/*.v tests/*.v:%.v=%.vo): __always__ Makefile.test-suite.coq
+	+$(COQMAKE_TESTSUITE) $@
diff --git a/_CoqProject b/_CoqProject
@@ -1,56 +1,3 @@
 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
-
--R . HB
+-Q . HB
diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite
@@ -0,0 +1,57 @@
+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
+
+-R tests HB.tests
+-R examples HB.examples
+
+-Q . HB
diff --git a/coq-hierarchy-builder-shim.opam b/coq-hierarchy-builder-shim.opam
@@ -0,0 +1,19 @@
+opam-version: "2.0"
+name: "coq-hierarchy-builder"
+version: "dev"
+maintainer: "Enrico Tassi <enrico.tassi@inria.fr>"
+authors: [ "Cyril Cohen" "Kazuhiko Sakaguchi" "Enrico Tassi" ]
+license: "MIT"
+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 "-C" "shim" ]
+install: [ make "-C" "shim" "install" ]
+conflicts: [ "coq-hierarchy-builder" ]
+synopsis: "Shim package for HB"
+description: """
+This package provide the support constants one can use to compile files
+generated by HB.
+"""
+tags: [ "logpath:HB" ]
diff --git a/coq-hierarchy-builder.opam b/coq-hierarchy-builder.opam
@@ -8,9 +8,12 @@ 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" ]
+build: [ [ make "build"]
+         [ make "test-suite" ]  # {with-test} waiting https://github.com/coq-community/docker-coq-action/pull/48
+       ]
+install: [ make "install" ]
 depends: [ "coq-elpi" {>= "1.9.1" & < "1.10~"} ]
+conflicts: [ "coq-hierarchy-builder-shim" ]
 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
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.

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.

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
diff --git a/readme.v → examples/readme.v b/readme.v → examples/readme.v
diff --git a/shim/Makefile b/shim/Makefile
@@ -0,0 +1 @@
+include ../Makefile.common
diff --git a/shim/_CoqProject b/shim/_CoqProject
@@ -0,0 +1,3 @@
+-R . HB
+
+structures.v
diff --git a/shim/structures.v b/shim/structures.v
@@ -0,0 +1,10 @@
+From Coq Require Import String ssreflect ssrfun.
+Export String.StringSyntax.
+
+Definition unify T1 T2 (t1 : T1) (t2 : T2) (s : option (string * Type)) :=
+  phantom T1 t1 -> phantom T2 t2.
+Definition id_phant {T} {t : T} (x : phantom T t) := x.
+Definition nomsg : option (string * Type) := None.
+Definition is_not_canonically_a : string := "is not canonically a".
+Definition indexed {T} (x : T) := x.
+Definition new {T} (x : T) := x.
diff --git a/structures.v b/structures.v
@@ -1,13 +1,17 @@
+(* Support constants, to be kept in sync with shim/structures.v *)
 From Coq Require Import String ssreflect ssrfun.
-From elpi Require Import elpi.
 Export String.StringSyntax.
 
-(** Technical definition from /Canonical Structures for the working Coq user/ *)
 Definition unify T1 T2 (t1 : T1) (t2 : T2) (s : option (string * Type)) :=
   phantom T1 t1 -> phantom T2 t2.
 Definition id_phant {T} {t : T} (x : phantom T t) := x.
 Definition nomsg : option (string * Type) := None.
 Definition is_not_canonically_a : string := "is not canonically a".
+Definition indexed {T} (x : T) := x.
+Definition new {T} (x : T) := x.
+
+(* ********************* structures ****************************** *)
+From elpi Require Import elpi.
 
 Register unify as hb.unify.
 Register id_phant as hb.id.
@@ -18,10 +22,8 @@ Register Coq.Init.Datatypes.Some as hb.some.
 Register Coq.Init.Datatypes.pair as hb.pair.
 Register Coq.Init.Datatypes.prod as hb.prod.
 Register Coq.Init.Specif.sigT as hb.sigT.
-Definition indexed {T} (x : T) := x.
 Bind Scope type_scope with indexed.
 Register indexed as hb.indexed.
-Definition new {T} (x : T) := x.
 Register new as hb.new.
 
 Declare Scope HB_scope.