logging: ability to print vernacular commands

Attributes #[log] and #[elpi.log_hb] to get the text in the console or
the disk.

Utility hb to patch/reset files (replacing calls to HB by their
equivalent).

.github/workflows/main.yml

@@ -29,8 +29,6 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - '8.11'
-          - '8.12'
           - '8.13'
         ocaml_version:
           - 'minimal'
@@ -41,3 +39,22 @@ jobs:
         opam_file: './coq-hierarchy-builder.opam'
         coq_version: ${{ matrix.coq_version }}
         ocaml_version: ${{ matrix.ocaml_version }}
+
+  hb-plan-B:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v2
+    - uses: coq-community/docker-coq-action@v1
+      with:
+        opam_file: './coq-hierarchy-builder.opam'
+        coq_version: '8.13'
+        ocaml_version: 'minimal'
+        script: |
+          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
+          git diff --exit-code

.gitignore

@@ -34,6 +34,9 @@ nra.cache
 Makefile.coq
 Makefile.coq.conf
 .coqdeps.d
+*.v.hb
+*.v.hb.old
+hb
 
 _minted-*
 *.aux

Makefile.common

@@ -128,6 +128,14 @@ endif
 %.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

Makefile.coq.local

@@ -14,3 +14,19 @@ structures.vo : hb.elpi
 #  $(foreach M,$(shell seq 0 10),\
 #   $(foreach K,$(shell seq 0 10),\
 #     $(eval $(call MKRULE,$(N),$(M),$(K))))))
+
+pre-all:: hb
+
+hb: hb.ml
+	$(SHOW)'OCAMLC hb.ml -o hb'
+	$(HIDE) ocamlc unix.cma str.cma hb.ml -o hb
+
+install-extra::
+	$(SHOW)'install hb $(dir $(shell which $(COQBIN)coqc))'
+	$(HIDE) install -m 0755 hb $(dir $(shell which $(COQBIN)coqc))
+
+clean::
+	$(SHOW)'CLEAN *.hb *.hb.old ./hb'
+	$(HIDE) find . -name \*.hb -delete
+	$(HIDE) find . -name \*.hb.old -delete
+	$(HIDE) rm -f hb

README.md

@@ -143,3 +143,67 @@ prefixed with the attribute `#[verbose]` to get an idea of what they are doing.
   this seamingly mutual dependency using HB.
 
 </p></details>
+
+#### Plan B
+
+Scared of making your project depend on HB? This section is for you.
+
+HB is based on a thick layer of software which we plan to maintain, but we
+also understand it can look scary. Hence this insurance plan. By passing
+the attribute `#[log]` each command prints Coq commands which are equivalent to
+its effect. By replacing each HB command by its equivalent Coq commands, you
+can eliminate the dependency on HB from your project.
+
+This is a "plan B", by looking at the output of`#[log]` you will realize that
+HB commands are much nicer (and shorter) than the equivalent Coq code. The
+point of a "plan B" is to avoid nightmares, not to be nicer than plan A ;-)
+
+How can you be ensure plan B works? We provide tools to check that, see
+the details below.
+
+<details><summary>(click to expand)</summary><p>
+
+
+Hierarchy Builder commands can log their equivalent vernacular commands
+to "patch" file (extension `.hb`). In order to do so, one has to
+compile the project with the `COQ_ELPI_ATTRIBUTES=log_hb` variable set. Eg
+
+```shell
+COQ_ELPI_ATTRIBUTES=log_hb make
+```
+
+The `hb` command line utility, provided by the `coq-hierarchy-builder` package,
+is able to apply the generated patches: it comments out HB commands and
+inserts their equivalent Coq commands.
+
+```shell
+hb apply file1.v file2.v ...
+```
+
+The converse operation can be performed using the following command:
+
+```shell
+hb reset file1.v file2.v ...
+```
+
+We recommend to setup a CI job testing plan B. If you are using
+`docker-coq-action` the following snippet is a good start:
+
+```yaml
+  hb-plan-B:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v2
+    - uses: coq-community/docker-coq-action@v1
+      with:
+        opam_file: './your-project.opam'        # depends on coq-hierarchy-builder
+        script: |
+          COQ_ELPI_ATTRIBUTES=log_hb make -j2
+          hb patch `find . -name \*.v`
+          rm -rf `coqc -where`/user-constribs/HB
+          make -j2
+          hb reset `find . -name \*.v`
+          git diff --exit-code
+```
+
+</p></details>

coq-hierarchy-builder.opam

@@ -10,7 +10,7 @@ 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~"} ]
+depends: [ "coq-elpi" {>= "1.6" & < "1.10~"} ]
 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

demo2/stage10.v

@@ -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;

demo2/stage11.v

@@ -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;

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;