Oh, yeah, I've been waiting with bated breath for a new release. Thought about doing it this way myself, since it definitely can build with the new version but is not quite stable yet.

Honestly, I think this is fine. If people want to use LLVM 13, they can use an older nixpkgs version.

I’m cool going with this if it’s still valuable in this form. I tend to be a little hesitant about shipping prerelease code from active upstreams, and in this case there’s a very measurable loss of functionality, but if you think it’s more useful than a dropped package I’m happy with the bump :) I just don’t know KLEE well enough to judge myself whether it can still be used for real tasks like this.

I wonder if the test disabling and asserts can be conditional on LLVM version. That way users can still overlay an older LLVM version if they want to use it. If a hello world still worked, and it was able to solve for some bitcode, that still seems useful, though I'll have to try with some examples I've got to verify how useful.

In any case, these problems will go away with a future Klee update. If we need to break things for now and a backport will fix them, that sounds fairly reasonable. 13 is way too old.

I’m a little hesitant to establish a precedent of in‐tree Nixpkgs expressions exposing functionality for removed versions of dependencies; I figure that anyone adventurous enough to get a removed LLVM building out‐of‐tree can overrideAttrs their way to or copy‐paste the KLEE expression too. The test failures differ across LLVM versions, too, so making this package version‐generic would involve building it for all of 17, 18, 19, 20, and soon 21.

How do you feel about including the disabled tests so that the package will build and run, but marking it as broken for now to signal to users that it’s not in a state upstream considers to be supported? Adventurous users can check the package and see that they can bypass it to get a partially‐functioning KLEE to play around with, even more adventurous users can pass it a removed LLVM version and overrideAttrs their way to a fully‐functional one, but casual users won’t be misled by any issues with the configuration until upstream fixes the issues. I’ve pushed that along with an explanatory comment, if you think it’s a good idea.

That sounds reasonable to me. Let me give this a final review shortly. :-)