Jacques Carette
Jacques Carette
So this feels like the tip of a very large iceberg. It's a symptom of a fundamental "how do we do APIs in dependently-typed programming?" question. Repeating some of the...
I'm fine with that (i.e. leave it to a subsequent refactoring). Fair to say that if I believe in this splitting enough, I should be willing to do it myself...
What did `pr_label_update.py` do? (I'm not against deleting it, I just want to be more informed first).
I think the idea was to automate that "quick peek into the logs" - which still seems like a good idea! It would just need to be ported to be...
@hrzhuang could you try to take over this PR please?
Once you've 'mined' this, do close this PR please.
So are the times still roughly on par with the table at the top of this issue? I'd be curious to know where we are at, before deciding to not...
Yes, making sure the build happens in 'optimal' order is a good idea. I think builds generally work, but hlint often fails. And good point about TeX.
And also remember that in that same Issue, I pointed out 'precompilate' for LaTeX headers which might help too. It might be worthwhile to revisit the table at the very...
Yes, let's close this one as done and open a new one.