From 4154f946e1a50e6a560d9beb8b0f5ede2d8e75b3 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 27 Sep 2023 11:19:45 +0200 Subject: [PATCH] Update README.md --- README.md | 73 ++----------------------------------------------------- 1 file changed, 2 insertions(+), 71 deletions(-) diff --git a/README.md b/README.md index 7db7c8dd8..6bf60cb14 100644 --- a/README.md +++ b/README.md @@ -162,7 +162,8 @@ The documentation of all commands can be found in the comments of find them. All commands can be prefixed with the attribute `#[verbose]` to get an idea of what they are doing. -See also the `#[log]` attribute in the "Plan B" section below. +For debugging purposes, passing the attribute `#[log]` or `#[log(raw)]` +to a HB command prints Coq commands which are equivalent to its effect.

@@ -181,73 +182,3 @@ See also the `#[log]` attribute in the "Plan B" section below. this seamingly mutual dependency using HB.

- -### 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 sure plan B works? We provide tools to check that in your CI, see -the details below. - -
(click to expand)

- - -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` variable set. Eg - -```shell -COQ_ELPI_ATTRIBUTES='hb(log(raw))' make -``` - -The `coq.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 -coq.hb patch file1.v file2.v ... -``` - -The converse operation can be performed using the following command: - -```shell -coq.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 - 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: | - # build the project so that it generates patch files - COQ_ELPI_ATTRIBUTES="hb(log(raw))" make -j2 - # apply the patches - coq.hb patch `find . -name \*.v` - # check something happened - if git diff --quiet; then echo "No patch!"; exit 1; fi - # replace HB by a package with trivial dependencies, just to make - # the From HB Require... line work - opam remove coq-hierarchy-builder - opam install coq-hierarchy-builder-shim - # build the project without HB - make -j2 -``` - -