Add arm8 bootstrap

[LudvikGalois]

No description provided.

[oskarabrahamsson]

• To get an arm64 compiler binary out of the bootstrap runs, you also need to add your target to this file: https://github.com/CakeML/cakeml/blob/master/developers/build-sequence.
• The 32-bit arm8 target seems unnecessary: are there are any armv8 processors that only support aarch32?

[LudvikGalois]

• To get an arm64 compiler binary out of the bootstrap runs, you also need to add your target to this file: https://github.com/CakeML/cakeml/blob/master/developers/build-sequence.

The arm64 bootstrap needs to be run on an arm64 system, so I don't think it makes sense to add it to the build-sequence, since whatever is running the regression tests is an x86-64 system.

• The 32-bit arm8 target seems unnecessary: are there are any armv8 processors that only support aarch32?

I'll remove the 32-bit target.

[tanyongkiam]

• To get an arm64 compiler binary out of the bootstrap runs, you also need to add your target to this file: https://github.com/CakeML/cakeml/blob/master/developers/build-sequence.

The arm64 bootstrap needs to be run on an arm64 system, so I don't think it makes sense to add it to the build-sequence, since whatever is running the regression tests is an x86-64 system.

The in-logic compilation runs inside HOL4 and can produce the arm64 version of the compiler's .S file even while ran on an x86-64 server. It would be good to have it in the regression so that we can distribute the arm64 version of the .S file (like we do for x86-x64).

[LudvikGalois]

The in-logic compilation runs inside HOL4 and can produce the arm64 version of the compiler's .S file even while ran on an x86-64 server. It would be good to have it in the regression so that we can distribute the arm64 version of the .S file (like we do for x86-x64).

Currently the makefile rule for the cake-arm8-64.tar.gz target includes a quick test to make sure the bootstrap works (because the x86-64 bootstrap had that test), and that won't run on an x86 machine. I'll remove that test since the x86-32 bootstrap doesn't have it, and then add arm8-64 as a target to the build-sequence file.

Also, sorry this is taking so long; I wanted to re-run the bootstrap after removing the arm8-32 bootstrap to make sure I didn't break anything.

[tanyongkiam]

Great, thanks.

Also, you don't need to run this yourself. Once the relevant files are in the build-sequence, open PRs will get picked up by the CakeML regression testing system.