Erik Martin-Dorel (Mar 25 2022 at 13:45): 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
This topic was moved here from #math-comp users > Hierarchy builder error by Karl Palmskog.
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)
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.
Erik Martin-Dorel (Mar 25 2022 at 13:57):OK thanks @Pierre Roux !
Julien Puydt (Mar 25 2022 at 14:04):When will it be released? (curious)
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: Apr 19 2024 at 13:02 UTC