Dan Christensen

Here's something easy that is win-win: look for unneeded imports. Importing large things takes a surprising amount of time. I checked Descent.v and Separated.v, and found a bunch. Removing unneeded...

Cool. If someone wants to give it a try, please do!

And here are the 20 slowest lines in the library. This is after #1267, which greatly speeds up BlakersMassey. (In current master, it tops the list with >10s on one...

I tried using @JasonGross 's minimize-requires script, but I couldn't get it to work on the HoTT library. I opened an issue: https://github.com/JasonGross/coq-tools/issues/123 It would be great to get rid...

This seems to even mangle things that are explicitly named, e.g. if I start with ``` Definition foo : forall X : Type, forall x : X, X. ``` then...

I'm impressed that it worked! I sometimes forget to make things robust to name choices. We could consider adding the option to one of the CI runs.

Jarl and I have been finding the Integers defined using the binary naturals to be pretty painful to deal with. You have to case split on pos, neg and zero,...

I see that there is a related issue: #1154. (And I forgot to tag @jarlg .) Maybe efficiency is more important than I realize? In a slightly different direction, is...

Thanks, that explains why it's not so easy to reuse code from the stdlib. That's unfortunate. I'm still unsure about whether working with binary numbers is worth it. I guess...

@Alizter Yes, I found working with binary positives difficult. Too many cases arise. Even with the custom induction principle, you end up having to reprove things for Pos that we...