Stream: Hierarchy Builder devs & users

Topic: Debug Commands


view this post on Zulip 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.

view this post on Zulip Cyril Cohen (Apr 02 2021 at 14:30):

You can use the attribute:

view this post on Zulip Enrico Tassi (Apr 02 2021 at 14:47):

Also HB.status and HB.graph

view this post on Zulip 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)

view this post on Zulip Enrico Tassi (Apr 03 2021 at 10:10):

You need to Require Import HB before other files using it

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Apr 03 2021 at 10:11):

So it won't happen soon ;-)

view this post on Zulip Reynald Affeldt (Apr 03 2021 at 11:36):

Indeed, that was it! Thank you!

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Apr 05 2021 at 10:46):

https://github.com/math-comp/hierarchy-builder/wiki/FAQ

view this post on Zulip 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_»

view this post on Zulip Enrico Tassi (Apr 08 2021 at 10:48):

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.

view this post on Zulip Enrico Tassi (Apr 08 2021 at 10:49):

the message is perfectible, but it seems the order in which you are declaring your structures is not bottom up

view this post on Zulip Enrico Tassi (Apr 08 2021 at 10:53):

IMO you did the join before doing one of the two siblings

view this post on Zulip Enrico Tassi (Apr 08 2021 at 10:55):

https://github.com/math-comp/hierarchy-builder/pull/214

view this post on Zulip 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]

view this post on Zulip Enrico Tassi (Apr 08 2021 at 11:47):

How can I reproduce your exact issue?

view this post on Zulip Reynald Affeldt (Apr 08 2021 at 13:18):

view this post on Zulip Enrico Tassi (Apr 08 2021 at 13:18):

@Cyril Cohen

view this post on Zulip Reynald Affeldt (Apr 08 2021 at 13:18):

It's about exceptStateRun and nondetState

view this post on Zulip Reynald Affeldt (Apr 08 2021 at 13:22):

https://github.com/affeldt-aist/monae/blob/monae_hb/hierarchy.v

view this post on Zulip Reynald Affeldt (Apr 12 2021 at 09:50):

smaller.png

view this post on Zulip Reynald Affeldt (Apr 12 2021 at 09:50):

it might boil down to that (so that an intermediate mixin might do it)

view this post on Zulip Enrico Tassi (Apr 12 2021 at 10:32):

can you sum up your discovery?

view this post on Zulip 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

view this post on Zulip Reynald Affeldt (Apr 13 2021 at 05:07):

@Kazuhiko Sakaguchi (<- thanks!) confirms that’s what I should have done

view this post on Zulip 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)

view this post on Zulip Reynald Affeldt (Apr 14 2021 at 06:48):

I issued but I don't seem to have write access to the FAQ.

view this post on Zulip Enrico Tassi (Apr 14 2021 at 07:00):

should be fixed, apprarently the new default to let write only users with push access

view this post on Zulip 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?

view this post on Zulip 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: Jan 29 2023 at 15:02 UTC