search

idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.49k stars 373 forks source link

Racket cannot find libidris2_support on Mac M1 #1032

Open burcatowlet opened 3 years ago

burcatowlet commented 3 years ago

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 commented 3 years ago

Is this #840?

burcatowlet commented 3 years ago

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

gallais commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

Could it be related to this: https://support.apple.com/en-us/HT204899 ? Googling lead me to this issue https://github.com/nteract/nteract/issues/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 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

I missed one, sorry:

gallais commented 3 years ago

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 commented 3 years ago

I made some progress on this: https://github.com/idris-lang/Idris2/issues/1219#issuecomment-804436683

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

codimension commented 3 years ago

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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

Can you try main instead of 0.5.1?

kevzettler commented 2 years ago

@gallais

here is output from commit 98b10627728df3c5c49565cd5894f0df132ad201

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 <guillaume.allais@ens-lyon.org>
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 commented 2 years ago

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

This seems to be the issue

Syzygies commented 2 years ago

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 commented 1 year ago

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.