Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support for Apple Silicon? #168

Closed
k4rtik opened this issue Nov 7, 2021 · 42 comments
Closed

Support for Apple Silicon? #168

k4rtik opened this issue Nov 7, 2021 · 42 comments

Comments

@k4rtik
Copy link
Contributor

k4rtik commented Nov 7, 2021

Hi

When I tried the 2021.09.0 install script for macOS on an M1 Macbook Air, I received the error that uname -m output of "arm64" was unrecognized.

Are Apple's new SoCs supported at all?

@MSoegtropIMC
Copy link
Collaborator

Sorry - not yet, mostly because we have no means to do CI tests.

But as far as I know opam does support it, so it shouldn't be that hard to fix. I would appreciate if you could try it.

@MSoegtropIMC
Copy link
Collaborator

For this specific error, the fix should be to add to the case in shell_scripts/init_machine_type.sh these lines:

    arm64)
      BITSIZE=64
      HYPHEN32=
      HYPHEN64=-64
      ;;

You might encounter a few other places ...

@k4rtik
Copy link
Contributor Author

k4rtik commented Nov 8, 2021

Ah, that's good to know. I was surprised that the lack of support was not documented anywhere in the repo.

When I get a chance to test, I will report back here.

@Zimmi48
Copy link
Member

Zimmi48 commented Nov 9, 2021

We should probably add a link to this known issue from the release notes.

@MSoegtropIMC
Copy link
Collaborator

@Zimmi48 : yes done. I also encouraged people who have Apple silicon to ping us for a remote debug session.

@k4rtik
Copy link
Contributor Author

k4rtik commented Nov 9, 2021

Alright, with the changes that @MSoegtropIMC suggested above I got up to the following:

===== CHECKING VERSION OF INSTALLED OPAM =====
Found opam 2.1.0 - good!
/opt/homebrew/bin/opam
===== opam already initialized =====
===== CREATE OPAM SWITCH =====
[__coq-platform.2021.09.0.patch_ocaml] Initialised
[__coq-platform.2021.09.0.patch_coq-released] Initialised
[__coq-platform.2021.09.0.patch_coq-dev] Initialised
[coq-released] Initialised
[coq-core-dev] Initialised
[coq-extra-dev] Initialised

<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><>  🐫
Switch invariant: ["ocaml-base-compiler" {= "4.10.0"}]
[ERROR] Could not determine which packages to install for this switch:
  * Missing dependency:
    - ocaml-base-compiler = 4.10.0
    unmet availability conditions: '!(os = "macos" & arch = "arm64")'


Switch initialisation failed: clean up? ('n' will leave the switch partially installed) [Y/n] y

But after changing the ocaml-base-compiler version to 4.10.2 that supports arm64 at:

COQ_PLATFORM_OCAML_VERSION='ocaml-base-compiler.4.10.0'

I was able to proceed seamlessly. Here's a log for specifics: https://gist.github.com/k4rtik/e23a87f573c7b6e16cac4ec1c89615cc

@k4rtik
Copy link
Contributor Author

k4rtik commented Nov 9, 2021

Unsure if the maintainers want to wait until the availability of the CI to add (unofficial) support to the scripts. If it's not a blocker, I am happy to submit a PR.

PS: I may be able to test with other versions of Coq supported in version 2021.09.0, at least for the base installs.

@MSoegtropIMC
Copy link
Collaborator

@k4rtik : I would be fine to have a "not official / beta" support for Apple silicon.

Regarding ocaml: it might suffice to change the OCaml version to 4.10.2.

See 4.10.0 vs 4.10.2.

One would have to change this here (keep the cygwin version as is):

COQ_PLATFORM_OCAML_VERSION='ocaml-base-compiler.4.10.0'

@MSoegtropIMC
Copy link
Collaborator

P.S.: The ocaml version chosen is the same for all versions of Coq in Coq Platform 2021.09.0.

@MSoegtropIMC
Copy link
Collaborator

@k4rtik : sorry, I didn't see the second part of your post - so with the two changes it does work on Apple silicon?

Can you please try "extended/x" instead of "base/b"?

If this works, I would appreciate a PR. The only thing we have to check is if 4.10.2 is available on Windows, but I wouldn't see it as a blocker to have 4.10.0 on Windows and 4.10.2 elsewhere. Also I would ask you to check new versions of the Coq Platform in a timely manner (until I can get my own M1 Mac mini back to life - I bricked it in an attempt to install a fresh OS for testing ...).

@k4rtik
Copy link
Contributor Author

k4rtik commented Nov 10, 2021

@k4rtik : sorry, I didn't see the second part of your post - so with the two changes it does work on Apple silicon?

No problem and yes, it worked without any issue with base.

Can you please try "extended/x" instead of "base/b"?

I will try later this week.

If this works, I would appreciate a PR. The only thing we have to check is if 4.10.2 is available on Windows, but I wouldn't see it as a blocker to have 4.10.0 on Windows and 4.10.2 elsewhere.

The page I linked to for 4.10.2 above does confirm support for Windows/Cygwin:

Source distribution
Source tarball (.tar.gz) for compilation under Unix (including Linux and macOS)
and Microsoft Windows (including Cygwin).

Also I would ask you to check new versions of the Coq Platform in a timely manner (until I can get my own M1 Mac mini back to life - I bricked it in an attempt to install a fresh OS for testing ...).

I can't promise this yet as I am yet to receive my own M1 Pro machine. I have been trying out M1 on a friend's machine released last year to make sure that the things I need will work. But happy to help when I can.

@k4rtik
Copy link
Contributor Author

k4rtik commented Nov 11, 2021

I am trying the extended install. The first error I ran into is package gappa is unable to find gmp which is actually installed:

[ERROR] The compilation of gappa.1.4.0 failed at "./configure CXXFLAGS=-I/opt/local/include --prefix=/Users/kartik/.opam/__coq-platform.2021.09.0~8.13".

Full log for opam install gappa:

kartik@Kartiks-MacBook-Pro platform % opam install gappa
The following actions will be performed:
  ∗ install gappa 1.4.0

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫
⬇ retrieved gappa.1.4.0  (cached)
[ERROR] The compilation of gappa.1.4.0 failed at "./configure CXXFLAGS=-I/opt/local/include --prefix=/Users/kartik/.opam/__coq-platform.2021.09.0~8.13".

#=== ERROR while compiling gappa.1.4.0 ========================================#
# context     2.1.1 | macos/arm64 | ocaml-base-compiler.4.10.2 | https://opam.ocaml.org#38d03f63
# path        ~/.opam/__coq-platform.2021.09.0~8.13/.opam-switch/build/gappa.1.4.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build ./configure CXXFLAGS=-I/opt/local/include --prefix=/Users/kartik/.opam/__coq-platform.2021.09.0~8.13
# exit-code   1
# env-file    ~/.opam/log/gappa-47045-90ddec.env
# output-file ~/.opam/log/gappa-47045-90ddec.out
### output ###
# [...]
# checking whether gcc accepts -g... yes
# checking for gcc option to enable C11 features... (cached) none needed
# checking how to run the C preprocessor... gcc -E
# checking how to run the C++ preprocessor... g++ -E
# checking for g++... g++
# checking whether the compiler supports GNU C++... (cached) yes
# checking whether g++ accepts -g... yes
# checking for g++ option to enable C++11 features... (cached) none needed
# checking how to run the C++ preprocessor... g++ -E
# checking whether g++ supports C++11 features with -std=gnu++11... yes
# checking for __gmpz_init in -lgmp... no
# configure: error:  *** Unable to find GMP library (http://www.swox.com/gmp/)



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫
┌─ The following actions failed
│ λ build gappa 1.4.0
└─
╶─ No changes have been performed
# Run eval $(opam env) to update the current shell environment
kartik@Kartiks-MacBook-Pro platform %

I guess the source of this error might be

"CXXFLAGS=-I/opt/local/include" "LDFLAGS=-L/opt/local/lib" { os-distribution = "macports" & os = "macos" }

because on arm64 homebrew installed gmp is found at /opt/homebrew/include but then it's not clear to me why opam install gappa fails in other switches as well.

EDIT: Ah, even the opam package has the same issue: https://github.com/ocaml/opam-repository/blob/6603f2c2661a8fe202a6e1766382e48a94fb9ef5/packages/gappa/gappa.1.4.0/opam#L17

@k4rtik
Copy link
Contributor Author

k4rtik commented Nov 11, 2021

Found the issue, the configure command needs to be passed the following: CPPFLAGS=-I/opt/homebrew/include LDFLAGS=-L/opt/homebrew/lib to find gmp and boost libraries for gappa.

Here's a PR: ocaml/opam-repository#19990

MSoegtropIMC added a commit that referenced this issue Nov 12, 2021
Add unofficial support for Apple Silicon, see: #168
@k4rtik
Copy link
Contributor Author

k4rtik commented Nov 12, 2021

Just adding some stats here as I try some combinations of packages on main branch after merge of #171:

Desc Time Switch
x,1,p,4,n 36m 30s __coq-platform.2021.09.0~8.13
x,1,p,4,y,y 31m 40s __coq-platform.2021.09.0~8.13
f,1,p,4,y,y 29m 16s __coq-platform.2021.09.0~8.13
f,3,p,4,y,y failed __coq-platform.2021.09.0~8.12
f,4,p,4,y,y 27m 5s __coq-platform.2021.09.0~8.14+beta2
f,5,p,4,y,y 25m 19s __coq-platform.2021.09.0~8.14~ltacdebug
b,3,p,4 4m 31s __coq-platform.2021.09.0~8.12
b,4,p,4 5m 50s __coq-platform.2021.09.0~8.14+beta2
b,5,p,4 5m 6s __coq-platform.2021.09.0~8.14~ltacdebug

Note, some of these numbers (especially the first and second) include time for downloading packages and hence may seem more than actual.

My config is:

$ system_profiler SPHardwareDataType
Hardware:

    Hardware Overview:

      Model Name: MacBook Pro
      Model Identifier: MacBookPro18,3
      Chip: Apple M1 Pro
      Total Number of Cores: 10 (8 performance and 2 efficiency)
      Memory: 16 GB

@k4rtik
Copy link
Contributor Author

k4rtik commented Nov 14, 2021

I was able to compile the failing config in the table above after merge of ocaml/opam-repository#20004, so I am happy to consider this issue resolved.

Let me know if you need me to test any other specific config. I should have easy access to a M1 Pro machine for the foreseeable future.

@MSoegtropIMC
Copy link
Collaborator

Thanks for your help with this!

It would make sense to test the 8.14+beta2 config as well.

Please note that the config numbers will change soon in main.

I keep the issue open until release so that people more easily find it.

@k4rtik
Copy link
Contributor Author

k4rtik commented Nov 14, 2021

It would make sense to test the 8.14+beta2 config as well.

Do you mean test it with some option other than full (f)? I did test it for full and base as shown in the table above.

@k4rtik
Copy link
Contributor Author

k4rtik commented Nov 21, 2021

So I just tried installing __coq-platform.2021.11.0~8.14~2021.11 with f,1,p,4,y,y options and it took my machine 29m 20s. With the same options, it took 27m 25s for __coq-platform.2021.11.0~8.13~2021.11.

I think I am quite satisfied. Let me know if you need me to test any other config.


With extended instead of full above:

  1. 31m 39s (8.14)
  2. 34m 53s (8.13)

Fri Dec 3

 ❯ git describe
2021.09.0-54-g8568054
 ❯ time ./coq_platform_make.sh -extent=x -pick=8.14~2021.11 -parallel=p -jobs=4 -compcert=y -vst=y -switch=d
...
8156.30s user
990.69s system
556% cpu
27:24.00 total
 ❯ time ./coq_platform_make.sh -extent=x -pick=8.13~2021.11 -parallel=p -jobs=4 -compcert=y -vst=y -switch=d
8398.90s user
1060.70s system
565% cpu
27:52.69 total

@MSoegtropIMC
Copy link
Collaborator

Thanks for the tests - indeed this is quite fast. Just to make sure: this where builds from scratch - not just an update of an already existing switch?

I am about to add a few more non Coq ocaml packages, notably a generator for prime proofs (currently in CI) and a special Z3 for Coq hammer. These might be tricky on ARM silicon. I will ping you as soon as it passed the other CI.

@MSoegtropIMC
Copy link
Collaborator

P.S.: in general it would make sense to test the 'x' variant - it should take only slightly longer.

@k4rtik
Copy link
Contributor Author

k4rtik commented Nov 22, 2021

Oh I was under the impression that full had more packages than extended.

@k4rtik
Copy link
Contributor Author

k4rtik commented Nov 22, 2021

Just to make sure: this where builds from scratch - not just an update of an already existing switch?

Yes. Sometimes these include times for downloading packages, but that will only be an overestimate then, not underestimate.

@k4rtik
Copy link
Contributor Author

k4rtik commented Nov 22, 2021

a special Z3 for Coq hammer. These might be tricky on ARM silicon.

Hope it's not too special, we had a fun time getting a new Z3 version out that works on macOS. But it helps that I got to participate in that process.

@MSoegtropIMC
Copy link
Collaborator

As far as my limited understanding goes, this is just a different frontend which uses the usual Z3 shared library.

@k4rtik
Copy link
Contributor Author

k4rtik commented Nov 22, 2021

I see. The main change we may have to do on macOS is to use the dynamic library instead. But happy to investigate when it's ready.

@MSoegtropIMC
Copy link
Collaborator

@k4rtik : in #186 it was reported that OCaml 4.10.2 doesn't work for WSL2 (Windows Subsystem for Linux). The reporter found that 4.13.1 does work. Would you ming to test if 4.13.1 also works for Apple Silicon?

@MSoegtropIMC
Copy link
Collaborator

P.S.: better test 4.13.2 - the latest patch release for 4.13.

@k4rtik
Copy link
Contributor Author

k4rtik commented Nov 26, 2021

Just to be sure, I don't see an ocaml-base-compiler release for 4.13.2 yet, just up to 4.13.1: https://opam.ocaml.org/packages/ocaml-base-compiler/

4.13.1 currently fails as follows:

===== UPDATE OPAM REPOSITORIES =====

<><> Updating package repositories ><><><><><><><><><><><><><><><><><><><><>  🐫
[__coq-platform.2021.11.0.patch_ocaml] no changes from file:///Users/kartik/Hub/platform/opam/opam-repository
[__coq-platform.2021.11.0.patch_coq-released] no changes from file:///Users/kartik/Hub/platform/opam/opam-coq-archive/released
[coq-released] no changes from https://coq.inria.fr/opam/released
[default] no changes from https://opam.ocaml.org
POL="$POL"'(allow network* (remote unix))'
===== INSTALL PREREQUISITES =====
[ERROR] Package conflict!
  * Missing dependency:
    - ppxlib = 0.15.0 → ocaml-migrate-parsetree < 2.0.0 → ocaml-variants = 4.08.0+beta2
    unmet availability conditions: '!(os = "macos" & arch = "arm64")'
  * Missing dependency:
    - ppxlib = 0.15.0 → ocaml-migrate-parsetree < 2.0.0 → ocaml-variants = 4.08.0+beta3
    unmet availability conditions: '!(os = "macos" & arch = "arm64")'

[WARNING] set was deprecated in version 2.1 of the opam CLI. Use opam var instead or set OPAMCLI environment variable to 2.0.
Added 'jobs: "4"' to field variables in switch __coq-platform.2021.11.0~8.14~2021.11
===== INSTALL OPAM PACKAGES (PARALLEL) =====
[ERROR] Package conflict!
  * Missing dependency:
    - ppxlib = 0.15.0 → ocaml-migrate-parsetree < 2.0.0 → ocaml-variants = 4.08.0+beta2
    unmet availability conditions: '!(os = "macos" & arch = "arm64")'
  * Missing dependency:
    - ppxlib = 0.15.0 → ocaml-migrate-parsetree < 2.0.0 → ocaml-variants = 4.08.0+beta3
    unmet availability conditions: '!(os = "macos" & arch = "arm64")'

No solution found, exiting

@k4rtik
Copy link
Contributor Author

k4rtik commented Nov 28, 2021

@MSoegtropIMC it seems this dependency problem is not specific to Apple Silicon, it may appear on all platforms. I see:

PACKAGES="${PACKAGES} PIN.ppxlib.0.15.0"            # coq-serapi requires this old version

in several package picks.

EDIT: never mind, unmet availability conditions: '!(os = "macos" & arch = "arm64")' must be important here. There is #13 discussing this dependency downgrade.

@MSoegtropIMC
Copy link
Collaborator

@k4rtik : thanks for testing! The 4.13.1 vs 4.13.2 is different if looks at the "ocaml" metapackage and the "ocaml-base-compiler" package. ocaml does have 4.13.2 but ocam-base-compiler doesn't. I can't say how relevant this is.

The ppxlib down version is required by serapi - it can't live yet with a newer version.

So in case of doubt I would drop serapi and keep elpi. If serapi is dropped, the restriction to ppxlib.0.15.0 can be dropped.

@ejgallego : FYI.

@k4rtik
Copy link
Contributor Author

k4rtik commented Nov 29, 2021

ocaml does have 4.13.2 but ocam-base-compiler doesn't. I can't say how relevant this is.

It might be a convenience package for testing before release as the latest on ocaml.org is also still 4.13.1 In any case, it's not installable using opam switch create:

$ opam switch create 4.13.2
[ERROR] No compiler matching `4.13.2' found, use `opam switch list-available' to see what is available, or use `--packages'
        to select packages explicitly.

I see at #186 (comment) that we are sticking to 4.10.2 for now.

@Blaisorblade
Copy link
Contributor

Blaisorblade commented Dec 2, 2021

Tried basic pick on current main (8568054)

$ git describe
2021.09.0-54-g8568054
$ time ./coq_platform_make.sh -extent=b -pick=8.13~2021.11 -parallel=p -jobs=16

real	3m37.415s
user	9m59.257s
sys	2m18.464s
$ system_profiler SPHardwareDataType
Hardware:

    Hardware Overview:

      Model Name: MacBook Pro
      Model Identifier: MacBookPro18,2
      Chip: Apple M1 Max
      Total Number of Cores: 10 (8 performance and 2 efficiency)
      Memory: 64 GB
      [snipped for privacy]

Time for the extended one next: time ./coq_platform_make.sh -extent=x -pick=8.13~2021.11 -parallel=p -jobs=16 -compcert=y -vst=y -switch=d. I should probably restart it after installing the prerequisites for good timings...

EDIT: getting up to the system prerequisites took

real	5m4.167s
user	4m50.197s
sys	1m35.480s

EDIT2: From a clean full build:

time ./coq_platform_make.sh -extent=x -pick=8.13~2021.11 -parallel=p -jobs=16 -compcert=y -vst=y -switch=d
[...]
real	25m57.207s
user	142m15.221s
sys	12m25.202s

@MSoegtropIMC
Copy link
Collaborator

@Blaisorblade : how much RAM to do you have?

@Blaisorblade
Copy link
Contributor

@MSoegtropIMC 64 GB

@k4rtik
Copy link
Contributor Author

k4rtik commented Dec 9, 2021

I am now testing on a different machine (note lower CPU count and more RAM):

❯ system_profiler SPHardwareDataType
Hardware:

    Hardware Overview:

      Model Name: MacBook Pro
      Model Identifier: MacBookPro18,3
      Chip: Apple M1 Pro
      Total Number of Cores: 8 (6 performance and 2 efficiency)
      Memory: 32 GB
[...]
❯ git describe
2021.09.0-54-g8568054
❯ time ./coq_platform_make.sh -extent=x -pick=8.14~2021.11 -parallel=p -jobs=16 -compcert=y -vst=y -switch=d
[...]
real	29:39.13
user	2:20:25.56
sys	12:40.06
~/Hub/platform main 29m 39s
❯ time ./coq_platform_make.sh -extent=x -pick=8.13~2021.11 -parallel=p -jobs=16 -compcert=y -vst=y -switch=d
[...]
real	31:03.97
user	2:22:58.13
sys	12:33.68
~/Hub/platform main 31m 4s
❯ time ./coq_platform_make.sh -extent=x -pick=8.12 -parallel=p -jobs=16 -compcert=y -vst=y -switch=d
[...]
real	21:59.31
user	1:12:23.50
sys	7:13.60
~/Hub/platform main 21m 59s

It certainly takes longer, but my system doesn't run out of memory anymore with 16 parallel jobs (I had other tasks such as a web browser and even a Zoom meeting running alongside these tests).

@k4rtik
Copy link
Contributor Author

k4rtik commented Jan 13, 2022

And here's the output from my final machine (note higher CPU count and same RAM):

❯ system_profiler -detailLevel mini SPHardwareDataType
Hardware:

    Hardware Overview:

      Model Name: MacBook Pro
      Model Identifier: MacBookPro18,3
      Chip: Apple M1 Pro
      Total Number of Cores: 10 (8 performance and 2 efficiency)
      Memory: 32 GB
      System Firmware Version: 7429.61.2
      OS Loader Version: 7429.61.2

❯ git describe
2021.09.0-54-g8568054
❯ time ./coq_platform_make.sh -extent=x -pick=8.14~2021.11 -parallel=p -jobs=16 -compcert=y -vst=y -switch=d
[...]
real	25:42.57
user	2:16:23.56
sys	13:23.00
❯ time ./coq_platform_make.sh -extent=x -pick=8.13~2021.11 -parallel=p -jobs=16 -compcert=y -vst=y -switch=d
[...]
real	25:36.52
user	2:21:38.58
sys	12:46.15
❯ time ./coq_platform_make.sh -extent=x -pick=8.12 -parallel=p -jobs=16 -compcert=y -vst=y -switch=d
[...]
real	19:21.28
user	1:12:11.36
sys	6:42.23

Clear improvement of 3 to 5 minutes with two extra cores.

@Blaisorblade
Copy link
Contributor

Cool! Haven't tried 8.12 but the other times seem to match my M1 Max 64 GB, which will help people save quite a bit.

@k4rtik
Copy link
Contributor Author

k4rtik commented Jan 13, 2022

Right, I feel like it means 32GB will be sufficient for most people's needs (while 16GB was too constraining).

@k4rtik
Copy link
Contributor Author

k4rtik commented Jan 23, 2022

Hi @MSoegtropIMC I tried installing __coq-platform.2022.01.0~8.14~2022.01 and __coq-platform.2022.01.0~8.15~preview1 last night with your commit 7cf8bc1 (prep3) and had no issues.

Do you think we can close this issue now?

PS: let me know if you'd like me to test any other config of the platform script options.

@MSoegtropIMC
Copy link
Collaborator

Thanks for your continued test efforts!

I don't think the other configurations make any difference in arm vs intel code, so I will close this issue.

@Zimmi48
Copy link
Member

Zimmi48 commented Jun 17, 2022

There is now a GitHub roadmap item (with no ETA) about M1 support: github/roadmap#528

@MSoegtropIMC
Copy link
Collaborator

I don't expect this to be realized any time soon - afaik there is no M1 HW which is suitable for large data centers. A web search shows that those who offer M1 servers base this on Mac Mini. For small applications (like a Coq CI) a bunch of MacMinis in a rack is fine, but I can't quite imagine that Github will do this.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

4 participants