Cross-compiled build for Linux/aarch64#734
Closed
gebner wants to merge 1 commit intoleanprover:masterfrom
Closed
Conversation
Member
|
I'll cherry-pick the fix to master tomorrow. For the remainder it might make more sense to wait for #733 first. |
Member
Member
Author
|
I believe Sebastian wants to do this in a completely different way. |
Member
|
For what it's worth, the first alpha release of Asahi Linux might increase the priority of this feature a little; personally I'm waiting for better 16K pages support in Emacs & libunwind. There are even reports about Linux on M1 being faster than macOS. I'll try cross-compiling LLVM as soon as this PC has been upgraded to more than 8GB RAM. |
ChrisHughes24
pushed a commit
to ChrisHughes24/lean4
that referenced
this pull request
Dec 2, 2022
mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7 porting notes: mostly smooth but: 1. there were two places where I had to add `MulZeroClass` explicitly (toward the end of the file), which was weird 2. one declaration is surprisingly slow for no apparent reason
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This adds a new build for Linux/aarch64, which is cross-compiled on github actions. The tests are run using CPU emulation.
The release tarball is called
lean-x.y.z-linux_aarch64.tar.gz, this is supported by recent elan versions.The main difficulty was getting stage0 to work as a cross-compiler (i.e., compile the stage0 compiler for amd64 but have it generate oleans and C files that run on aarch64). It turns out that the oleans were not architecture-independent, because of the hash function we use for strings. This function had a parameter of type
char const *, on amd64 this issigned char const *, on aarch64 this isunsigned char const *. I have changed it tounsigned charindependent of the architecture (requiring a stage0 update).(Thanks to @Kha for pointing me to the olean files as a source of troubles. In order to debug the olean differences, I wrote a small and very incomplete olean parser in Lean: https://github.com/gebner/oleanparser)