Enrico Borba

> Just adding the git hash here would defeat most of benefits of using nix, such as a cache hit if you build identical sources. How would you have identical...

Fair enough, I think this is enough rationale not to pursue adding the git hash like I proposed. Since nix installs are not technically supported, nix users can patch in...

Is `LEAN_GITHASH` read during runtime? Setting it to a garbage value and doing `lake update` still downloads the cache successfully (making me think it's not being used in the way...

Yeah that would simplify using the cache through a nix install. The devshell could then export `LEAN_GITHASH` locked to the lean4 revision that was used as an input to the...

Yeah but I think the mathlib cache code runs lake (and lean) through `elan`, instead of letting the current `PATH` find those binaries.

Was there any Zulip discussion on deprecating the Nix build?

So I'm in middle of a major rewrite because of this issue: https://github.com/enricozb/intuitive/issues/4, but I'm curious why [`VStack`](https://docs.rs/intuitive/latest/intuitive/components/struct.VStack.html) or [`HStack`](https://docs.rs/intuitive/latest/intuitive/components/struct.HStack.html) wouldn't work here?

Ah I see. Okay I'll keep this in mind as I'm designing the components. This is a good use case for fixed size components. Like I mentioned earlier, I'm going...

Thanks for the PR! This looks safe to me, I'll probably remove the comment though. Please feel free to make PRs for any widgets you'd like to add! If they're...

This is a known problem. I've thought a lot about how to implement this but I'm unsure what the best way is. I'll try see if I can implement a...