Laurent Théry (Apr 02 2021 at 14:18): Laurent Théry (Apr 02 2021 at 14:18):Where can I find a list of the commands I could you use to debug when I have a problem. Something that helps me inspecting the Mixins, the Canonical Structures, Coercions and so on, would be great.
Cyril Cohen (Apr 02 2021 at 14:30):You can use the attribute:
#[log] to see the equivalent in Coq commands#[verbose] to see the steps that we highlighted for each HB command Enrico Tassi (Apr 02 2021 at 14:47):Also HB.status and HB.graph
Reynald Affeldt (Apr 03 2021 at 09:53):what would you advise to debug a Error: unable to graft this clause: no clause named compress:begin? (this is for a HB.instance Definintion that used to work with the PR #179 but not anymore with hb 1.1.0 anymore)
Enrico Tassi (Apr 03 2021 at 10:10):You need to Require Import HB before other files using it
Enrico Tassi (Apr 03 2021 at 10:11):The error is a bit too low level, but I need to hack elpi in order to let coq-elpi catch this (in a proper way) and complain a nicer way
Enrico Tassi (Apr 03 2021 at 10:11):So it won't happen soon ;-)
Reynald Affeldt (Apr 03 2021 at 11:36):Indeed, that was it! Thank you!
Cyril Cohen (Apr 05 2021 at 10:26):@Enrico Tassi for the time being I think the is no better solutiom than creating a faq so that this kind of failure can be listed and indexed by search engines
Enrico Tassi (Apr 05 2021 at 10:46):https://github.com/math-comp/hierarchy-builder/wiki/FAQ
Reynald Affeldt (Apr 08 2021 at 10:46):What does that kind of error message witness? A design flaw in the hierarchy?
Error:
You must declare the current class indt «axioms_» before
indt «Blah.axioms_»
pred assert-building-bottom-up i:class, i:classname.
assert-building-bottom-up CurrentClass C3n :-
class-def (class C3n X Y),
CurrentClass = class CC _ _,
if (not (sub-class? CurrentClass (class C3n X Y)))
(coq.error "You must declare the current class" CC "before" C3n)
true.
the message is perfectible, but it seems the order in which you are declaring your structures is not bottom up
Enrico Tassi (Apr 08 2021 at 10:53):IMO you did the join before doing one of the two siblings
Enrico Tassi (Apr 08 2021 at 10:55):https://github.com/math-comp/hierarchy-builder/pull/214
Enrico Tassi (Apr 08 2021 at 11:45):Hum, my analisys was wrong, if you build in a non bottom up way you get a message like this one
HB: the first structure declared in this hierarchy containing
AddAG_of_AddComoid is Ring which also contains
[AddComoid_of_TYPE, SemiRing_of_AddComoid] .
The are two ways to fix this problem:
1) change the current structure to contain
[AddComoid_of_TYPE, SemiRing_of_AddComoid] as well;
2) amend the hierarchy by declaring a structure before Ring
which contains at most [AddAG_of_AddComoid, AddComoid_of_TYPE]
How can I reproduce your exact issue?
Reynald Affeldt (Apr 08 2021 at 13:18):
Enrico Tassi (Apr 08 2021 at 13:18):@Cyril Cohen
Reynald Affeldt (Apr 08 2021 at 13:18):It's about exceptStateRun and nondetState
Reynald Affeldt (Apr 08 2021 at 13:22):https://github.com/affeldt-aist/monae/blob/monae_hb/hierarchy.v
Reynald Affeldt (Apr 12 2021 at 09:50):
Reynald Affeldt (Apr 12 2021 at 09:50):it might boil down to that (so that an intermediate mixin might do it)
Enrico Tassi (Apr 12 2021 at 10:32):can you sum up your discovery?
Reynald Affeldt (Apr 13 2021 at 00:13):my discovery is likely to be my mistake ^_^ the above pattern corresponds to the following script:
From HB Require Import structures.
HB.mixin Record isTop M := { }.
HB.structure Definition Top := {M of isTop M}.
HB.mixin Record isA1 M of Top M := { }.
HB.structure Definition A1 := {M of isA1 M & isTop M}.
HB.mixin Record isA2 M of Top M := { }.
HB.structure Definition A2 := {M of isA2 M & isTop M}.
HB.mixin Record isB1 M of A1 M := { }.
HB.structure Definition B1 := {M of isB1 M & }.
HB.mixin Record isB2 M of A2 M := { }.
HB.structure Definition B2 := {M of isB2 M & isA2 M }.
HB.structure Definition B2A1 := {M of B2 M & A1 M }.
HB.structure Definition A2B1 := {M of A2 M & B1 M }.
if I add a structure such as HB.structure Definition A1A2 := {M of isA1 M & isA2 M}. the error message goes away
Reynald Affeldt (Apr 13 2021 at 05:07):@Kazuhiko Sakaguchi (<- thanks!) confirms that’s what I should have done
Enrico Tassi (Apr 13 2021 at 07:07):if It's possible, you could write something here https://github.com/math-comp/hierarchy-builder/wiki/FAQ (and open a bug report if the error message is bad)
Reynald Affeldt (Apr 14 2021 at 06:48):I issued but I don't seem to have write access to the FAQ.
Enrico Tassi (Apr 14 2021 at 07:00):should be fixed, apprarently the new default to let write only users with push access
Reynald Affeldt (Apr 14 2021 at 09:27):Error: No builders to declare, did you forget HB.instance?
What does this message mean when there actually is an HB.instance in the HB.context/HB.end section?
Reynald Affeldt (Apr 14 2021 at 09:28):(btw, this is the master version, with 1.1.0 I have no error message but I'm hit later in another file)
Last updated: May 28 2023 at 18:29 UTC