Stream: Hierarchy Builder devs & users

Topic: Instance declaration takes nearly 30s...


view this post on Zulip Florent Hivert (Dec 24 2023 at 15:36):

Deoending on how section are organized, variants of the following code could take a very long time. Here is an example

From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg.
From mathcomp Require Import mpoly.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section DefType.
Variables (n : nat) (R : ringType).
Record sympoly : predArgType :=
  SymPoly {sympol :> {mpoly R[n]}; _ : sympol \is symmetric}.

HB.instance Definition _ := [isSub of sympoly for sympol].
HB.instance Definition _ := [Choice of sympoly by <:].
HB.instance Definition _ := [SubChoice_isSubLalgebra of sympoly by <:].
End DefType.

Section SymPolyComRingType.
Variables (n : nat) (R : comRingType).
HB.instance Definition _ := [SubRing_isSubComRing of (sympoly n R) by <:].
HB.instance Definition _ := [SubChoice_isSubAlgebra of (sympoly n R) by <:].
End SymPolyComRingType.

Section SymPolyIdomainType.
Variables (n : nat) (R : idomainType).
HB.instance Definition _ := [SubRing_isSubUnitRing of (sympoly n R) by <:].   (* stuck here for more than 25s *)
HB.instance Definition _ :=
  [SubComUnitRing_isSubIntegralDomain of (sympoly n R) by <:].
End SymPolyIdomainType.

Is this normal ? Is there a way to improve that ?

view this post on Zulip Cyril Cohen (Dec 25 2023 at 22:08):

Hi! Merry Christmas, thank you for reporting this. This will give us an opportunity to investigate the slowdowns related to subtypes. Can you fill an issue please?

view this post on Zulip Florent Hivert (Dec 26 2023 at 20:54):

@Cyril Cohen Merry Christmas to you !

view this post on Zulip Florent Hivert (Dec 26 2023 at 22:00):

This is https://github.com/math-comp/hierarchy-builder/issues/408


Last updated: Apr 21 2024 at 02:41 UTC