I only just realized they did not offer any cinnamon powder so that's one obvious improvement right there

My mind cannot conceive of a better break. Please tell me about yours!

wavy

Summer is over, time for even more tea

Today I learned that you can just rent an AMD EPYC Genoa 9554P with 64 cores and 768GB RAM at $1.78/hr. That's crazy. ...well, you no longer can, at this particular provider, because I took the last one

`import Mathlib` is a great way to start development on a module because it gives you everything, including invisible parts like registered simp theorems, out of the box without having to hunt for specific imports. But once development has become more stable, it only makes sense to minimize […]

I don't have a clear answer to the sys time collapse specifically, so Fable's guess is as good as mine: "the wrapper modules formed wide waves of short-lived processes all faulting in the same Mathlib mappings at once, and that contention, not the wrappers' own work, was most of the sys time". I […]

The Modulize.lean port so far really is naive: it keeps all existing `import` directives at `public` i.e. transitively available in all downstream modules, matching non-module system semantics. But building on it, we can quite easily express something the Prove2Me paper alluded to but could not […]

I should highlight that one limitation of our 100-modules cone is that Mathlib size dominates it by almost two orders of magnitude while the full build is one OOM larger than Mathlib. So any effects on Mathlib importing will have outsized impact compared to importing between local modules in […]

Ok, let's talk about those statement/proof splits: as the paper describes, this is because "Lean recompiles the entire downstream cone whenever a module changes, even for a proof-only edit". Now, if you are following recent Lean, you might know this is no longer actually true: the module system […]

The low degree of parallelism is perhaps not too surprising for this small cone of the project when looking at the concrete `lake build` output: `Def_ModularCurve_CharLFrobeniusGeomLevel` alone takes about 55s, half as long as the entire build. Haven't looked at what intra-file parallelism looks […]

Now I haven't tried to build the entire repo yet. The readme says it took them 5hrs+ and 153GB RAM using 96 jobs, so let's maybe start with something smaller. Assuming Mathlib is already built, the following will build exactly 100 FLT modules: lake build P2M.Sol […]