Stream: Hierarchy Builder devs & users

Topic: HB.declare does not work

view this post on Zulip Pierre Courtieu (Oct 22 2021 at 07:25):

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

view this post on Zulip Enrico Tassi (Oct 22 2021 at 11:37):

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).

view this post on Zulip Enrico Tassi (Oct 22 2021 at 11:38):

And you need to run opam update I'm afraid

view this post on Zulip Enrico Tassi (Oct 22 2021 at 11:39):

Thanks for playing with HB, btw!!

view this post on Zulip Pierre Courtieu (Oct 22 2021 at 16:03):

Thanks! I will try that.

Last updated: Apr 20 2024 at 00:02 UTC