• You can install HB via OPAM

opam repo add coq-released https://coq.inria.fr/opam/releasedopam install coq-hierarchy-builder

• You can use it in nix with the attributecoqPackages_8_XX.hierarchy-builder e.g.vianix-shell -p coq_8_13 -p coqPackages_8_13.hierarchy-builder

• amixin is a bare bone building block of the hierarchy, it packs operationsand axioms.

• afactory is a package of operations and properties that is elaborated byHB to one or more mixin. A mixin is hence a trivial factory.

• astructure is declared by attaching zero or more factories to a type.

• abuilder is a user provided piece of code capable ofbuilding one or more mixins from a factory.

• aninstance is an example of a structure: it provides all operation andfulfills all axioms.

• HB core commands:

  • HB.mixin declares a mixin,
  • HB.structure declares a structure,
  • HB.factory declares a factory,
  • HB.builders andHB.end declare a set of builders,
  • HB.instance declares a structure instance,
  • HB.declare declares a context with parameters, key and mixins.
  • HB.saturate reconsiders all mixin instances to see if some newly declaredstructure can be inhabited

• HB core tactic-in-term:

  • HB.pack to synthesize a structure instance in the middle of a term.

• HB utility commands:

  • HB.export exports a module and schedules it for re-export
  • HB.reexport exports all modules, instances and constants scheduled forre-export
  • HB.lock locks a definition behind an opaque symbol and an unfoldingequation using Coq module system

• HB queries:

  • HB.about is similar toAbout but prints more info on HB structures, likethe known instances and where they are declared
  • HB.locate is similar toLocate, prints file name and line of any globalconstant synthesized by HB
  • HB.graph prints the structure hierarchy to a dot file
  • HB.howto prints sequences of factories to equip a type with a given structure

• HB debug commands:

  • HB.status dumps the contents of the hierarchy (debug purposes)
  • HB.check is similar toCheck (testing purposes)

The documentation of all commands can be found in the comments ofstructures.v, search forElpi Command and you willfind them. All commands can be prefixed with the attribute#[verbose]to get an idea of what they are doing.

For debugging and teaching purposes, passing the attributes#[log] or#[log(raw)] to a HB command prints Coq commands which arealmost equivalent to its effect. Hence, copy-pasting the displayed commands intoyour source file is not expected to work, and we strongly recommendagainst it.

• demo1 anddemo3 declare and evolve a hierarchy up torings with various clients that are tested not to break when the hierarchyevolves
• demo2 describes the subtle triangular interaction between groups,topological space and uniform spaces. Indeed, 1. all uniform spaces induce atopology, which makes them topological spaces, but 2. all topological groups(groups that are topological spaces such that the addition and opposite arecontinuous) induce a uniformity, which makes them uniform spaces. We solvethis seamingly mutual dependency using HB.