Stream: Hierarchy Builder devs & users

Topic: glob file of `short` pragma with HB

view this post on Zulip YOSHIHIRO Imai (Jan 19 2024 at 08:22):

Hi, I am developing an extension of coq2html.

I found a problem when using the short pragma in HB that the glob file does not contain that abbreviation.
Is this a problem with HB? Or I also think if it may be a problem with the coqc pragma.

The following code occurs this problem:

From HB Require Import structures.

HB.mixin Record isA (T: Type) := {foo : T}.

#[short(type=typeA)]
HB.structure Definition A := {T of isA T}.

This code generates the glob file by coqc

DIGEST 2f7687aa48253fb06fc30b5adf0c25bc
FHBshort
R23:32 HB.structures <> <> lib
binder 57:57 <> T:1
R76:76 HBshort <> T:1 var
binder 70:72 <> foo:2
mod 36:78 <> isA
sec 36:78 isA isA
var 36:78 isA.isA T
rec 36:78 isA axioms_
proj 36:78 isA foo
R36:78 HBshort isA.isA <> sec
def 36:78 isA phant_Build
def 36:78 isA phant_axioms
def 36:78 isA identity_builder
mod 36:78 <> isA.Exports
R131:131 HB.structures <> ::HB_scope:'{'_x_'of'_x_'&'_'..'_'&'_x_'}' not
R133:136 HB.structures <> ::HB_scope:'{'_x_'of'_x_'&'_'..'_'&'_x_'}' not
R142:142 HB.structures <> ::HB_scope:'{'_x_'of'_x_'&'_'..'_'&'_x_'}' not
binder 132:132 <> T:4
R137:139 HBshort <> isA abbrev
R141:141 HBshort <> T:4 var
mod 81:143 <> A
rec 81:143 A axioms_
proj 81:143 A HBshort_isA_mixin
rec 81:143 A type
proj 81:143 A sort
proj 81:143 A class
def 81:143 A phant_clone
def 81:143 A pack_
mod 81:143 <> A.Exports
def 81:143 A phant_on_
mod 81:143 <> A.EtaAndMixinExports
sec 81:143 A.EtaAndMixinExports hb_instance_1
var 81:143 A.EtaAndMixinExports.hb_instance_1 T
def 81:143 A.EtaAndMixinExports HB_unnamed_factory_2
def 81:143 A.EtaAndMixinExports HBshort_A__to__HBshort_isA
def 81:143 A.EtaAndMixinExports HB_unnamed_mixin_4
def 81:143 A.EtaAndMixinExports structures_eta__canonical__HBshort_A
R81:143 HBshort A.EtaAndMixinExports.hb_instance_1 <> sec
def 81:143 <> foo
mod 81:143 <> ElpiOperations5

I think this glob file should include the typeA abbreviation definition, but it doesn't.

my environment

view this post on Zulip Enrico Tassi (Jan 19 2024 at 08:33):

Looks like a bug in Coq-Elpi, the code of add-abbreviation https://github.com/LPCIC/coq-elpi/blob/75b619727c7ae8e22e79b1a70331afa9c47f8eba/src/coq_elpi_builtins.ml#L2984 should do something like add-constant https://github.com/LPCIC/coq-elpi/blob/75b619727c7ae8e22e79b1a70331afa9c47f8eba/src/coq_elpi_builtins.ml#L1962 w.r.t. glob info.

Last updated: Sep 09 2024 at 06:02 UTC