OCaml for ARM MacOS

,

As a user of Coq on Macs, I wonder if OCaml will add native support for their new ARM CPUs, and how hard it is, and how long would that take roughly — 1month, 1 year, 10 years?

I realize this question might be very hard and annoying to answer, but I see OCaml has already ports for ARM-Linux and Mac-x86, which gives me hope?

5 Likes

I don’t think it would be very hard: there is an open PR https://github.com/ocaml/ocaml/pull/9699 at the moment adding support for the ARM architectures used in (some?) iPhones, and it is not a very large patch.

Best wishes,
Nicolás

2 Likes

The hardest bit of this will getting this in CI, since Apple is charging $500 for a (returnable) loan of their preview kit. I’m going to cough up the cash for this, but it’s pretty developer hostile. If anyone at the Apple open source program office is listening - send us some kit that doesn’t need to be returned, so it can be racked up for test purposes!

14 Likes

@nojb all Apple products uses almost the same architecture nowadays, ARM64(v8), ARM32 is not supported anymore, so this patch gets all iPhone’s since the iPhone 5s. There is also ARMv8.3 called arm64e, which is a must for some low level things(like drivers? and system plugins?).

Besides of that is the same kernel. In a different mode, if you look at the XNU source you’re going to see a lot of flags checking to see if it is a SECURE_KERNEL(like iOS) or not(like a mac)

#If SECURE_KERNEL

As pointed by @avsm the main problem is getting the CI to work, I will get my hands on one somehow, maybe not literally but an SSH. But ideally INRIA would have it running

Weird ways to test it

Another alternative is an iPhone X tethered, as it supports jailbreak in every version(it’s a ROM level bypass), about $450 US dollars used. But I’m almost sure that there is some under NDA Apple thing for compilers and tools like that(like an iPhone prototype with JTAG enabled) and tools to hook that properly. So if anyone knows someone who knows someone, that would solve the problem.

Another alternative, I have iOS 12 running on xnu-qemu-arm64, on Linux I made some patches to support async networking, and I’m also working on a KVM patch to that to run on the Raspberry PI. I “made” the patch at #9699 originally in the emulator. That is probably not legal, but really simple to maintain and it’s ready today, jailbreak is actually OK in most countries if you don’t break any DMCA.

I would like to have both macOS ARM and iOS ARM, especially because there is some code which is valid at only iOS, but this second one isn’t so simple to maintain.

COQ

Epecifically, there is one test failing which can imply that COQ is still not running, something related to unboxed primitives.

3 Likes

I think it’s possible to use Corellium iPhone emulation for development. Many projects and researchers rely on it. For example, Go language uses it for CI.

Another alternative is to run iOS in QEMU as it had been told already:

They published the source code at GitHub:

Hope that helps.

1 Like

At the platform state of the union, they announced that they will send Pr for the Mac ARM support to many oss projects.

Would be nice to find a way to have OCaml on the list

2 Likes

10 days? :innocent: The OCaml ARM64 code generator is in very good shape already, and the recent pull request https://github.com/ocaml/ocaml/pull/9699 adds iOS ARM64 support, which should not be very far from macOS ARM64 support.

However, I would really like to have SSH access to one of those MacMini ARM64 development platforms. That would speed up porting and testing tremendously. Emulators and jailbreaked phones are a pain.

13 Likes

I don’t have such a box, so I can only ask around on Twitter — feel free to retweet for reach or make a better tweet https://twitter.com/Blaisorblade/status/1275840699477434369

1 Like

So, while we’re on the topic of ARM, android also uses ARM. How hard is it to produce binaries for that as well?

If someone started a crowdfunding compain to get the box I would definitely back it.

4 Likes

@bluddy not hard, Android needs some patches after Android 5.0, I have it setup for ARM64 and x86_64 at my personal project, also got iOS x86_64 and ARM64.

I have a tooling to cross compile almost anything with esy, similar to ocaml-cross but more versatile and works with essentially any dune package not using cstubs(you need a patch for that). It was working with OCaml 4.08

The patches itself, not great yet, but will open a PR in the future. Also I want to get x86 PIC to work(Android requires that), which is a lot harder than iOS and Android ARM.

5 Likes

The emulator after you get to work is actually nice, works exactly like any VM, SSH and all, if you guys are okay with that I can setup the CI using it.

But also, maybe trying to give Corellium a try? I’m not a huge fan o Go but if they’re using as a CI it’s probably reliable.

Technically even the ABI of the mac ARM is the same as iOS so I would bet 99% is similar, probably same linker, same kernel. But would be great to have the real thing running as there is a lot of small limitations(like stack_size)

3 Likes