-
Notifications
You must be signed in to change notification settings - Fork 21
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
improve HB.instance #421
improve HB.instance #421
Conversation
gares
commented
Jun 10, 2024
•
edited
Loading
edited
- toposort using gref specific data structures
- fast fail for sub-classes of a class that failed to be inferred
The real bench is mca, I just added it, and I'm running it on my computer this afternoon (MCA takes about 20min if I recall correctly) |
@CohenCyril coq-community/coq-nix-toolbox#224 merged, could you please update the toolbox and rerun CI here |
CI green, this looks good to be (squashed and) merged |
I still don't get why There was a hack in ssrnum, maybe @CohenCyril recalls it? I don't think it should impact here though. |
The failure was about SemiGroup and Monoids, didn't felt like related to the hack (but maybe remotely who knows). |
FTR
|
We could also try with the version of toposort by @Tragicus but we need elpi 1.19.2 for an efficient coq.gref.set.fold |