Stream: Hierarchy Builder devs & users

Topic: Hierarchy builder error


view this post on Zulip Erik Martin-Dorel (Mar 25 2022 at 13:45):

(Pierre Pomeret-Coquot and I started using hierarchy builder, which is a very pleasant! but we have a possibly-simple question: )

The following code:

From Coq Require Import ssreflect.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import all_algebra.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

From HB Require Import structures.
Declare Scope hb_scope.
Delimit Scope hb_scope with G.
Open Scope hb_scope.

HB.mixin Record neset_of_set (W : finType) :=
  { neset_val : {set W} ;
    neset_ax : neset_val != set0 ;
  }.

HB.structure Definition neset := { M of neset_of_set M }.

yields

(* Toplevel input, characters 15-72: *)
(* > HB.structure Definition neset := { M of neset_of_set M }. *)
(* > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
(* Error: HB: coercion not to Sortclass or Funclass not supported yet. *)

We didn't find this error in the FAQ https://github.com/math-comp/hierarchy-builder/wiki/FAQ ; so, is it easy to explain this issue in a "low-level and/or simple" way?

And if (as we suspect) migrating to a more recent version of mathcomp and/or hierarchy builder might address this one, which versions should be enough?

Thanks!

— FWIW, an excerpt of the deps we use:

coq                     8.13.1      pinned to version 8.13.1
coq-elpi                1.11.1      Elpi extension language for Coq
coq-hierarchy-builder   1.2.1       High level commands to declare and
evolve a hierarchy based on packed classes
coq-mathcomp-ssreflect  1.14.0
elpi                    1.13.8      ELPI - Embeddable λProlog Interpreter

view this post on Zulip Notification Bot (Mar 25 2022 at 13:47):

This topic was moved here from #math-comp users > Hierarchy builder error by Karl Palmskog.

view this post on Zulip Karl Palmskog (Mar 25 2022 at 13:48):

(even though this was also about MathComp, we want to encourage specialized streams, and people can follow the link from the MathComp stream)

view this post on Zulip Pierre Roux (Mar 25 2022 at 13:53):

I guess the issue is the W : finType. You are trying to extend a hierarchy on a non HB hierarchy which is not really supported (I have a hack somewhere in dioid that somewhat does it bu that's terribly broken). What you need is the HB port of mathcomp (aka MathComp 2.0): https://github.com/math-comp/math-comp/tree/hierarchy-builder but that's no yet released.

view this post on Zulip Erik Martin-Dorel (Mar 25 2022 at 13:57):

OK thanks @Pierre Roux !

view this post on Zulip Julien Puydt (Mar 25 2022 at 14:04):

When will it be released? (curious)

view this post on Zulip Pierre Roux (Mar 25 2022 at 14:15):

Las answer I got was "before christmas" but that was last year so I don't know.
Likely after 8.16, hopefully before christmas 2022, but I really don't know.


Last updated: Jan 29 2023 at 15:02 UTC