Hi there. Doing some experiment with HB here.

I have a opam installed HB with coq-8.13.2 and `HB.declare`

does not seem to be even parsable. Is this normal?

This is from the wiki "Postulate Factories" (https://github.com/math-comp/hierarchy-builder/wiki/HbDeclareContext).

```
From Coq Require Import ssreflect ssrfun.
From HB Require Import structures.
HB.mixin Record hasA T := { a : T }.
HB.structure Definition A := {T of hasA T}.
HB.mixin Record hasB (p : unit) T of A T := { b : T }.
HB.structure Definition B p := {T of A T & hasB p T}.
HB.mixin Record hasC (p q : unit) T of B p T := { c : T }.
HB.structure Definition C p q := {T of B p T & hasC p q T}.
Section test.
HB.declare Context p q T of hasA T & hasB p T & hasC p q T.
```

gives

```
Toplevel input, characters 15-17:
> HB.declare Context p q T of hasA T & hasB p T & hasC p q T.
> ^^
Error: Syntax error: illegal begin of toplevel:vernac_toplevel.
```

my version of coq and HB:

```
coqtop -v
The Coq Proof Assistant, version 8.13.2 (September 2021)
compiled on Sep 23 2021 23:58:30 with OCaml 4.12.0
courtieu@dell-5750-Matafou:~
$ opam show coq-hierarchy-builder
<><> coq-hierarchy-builder: information on all versions <><><><><><><><><><><><>
name coq-hierarchy-builder
all-installed-versions 1.1.0 [full-coq]
all-versions 0.9.0 0.9.1 0.10.0 1.0.0 1.1.0
<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><><><>
version 1.1.0
repository coq-released
```

I did check the changelog, but we were sloppy and we did not write in which version it was introduced.

We do test it https://github.com/math-comp/hierarchy-builder/blob/235051251801cece66ed5b69726c1f85c1c2eb4a/tests/declare.v so version 1.2.0 surely has it. You should be able to install it on Coq 8.13 as well (it will upgrade coq-elpi, but that should be it).

And you need to run `opam update`

I'm afraid

Thanks for playing with HB, btw!!

Thanks! I will try that.

Last updated: Oct 13 2024 at 01:02 UTC