Mac Malone

@Kha @JLimperg I encountered this same bug a while back myself in Alloy. The problem is with `PresistentEnvExtension`, the extensions is seen both in the precompiled shared object and by...

@Kha Ah, sorry, from this issue and my experience, I was under the impression it just part of how Windows loads module shared objects. I guess the idea is that...

@Kha Ah. I saw that issue, and while the 128 module limit problem you found was interesting, I was a little confused as to why that would be causing this...

@leodemoura > It seems only the `def` reserved name creates problems in practice. Should we use a different name for it? Would `def_eq` be appropriate? Having snake_case names for the...

@digama0 Agreed. The idea was that a single world reserved identifier like `def` (or `induct`) clash with both potential theorem and non-theorem user names, whereas a multi-world name only clashes...

@digama0 I am still not sold on the utility of this and it seems like a burden to maintain. Why is this necessary?

@digama0 > as the user needs to make sure to have the right version of `lake-ext` for the toolchain or else it will segfault. It's one of the main reasons...

@digama0 > I want access to this information so I can do arbitrary other things with it, not just lean-cache You can get this information already, though? A Lake script...

@digama0 My overarching concern here is that this seems like an XY problem. This fixes a problem for issues that seem like they would be best fixed elsewhere. > Tell...

> No, the end goal is for this to be a tool that sits where lake sits, mediating the download and compile process. It is not itself part of the...