local development on apple silicon

Stream: lean4

[Matthew Ballard]

Right now I am relying GitHub CI to test things which is not ideal. My initial experiments with building Lean locally on my M1 machine have been mixed. For example, a few number of tests from a clone of the master on leanprover/lean4 fail. Is this to be expected?

Does anyone have any experience with local development on apple silicon? Thanks.

[Eric Rodriguez]

which ones? Can try to see if I can replicate. I just build with lake build <file I care about> and let CI deal with the tests and stuff later

[Matthew Ballard]

https://leanprover.github.io/lean4/doc/make/index.html

[Matthew Ballard]

https://leanprover.github.io/lean4/doc/dev/testing.html

[Matthew Ballard]

I think I have working builds from make but the tests seem off

[Eric Rodriguez]

oh I see this is about Lean4 itself, as opposed to mathlib . I will run this stuff and see if I get any issues

[Eric Rodriguez]

I get a bunch of "no such file" after leanshared:

[100%] Built target leanshared
[    ] Building /Users/ericr/repos/lean4/build/release/stage1/bin/lean
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: /Users/ericr/repos/lean4/build/release/stage1/temp/Leanc.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../../build/release/stage1/lib/temp/Lake/Util/Family.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../../build/release/stage1/lib/temp/Lake/Util/StoreInsts.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../../build/release/stage1/lib/temp/Lake/Util/Opaque.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../../build/release/stage1/lib/temp/Lake/Util/DRBMap.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../../build/release/stage1/lib/temp/Lake/Util/MainM.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../../build/release/stage1/lib/temp/Lake/Util/Binder.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../../build/release/stage1/lib/temp/Lake/Util/Proc.depend: No such file or directory

and so on

[Eric Rodriguez]

happens twice, actually, this one was earlier:

[    ] Building Init.lean
[    ] Building ../build/release/stage1/lib/temp/Init/Control.c
[    ] Building ../build/release/stage1/lib/temp/Init.c
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../build/release/stage1/lib/temp/Lean/Compiler.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../build/release/stage1/lib/temp/Lean/Class.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../build/release/stage1/lib/temp/Lean/ParserCompiler/Attribute.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../build/release/stage1/lib/temp/Lean/DeclarationRange.depend: No such file or directory

and so on

[Eric Rodriguez]

think it started at 2% but I didn't spot it:

[  2%] Building CXX object library/compiler/CMakeFiles/compiler.dir/init_module.cpp.o
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../build/release/stage1/lib/temp/Init/Data.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../build/release/stage1/lib/temp/Init/Core.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../build/release/stage1/lib/temp/Init/Hints.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../build/release/stage1/lib/temp/Init/Conv.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../build/release/stage1/lib/temp/Init/ShareCommon.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../build/release/stage1/lib/temp/Init/NotationExtra.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../build/release/stage1/lib/temp/Init/SimpLemmas.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../build/release/stage1/lib/temp/Init/Util.depend: No such file or directory
/Users/ericr/repos/lean4/build/release/stage1/bin/../share/lean/lean.mk:110: ../build/release/stage1/lib/temp/Init/Control.depend: No such file or directory

[Eric Rodriguez]

and I get 73 failed tests:

Tests failed

    1519 - leancomptest_534.lean (Failed)
    1520 - leancomptest_StackOverflow.lean (Failed)
    1521 - leancomptest_StackOverflowTask.lean (Failed)
    1522 - leancomptest_append.lean (Failed)
    1523 - leancomptest_array.lean (Failed)
    1524 - leancomptest_arrayMk.lean (Failed)
    1525 - leancomptest_array_test.lean (Failed)
    1526 - leancomptest_array_test2.lean (Failed)
    1527 - leancomptest_bigctor.lean (Failed)
    1528 - leancomptest_bytearray_bug.lean (Failed)
    1529 - leancomptest_closure_bug1.lean (Failed)
    1530 - leancomptest_closure_bug2.lean (Failed)
    1531 - leancomptest_closure_bug3.lean (Failed)
    1532 - leancomptest_closure_bug4.lean (Failed)
    1533 - leancomptest_closure_bug5.lean (Failed)
    1534 - leancomptest_closure_bug6.lean (Failed)
    1535 - leancomptest_closure_bug7.lean (Failed)
    1536 - leancomptest_closure_bug8.lean (Failed)
    1537 - leancomptest_escape.lean (Failed)
    1538 - leancomptest_expr.lean (Failed)
    1539 - leancomptest_extractClosedMutualBlock.lean (Failed)
    1540 - leancomptest_float.lean (Failed)
    1541 - leancomptest_float_cases_bug.lean (Failed)
    1542 - leancomptest_init.lean (Failed)
    1543 - leancomptest_initUnboxed.lean (Failed)
    1544 - leancomptest_lazylist.lean (Failed)
    1545 - leancomptest_link_lake.lean (Failed)
    1546 - leancomptest_map_big.lean (Failed)
    1547 - leancomptest_overflow1.lean (Failed)
    1548 - leancomptest_overflow2.lean (Failed)
    1549 - leancomptest_overflow3.lean (Failed)
    1550 - leancomptest_partial.lean (Failed)
    1551 - leancomptest_phashmap.lean (Failed)
    1552 - leancomptest_phashmap2.lean (Failed)
    1553 - leancomptest_phashmap3.lean (Failed)
    1554 - leancomptest_print_error.lean (Failed)
    1555 - leancomptest_qsortBadLt.lean (Failed)
    1556 - leancomptest_rbmap_library.lean (Failed)
    1557 - leancomptest_reusebug.lean (Failed)
    1558 - leancomptest_str.lean (Failed)
    1559 - leancomptest_strictAndOr.lean (Failed)
    1560 - leancomptest_strictOrSimp.lean (Failed)
    1561 - leancomptest_t1.lean (Failed)
    1562 - leancomptest_t2.lean (Failed)
    1563 - leancomptest_t4.lean (Failed)
    1564 - leancomptest_thunk.lean (Failed)
    1565 - leancomptest_uint_fold.lean (Failed)
    1566 - leancomptest_unreachable.lean (Failed)
    1567 - leancomptest_uset.lean (Failed)
    1569 - leancomptest_doc_example (Failed)
    1613 - leanbenchtest_binarytrees.lean (Failed)
    1614 - leanbenchtest_const_fold.lean (Failed)
    1615 - leanbenchtest_dag_hassorry_issue.lean (Failed)
    1616 - leanbenchtest_deriv.lean (Failed)
    1617 - leanbenchtest_liasolver.lean (Failed)
    1618 - leanbenchtest_qsort.lean (Failed)
    1619 - leanbenchtest_rbmap.lean (Failed)
    1620 - leanbenchtest_rbmap_checkpoint.lean (Failed)
    1621 - leanbenchtest_unionfind.lean (Failed)
    1622 - leanplugintest_SnakeLinter.lean (Failed)
    1629 - leanpkgtest_user_attr_app (Failed)
    1700 - leanlaketest_deps (Failed)
    1701 - leanlaketest_ffi (Failed)
    1702 - leanlaketest_hello (Failed)
    1703 - leanlaketest_init (Failed)
    1704 - leanlaketest_precompile (Failed)
    1705 - leanlaketest_reverse-ffi (Failed)
    1707 - leanlaketest_targets (Failed)
    1710 - leanlaketest_44 (Failed)
    1712 - leanlaketest_62 (Failed)
    1713 - leanlaketest_75 (Failed)
    1714 - leanlaketest_buildArgs (Failed)
    1715 - leanlaketest_clone (Failed)

[Matthew Ballard]

That failed test list looks similar

[Matthew Ballard]

I think I get those others too. They whip by fast

[Henrik Böving]

Can you run one of the comp tests using the test-single.sh script and show us the output?

[Matthew Ballard]

I ran the script itself but should I point it at something?

[Matthew Ballard]

Ok I figured out what I should

ld64.lld: warning: directory not found for option -L/Applications/Xcode_14.2.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX13.1.sdk/usr/lib

[Matthew Ballard]

I already had a SnakeLinter.lean.c in there. Deleting it and re-running produces SnakeLinter.so and SnakeLinter.produced.out

[Matthew Ballard]

For a compiler test

running C program...
rm: ./str.lean.out: No such file or directory
ld64.lld: warning: directory not found for option -L/Applications/Xcode_14.2.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX13.1.sdk/usr/lib
../common.sh: line 42: 25062 Abort trap: 6           LEAN_BACKTRACE=0 "$@" 2>&1
     25063 Done                    | perl -pe 's/(\?(\w|_\w+))\.[0-9]+/\1/g' > "$f.produced.out"
Unexpected return code 134 executing './str.lean.out'; expected 0. Output:
dyld[25062]: Library not loaded: @rpath/libc++.1.dylib
  Referenced from: <4C4C4451-5555-3144-A1CF-E3D6AFA1FC9A> /Users/matt/GitHub/lean4/tests/compiler/str.lean.out
  Reason: no LC_RPATH's found

so it looks like rpath is not resolving correctly again

[Matthew Ballard]

And I've already forgotten what Sebastian did lol

[Sebastian Ullrich]

That's fine, so have I

[Matthew Ballard]

https://github.com/leanprover/lean4/pull/2356/commits/23631eb57d0742195c627f2b08d8ebb76031a3a4

[Matthew Ballard]

install_name_tool -id /usr/lib/$lib stage1/lib/libc/$lib

[Matthew Ballard]

For the prepare-llvm.macos.sh

[Sebastian Ullrich]

I'm starting to think this is a general LLVM bug/Sonoma incompatibility and I simply worked around it for the release job

[Matthew Ballard]

@Eric Rodriguez what version of MacOS are you on?

[Eric Rodriguez]

13.4.1 (c) (22F770820d)

[Matthew Ballard]

14.0 Beta (23A5301h) for me

[Matthew Ballard]

So it's not just Sonoma

[Sebastian Ullrich]

@Eric Rodriguez And you get the same test output?

[Eric Rodriguez]

what exact script should I run?

[Matthew Ballard]

I ran ./test_single.sh str.lean from ./tests/compiler

[Eric Rodriguez]

as in cd tests/compiler? I didn't get any good output, for some reason my elan default lean is triggering there, and sadly that's some lean3

[Matthew Ballard]

I've commandeered my wife's laptop

[Matthew Ballard]

That seems to work, MacOS 13.4.1 (c) also

[Matthew Ballard]

I even nuked .elan and did it from a fresh copy of the repo

[Eric Rodriguez]

does this mean my elan is borked and I should reinstall it?

[Matthew Ballard]

Not sure. What is the worst that can happen?

[Matthew Ballard]

I am swallowed in ld64.lld warnings about having too new versions of things (lesser issue)

[Scott Morrison]

I get these warning too, but for now am on rather old hardware/OS version so haven't been complaining about it hoping it magically goes away soon. :-)

[Matthew Ballard]

Sebastian Ullrich said:

I'm starting to think this is a general LLVM bug/Sonoma incompatibility and I simply worked around it for the release job

This still seems to be present in the released version.

[Scott Morrison]

These linker warnings will disappear after lean4#2598 is merged, so probably v4.3.0-rc1.

[Matthew Ballard]

I can’t build Lean on Sonoma.

[Sebastian Ullrich]

I thought you were able to get up to the test suite?

[Julian Berman]

(It definitely builds here on Sonoma. Though I have never tried to run the test suite.)

[Matthew Ballard]

It looked like it built but using the toolchain with an override was wonky. The same tests fail.

Good to know this might be user error! Retrying again on a clean clone.

[Matthew Ballard]

Building the first 1300 files in mathlib with the toolchain is ok. I will test out the infoview once I has some things from mathlib to poke at.

Here are my

failed tests

The following tests FAILED:
    1524 - leancomptest_534.lean (Failed)
    1525 - leancomptest_StackOverflow.lean (Failed)
    1526 - leancomptest_StackOverflowTask.lean (Failed)
    1527 - leancomptest_append.lean (Failed)
    1528 - leancomptest_array.lean (Failed)
    1529 - leancomptest_arrayMk.lean (Failed)
    1530 - leancomptest_array_test.lean (Failed)
    1531 - leancomptest_array_test2.lean (Failed)
    1532 - leancomptest_bigctor.lean (Failed)
    1533 - leancomptest_bytearray_bug.lean (Failed)
    1534 - leancomptest_closure_bug1.lean (Failed)
    1535 - leancomptest_closure_bug2.lean (Failed)
    1536 - leancomptest_closure_bug3.lean (Failed)
    1537 - leancomptest_closure_bug4.lean (Failed)
    1538 - leancomptest_closure_bug5.lean (Failed)
    1539 - leancomptest_closure_bug6.lean (Failed)
    1540 - leancomptest_closure_bug7.lean (Failed)
    1541 - leancomptest_closure_bug8.lean (Failed)
    1542 - leancomptest_escape.lean (Failed)
    1543 - leancomptest_expr.lean (Failed)
    1544 - leancomptest_extractClosedMutualBlock.lean (Failed)
    1545 - leancomptest_float.lean (Failed)
    1546 - leancomptest_float_cases_bug.lean (Failed)
    1547 - leancomptest_init.lean (Failed)
    1548 - leancomptest_initUnboxed.lean (Failed)
    1549 - leancomptest_lazylist.lean (Failed)
    1550 - leancomptest_link_lake.lean (Failed)
    1551 - leancomptest_map_big.lean (Failed)
    1552 - leancomptest_overflow1.lean (Failed)
    1553 - leancomptest_overflow2.lean (Failed)
    1554 - leancomptest_overflow3.lean (Failed)
    1555 - leancomptest_partial.lean (Failed)
    1556 - leancomptest_phashmap.lean (Failed)
    1557 - leancomptest_phashmap2.lean (Failed)
    1558 - leancomptest_phashmap3.lean (Failed)
    1559 - leancomptest_print_error.lean (Failed)
    1560 - leancomptest_qsortBadLt.lean (Failed)
    1561 - leancomptest_rbmap_library.lean (Failed)
    1562 - leancomptest_reusebug.lean (Failed)
    1563 - leancomptest_str.lean (Failed)
    1564 - leancomptest_strictAndOr.lean (Failed)
    1565 - leancomptest_strictOrSimp.lean (Failed)
    1566 - leancomptest_t1.lean (Failed)
    1567 - leancomptest_t2.lean (Failed)
    1568 - leancomptest_t4.lean (Failed)
    1569 - leancomptest_thunk.lean (Failed)
    1570 - leancomptest_trie.lean (Failed)
    1571 - leancomptest_uint_fold.lean (Failed)
    1572 - leancomptest_unreachable.lean (Failed)
    1573 - leancomptest_uset.lean (Failed)
    1575 - leancomptest_doc_example (Failed)
    1620 - leanbenchtest_binarytrees.lean (Failed)
    1621 - leanbenchtest_const_fold.lean (Failed)
    1622 - leanbenchtest_dag_hassorry_issue.lean (Failed)
    1623 - leanbenchtest_deriv.lean (Failed)
    1624 - leanbenchtest_liasolver.lean (Failed)
    1625 - leanbenchtest_qsort.lean (Failed)
    1626 - leanbenchtest_rbmap.lean (Failed)
    1627 - leanbenchtest_rbmap_checkpoint.lean (Failed)
    1628 - leanbenchtest_unionfind.lean (Failed)
    1629 - leanplugintest_SnakeLinter.lean (Failed)
    1633 - leanpkgtest_frontend (Failed)
    1637 - leanpkgtest_user_attr_app (Failed)
    1708 - leanlaketest_deps (Failed)
    1709 - leanlaketest_ffi (Failed)
    1710 - leanlaketest_hello (Failed)
    1711 - leanlaketest_precompile (Failed)
    1712 - leanlaketest_reverse-ffi (Failed)
    1714 - leanlaketest_targets (Failed)
    1715 - leanlaketest_buildArgs (Failed)
    1716 - leanlaketest_clone (Failed)
    1719 - leanlaketest_init (Failed)
    1723 - leanlaketest_old (Failed)
    1726 - leanlaketest_rebuild (Failed)

[Matthew Ballard]

Sample from the LastTest.log

rm: ./unreachable.lean.out: No such file or directory
ld: library 'c++' not found
clang: error: linker command failed with exit code 1 (use -v to see invocation)
Failed to compile C file unreachable.lean.c

[Matthew Ballard]

Reran with lean4#2598 in master to the same effect

[Schrodinger ZHU Yifan]

Allow me to mention: https://github.blog/changelog/2023-10-02-github-actions-apple-silicon-m1-macos-runners-are-now-available-in-public-beta/ GitHub Actions: Apple silicon (M1) macOS runners are now available in public beta!