fix: explicitly initialize Std in lean_initialize
#4668
Conversation
github-actions
bot
added
the
toolchain-available
| @@ -5,5 +5,6 @@ Authors: Markus Himmel | |||
| -/ | |||
| prelude | |||
| import Std.Data.DHashMap.Basic | |||
| import Std.Data.DHashMap.RawLemmas | |||
There was a problem hiding this comment.
@TwoFX Just checking, was orphaning the file intentional?
There was a problem hiding this comment.
Yes, the idea was that in the "normal" use case where you just want to use HashMap and not HashMap.Raw you can just import Std.Data.HashMap and import only the files that are needed for HashMap.
In fact, the same thing should be true for all three of DHashMap, HashMap and HashSet, so I'm surprised that just changing this for DHashMap made any difference.
There was a problem hiding this comment.
Ah, maybe it's because DHashMap.RawLemmas has macros in it, unlike HashMap.RawLemmas and HashSet.RawLemmas?
There was a problem hiding this comment.
Yes, exactly. It's a limitation of the bootstrapping setup, if you will. But note that a Lake build would also skip orphan files.
Perhaps the import should be moved to Std.Data instead then? Unlikely people will import that and then complain that it contains too much stuff.
There was a problem hiding this comment.
Sounds good to me, I'll open a PR.
Fixes the stage 2 build, which runs with
prefer_native=true