You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In the following code, HB takes nearly 30s to find the unit ring instance. Some variation are faster. I got something even much slower (more that 2 min) on more complicated code. I can't figure out a clear pattern. So I put here a reasonably simple code where the time seems to be excessive.
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.
In the following code, HB takes nearly 30s to find the unit ring instance. Some variation are faster. I got something even much slower (more that 2 min) on more complicated code. I can't figure out a clear pattern. So I put here a reasonably simple code where the time seems to be excessive.
Is was with
installed with OPAM on
The text was updated successfully, but these errors were encountered: