Build & distribute release builds with Zig as stand-alone C compiler #659
Conversation
Kha
force-pushed
the
zig
branch
8 times, most recently
from
5234638
to
2fffc9f
Compare
|
To give a bit more context and a progress update, this PR tries to build all of Lean with Zig, and then copy it to An alternative approach would be to keep using system/Nix clang for compiling Lean itself and ship Zig only for compiling user Lean programs. Since Lean produces C code, not C++, and of a quite limited variety, it should be much easier to ensure that Zig can cope with it. However, we would still need to link Lean programs with the C++ standard library used for compiling the Lean stdlib, so we would need to ship its static library with Lean. That should work I think, but we could still run into compiler mismatches in advanced cases, e.g. LTO. And we would not be able to cross-compile Lean. So the first approach would be preferable. The solved and unsolved issues with it are:
And for the fun of it, let's try cross-compiling from x86_64-linux-gnu:
|
|
I'll take the liberty to ping @andrewrk himself here in case he's interested in our little Zig experiment & progress :) ... |
I hope so too :) |
Kha
force-pushed
the
zig
branch
5 times, most recently
from
26c1eaa
to
2ea6d3c
Compare
|
Phew, good progress on Windows after many more fixes & workarounds (see above)! The test suite is now all green on my Windows machine, while on CI it randomly fails in the interactive tests with a single last error 🤔 . Unfortunately, on macOS the tests uncovered many more linker issues that I don't see easy workarounds for/where the issue isn't even clear. I can open upstream issues for them, but unless someone is nice enough to specifically fix all of them for us, I think the only realistic solution is to ship without Zig on macOS for the time being. |
Kha
force-pushed
the
zig
branch
2 times, most recently
from
554b7d8
to
40527a9
Compare
Kha
force-pushed
the
zig
branch
2 times, most recently
from
7fc6e25
to
0bd78cc
Compare
In particular, use ccache if used for build
needs pthread.h
|
Obsoleted by #795, which did not run into any of the above issues apart from the Windows headers (which apparently are from the clang64 toolchain) |
* `@[to_additive]` will now correctly guess names with `CoeTC`, `CoeT` and `CoeHTCT` in it * rewrite function `targetName`. - It will now warn the user if it gives a composite name that can be auto-generated (before `to_additive` would never warn if a composite name was given). - the logic when `allowAutoName = true` now corresponds to the docstring - Fix a bug where declarations were silently allowed to translate to itself (maybe because the `return` statements returned a value for the whole function?) - Add some more tracing - The behavior of namespaces when giving a composite name has been changed. It will always generate a name with the same number of components. Example: ```lean namespace MeasureTheory.MulMeasure @[to_additive AddMeasure.myOperation] def myOperation := ... -- before: generates `AddMeasure.myOperation` (and never gives a warning) -- after: generates `MeasureTheory.AddMeasure.myOperation` (and probably warns that the name can be auto-generated) end MeasureTheory.MulMeasure ``` * This should fix all problems in leanprover#659 other than leanprover#660 Minor changes: * When applying `@[to_additive]` to a structure, add a trace message if no translation is inserted for a field. * Define `Name.fromComponents` and `Name.splitAt` * Reduce transitive imports of `Tactic/toAdditive` * Move some auxiliary declarations from `Tactic/Simps` to more appropriate places - swap arguments of `String.isPrefixOf?` - improve `Name.getString` Co-authored-by: Scott Morrison <scott@tqft.net>
As they say, Zig is an obvious choice for what C compiler to ship with your language. In particular, this is a big step towards zero-setup native compilation on Windows.
We use Zig's cross-compilation feature to link the Linux build against the ancient glibc 2.15, obviating the previous workaround of using an older nixpkgs channel that combines a not-quite-recent glibc with a not-quite-recent clang. Other cross-compilation targets for platforms not supported by GH Actions would also be interesting, though I wasn't able to find one that works out of the box from Linux yet.