Joachim Breitner

Creating these projects dynamically seems easy. Adding them to the config a bit more tedious. Maybe lean4web could (or does it already) support non-listed projects for every directory in the...

> that it shouldn't be very hard to create all the directories appropriately. Already on it > Is there a reason why you specifically say "creating a project for every...

Here we go: There is still an issue with old versions that don’t support `experimental.module` yet… Feature requests: * Recognize when the project does not exist, and give a proper...

Ok, fixed that one as well, so now https://live.lean-lang.org/#project=lean-v4.0.0&codez=MQUwbghgNgBAMiCA7AdGEAnAzgSwPZIDKALhjkgOZA works as well

RCs are being installed as we speak, so I think we are good here (up to the usability feature requests above about non-configured projects)

That said, we should be monitoring this: ``` [root@live:~]# du -sh /home/lean4web/.elan/toolchains/ 176G /home/lean4web/.elan/toolchains/ ``` 😅 ``` [root@live:~]# du -sh $(ls -dv /home/lean4web/.elan/toolchains/*) 2.4G /home/lean4web/.elan/toolchains/leanprover--lean4-nightly---nightly-2025-09-29 2.4G /home/lean4web/.elan/toolchains/leanprover--lean4-nightly---nightly-2025-09-30 2.4G /home/lean4web/.elan/toolchains/leanprover--lean4-nightly---nightly-2025-10-01 2.4G...

I’d just rip out all the reference buffer handling code. We don’t have these kinds of references anywhere on the IC , and I expect by the time we get...

Did you read https://www.joachim-breitner.de/blog/786-A_Candid_explainer__Quirks? The first section is relevant.

We can also just leave it as it. But I'd rip it out before investing more into it

Hmm, but aren't these scoped for a reason? The feature I could see here is that you can specify which namespaces were opened, and then it'll just work. Tedious to...