Racket cannot find libidris2_support on Mac M1

[burcatowlet]

I'm building idris2 on a Mac M1 with Racket. When I run make bootstrap-racket, it builds idris2, but then it fails at

/Users/user1/Documents/Idris2-0.3.0/bootstrap/bin/idris2 --build tests.ipkg
1/2: Building Lib (Lib.idr)
2/2: Building Main (Main.idr)
make -C libs/prelude IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/Users/user1/Documents/Idris2-0.3.0/libs/prelude/build/ttc:/Users/user1/Documents/Idris2-0.3.0/libs/base/build/ttc:/Users/user1/Documents/Idris2-0.3.0/libs/contrib/build/ttc:/Users/user1/Documents/Idris2-0.3.0/libs/network/build/ttc"
../../build/exec/idris2 --build prelude.ipkg
ffi-lib: could not load foreign library
  path: libidris2_support.dylib
  system error: dlopen(libidris2_support.dylib, 10): image not found
  context...:
   .../ffi/unsafe.rkt:131:0: get-ffi-lib
   body of '#%mzc:idris2
make[2]: *** [all] Error 1
make[1]: *** [prelude] Error 2
make: *** [bootstrap-racket-build] Error 2

The idris2 executable under /Users/user1/Documents/Idris2-0.3.0/bootstrap/bin/idris2 works though.

[gallais]

Is this #840?

[burcatowlet]

It looks very similar but I don't understand how to resolve the problem.

[gallais]

Can you try RACKET=racket make bootstrap-racket?

I have been trying to fix the /usr/bin/env scenario to no avail so far.

[burcatowlet]

That doesn't help. Same error. But the file exists, see below:

MacBook-Air-M1 Idris2-0.3.0 % find . -name libidris2_support.dylib
./bootstrap/bin/idris2_app/libidris2_support.dylib
./bootstrap/idris2-0.3.0/lib/libidris2_support.dylib
./bootstrap/idris2_app/libidris2_support.dylib
./bootstrap/lib/libidris2_support.dylib
./support/c/libidris2_support.dylib

[gallais]

Yeah I expect the file is there. But for some reason MacOS is ignoring
the env variables telling it where to look for this lib.

I don't see how to fix this at the moment so you may want to build via
chez instead to get idris2 up and running.

[abailly]

Could it be related to this: https://support.apple.com/en-us/HT204899 ? Googling lead me to this issue nteract/nteract#1523 which seems to expose a similar issue.
Alternatively, digging into racket docs showed this: https://download.racket-lang.org/docs/5.1/html/foreign/Loading_Foreign_Libraries.html I wonder if racket is looking at those environment variables at all.

[TOTBWF]

This happens because the OSX dynamic library loader has some... bizzare behavior with regards to environment variables. Namely, it has a habit of ignoring them all! As a workaround, move the generated dylib into ~/lib/, then re-run the build.

The proper fix is to patch the Mach-O headers of the dylib using install-name-tool. I can take a look at doing this over the weekend.

For reference, here is the code for dyld:
https://opensource.apple.com/source/dyld/dyld-519.2.1/src/dyld.cpp.auto.html

Take a look at sLibraryFallbackPaths to see why this crazy behavior happens

[burcatowlet]

Moving the dylib into ~/lib. worked. Two tests are failing with the same error though:

ffi-lib: could not load foreign library
  path: libidris2_support.dylib
  system error: dlopen(libidris2_support.dylib, 10): image not found
  context...:
   /Applications/Racket v8.0.0.1/collects/ffi/unsafe.rkt:131:0: get-ffi-lib
   body of "/Users/user1/Documents/Idris2-0.3.0/tests/idris2/perf006/build/exec/_tmpracket_app/_tmpracket.rkt"
idris2/perf006: FAILURE

and

ffi-lib: could not load foreign library
  path: libidris2_support.dylib
  system error: dlopen(libidris2_support.dylib, 10): image not found
  context...:
   /Applications/Racket v8.0.0.1/collects/ffi/unsafe.rkt:131:0: get-ffi-lib
   body of "/Users/user1/Documents/Idris2-0.3.0/tests/idris2/evaluator004/build/exec/_tmpracket_app/_tmpracket.rkt"
idris2/evaluator004: FAILURE
Expected:
1/1: Building Issue735 (Issue735.idr)
Main> 0
Main> 3
Main> 0
Main> 9
Main> 
Bye for now!
3
8
0

Given:
1/1: Building Issue735 (Issue735.idr)
Main> 0
Main> 3
Main> 0
Main> 9
Main> 
Bye for now!

[gallais]

Two tests are failing with the same error though:

Only these 2? What about make test only=basic048?
(All 3 use --exec main --cg as options which gets idris2 to compile & run the program)

[burcatowlet]

I missed one, sorry:

• idris2/basic048: FAILURE
• idris2/evaluator004: FAILURE
• idris2/perf006: FAILURE

[gallais]

I did make some progress by putting the library in ~/lib/ on my mac-racket branch.

But then I still got quite a few failures in make test:
https://github.com/gallais/Idris2/runs/1926777245

I am starting to think that the ideal solution may be to generate a
static binary in these circumstances...

[ceberly]

I made some progress on this: #1219 (comment)

However, make test does not work, it fails with the missing lib_idris2.so error. However Idris2 itself runs.

[codimension]

This happens because the OSX dynamic library loader has some... bizzare behavior with regards to environment variables. Namely, it has a habit of ignoring them all! As a workaround, move the generated dylib into ~/lib/, then re-run the build.

I actually think it's a different thing. The issue is that the produced executable is a shell script which calls the generated binary.
E.g. if I compile a program called 'hello', I will get a shell script called 'hello' and a subdirectory 'hello_app' containing a binary 'hello'. The shell script sets LD_LIBRARY_PATH and then calls the executable.

The problem is that MacOS System Integrity Protection (SIP) prevents child processes from inheriting environment variables starting with LD_ or DYLD_, so the hello binary will never see the path to the support library.
I can get the binary to run as long as LD_LIBRARY_PATH is pointing to the right library.

Idris currently has a sort of 'portable' installation, i.e. all installed files are kept in the same location.
It seems that Apple would ideally have you install shared libraries via a 'Framework' (which at its simplest is just a folder with some headers and libraries). E.g. if I look at the dylibs loaded by my system installation of python, I can see there is a 'Python.framework' installed in /System/Library/Frameworks.
A simpler solution might be just to install in /usr/local/lib though (or even just to create a symlink there to the library location).

The Framework solution feels like what a production language would do, Idris feels more experimental at this stage. I would say that past the experimental stage though, you would want some way of installing the libraries required for running Idris programs without modifying LD_LIBRARY_PATH. I don't think many apps would be distributed that way.

[andrevidela]

I just tried to install idris2 on my M1 laptop and I could not reproduce the issue. Everything worked fine, except for one thing. gmp couldn't be found so I had to run the bootstrapping with

CFLAGS=-I`brew --prefix gmp`/include LDFLAGS=-L`brew --prefix gmp`/lib make bootstrap-racket

Since we haven't heard of this since August I think we can close it for now and reopen if someone else can reproduce the issue again

[kevzettler]

I am having this same issue installing with Idris2-0.5.1

kevzettler@Kevs-MacBook-Pro-3 Idris2-0.5.1 % racket -v
Welcome to Racket v8.4 [cs].
kevzettler@Kevs-MacBook-Pro-3 Idris2-0.5.1 % uname -a
Darwin Kevs-MacBook-Pro-3.local 21.2.0 Darwin Kernel Version 21.2.0: Sun Nov 28 20:29:10 PST 2021; root:xnu-8019.61.5~1/RELEASE_ARM64_T8101 x86_64

kevzettler@Kevs-MacBook-Pro-3 Idris2-0.5.1 % make bootstrap-racket
make[1]: Nothing to be done for `all'.
make[1]: Nothing to be done for `all'.
make[1]: Nothing to be done for `all'.
mkdir -p bootstrap-build/idris2_app
cp support/c/libidris2_support.dylib bootstrap-build/idris2_app/
sed 's|__PREFIX__|/Users/kevzettler/code/Idris2-0.5.1/bootstrap-build|g' \
        bootstrap/idris2_app/idris2.rkt \
        > bootstrap-build/idris2_app/idris2-boot.rkt
/bin/sh ./bootstrap-stage1-racket.sh
Bootstrapping IDRIS2_VERSION=0.5.1
Building idris2-boot from idris2-boot.rkt
IDRIS2_CG="racket" /bin/sh ./bootstrap-stage2.sh
/Users/kevzettler/code/Idris2-0.5.1/bootstrap-build
make -C libs/prelude IDRIS2=/Users/kevzettler/code/Idris2-0.5.1/build/exec/idris2 IDRIS2_INC_CGS=racket IDRIS2_PATH="/Users/kevzettler/code/Idris2-0.5.1/libs/prelude/build/ttc:/Users/kevzettler/code/Idris2-0.5.1/libs/base/build/ttc:/Users/kevzettler/code/Idris2-0.5.1/libs/contrib/build/ttc:/Users/kevzettler/code/Idris2-0.5.1/libs/network/build/ttc:/Users/kevzettler/code/Idris2-0.5.1/libs/test/build/ttc"
/Users/kevzettler/code/Idris2-0.5.1/build/exec/idris2 --build prelude.ipkg
ffi-lib: could not load foreign library
  path: libidris2_support.dylib
  system error: dlopen(libidris2_support.dylib, 0x000A): tried: 'libidris2_support.dylib' (no such file), '/usr/local/lib/libidris2_support.dylib' (no such file), '/usr/lib/libidris2_support.dylib' (no such file), '/Users/kevzettler/code/Idris2-0.5.1/libs/prelude/libidris2_support.dylib' (no such file), '/usr/local/lib/libidris2_support.dylib' (no such file), '/usr/lib/libidris2_support.dylib' (no such file)
  context...:
   .../ffi/unsafe.rkt:131:0: get-ffi-lib
   body of '#%mzc:idris2-boot
make[2]: *** [all] Error 1
make[1]: *** [prelude] Error 2
make: *** [bootstrap-racket] Error 2

[gallais]

Can you try main instead of 0.5.1?

[kevzettler]

@gallais

here is output from commit 98b1062

I had to add the gmp flags mentioned above

kevzettler@Kevs-MacBook-Pro-3 Idris2 % git log -1
commit 98b10627728df3c5c49565cd5894f0df132ad201 (HEAD -> main, origin/main, origin/HEAD)
Author: G. Allais <[email protected]>
Date:   Fri Apr 15 20:39:46 2022 +0100

    [ fix ] :printdef support for P(D)Pair & Equal (#2416)
kevzettler@Kevs-MacBook-Pro-3 Idris2 % CFLAGS=-I`brew --prefix gmp`/include LDFLAGS=-L`brew --prefix gmp`/lib make bootstrap-racket
make[1]: Nothing to be done for `all'.
make[1]: Nothing to be done for `all'.
make[1]: Nothing to be done for `all'.
mkdir -p bootstrap-build/idris2_app
cp support/c/libidris2_support.dylib bootstrap-build/idris2_app/
sed 's|__PREFIX__|/Users/kevzettler/code/Idris2/bootstrap-build|g' \
		bootstrap/idris2_app/idris2.rkt \
		> bootstrap-build/idris2_app/idris2-boot.rkt
/bin/sh ./bootstrap-stage1-racket.sh
Bootstrapping IDRIS2_VERSION=0.5.1
Building idris2-boot from idris2-boot.rkt
IDRIS2_CG="racket" /bin/sh ./bootstrap-stage2.sh
/Users/kevzettler/code/Idris2/bootstrap-build
make -C libs/prelude IDRIS2=/Users/kevzettler/code/Idris2/build/exec/idris2 IDRIS2_INC_CGS=racket IDRIS2_PATH="/Users/kevzettler/code/Idris2/libs/prelude/build/ttc:/Users/kevzettler/code/Idris2/libs/base/build/ttc:/Users/kevzettler/code/Idris2/libs/contrib/build/ttc:/Users/kevzettler/code/Idris2/libs/network/build/ttc:/Users/kevzettler/code/Idris2/libs/test/build/ttc:/Users/kevzettler/code/Idris2/libs/linear/build/ttc"
/Users/kevzettler/code/Idris2/build/exec/idris2 --build prelude.ipkg
ffi-lib: could not load foreign library
  path: libidris2_support.dylib
  system error: dlopen(libidris2_support.dylib, 0x000A): tried: '/Users/kevzettler/code/Idris2/build/exec/idris2_app/libidris2_support.dylib' (mach-o file, but is an incompatible architecture (have 'x86_64', need 'arm64e')), '/libidris2_support.dylib' (no such file), 'libidris2_support.dylib' (no such file), '/usr/local/lib/libidris2_support.dylib' (no such file), '/usr/lib/libidris2_support.dylib' (no such file), '/Users/kevzettler/code/Idris2/build/exec/idris2_app/libidris2_support.dylib' (mach-o file, but is an incompatible architecture (have 'x86_64', need 'arm64e')), '/libidris2_support.dylib' (no such file), '/Users/kevzettler/code/Idris2/libs/prelude/libidris2_support.dylib' (no such file), '/usr/local/lib/libidris2_support.dylib' (no such file), '/usr/lib/libidris2_support.dylib' (no such file)
  context...:
   .../ffi/unsafe.rkt:131:0: get-ffi-lib
   body of '#%mzc:idris2-boot
make[2]: *** [all] Error 1
make[1]: *** [prelude] Error 2
make: *** [bootstrap-racket] Error 2

[gallais]

(mach-o file, but is an incompatible architecture (have 'x86_64', need 'arm64e'))

This seems to be the issue

[Syzygies]

I have updated my guide for Apple silicon:

Building Idris2 for Apple silicon as of August 2022

I encountered a slew of related bugs involving libidris2_support.dylib including this one. First, yes, one needs to build the correct architecture. This can be checked with the file command.

Second, idris2 is a script, that fails to set the current directory. This leads to undefined behavior, as the dylib search path includes the current directory, which in the developer's case is likely to have a copy of libidris2_support.dylib. I unpredictably encountered this issue, as I had already sprayed copies of libidris2_support.dylib everywhere to get idris2 to build.

The fix is simple; have the idris2 script change directories to the executable before calling it, as I do in my notes. One of the several identical copies of libidris2_support.dylib is sitting next to the executable.

[ncihnegn]

For homebrew/cask Racket:

Welcome to Racket v8.9 [cs].
> (require setup/dirs)
> (get-lib-search-dirs)
'(#<path:~/Library/Racket/8.9/lib>
  #<path:/Applications/Racket v8.9/lib>)

So the dylib needs to be in ~/Library/Racket/8.9/lib.