Idris2: compiled executables are broken on Mac

[srid]

Describe the bug

On M1 Mac with Idris2 installed via rosetta packages, the compiler generated executables cannot be executed:

[nix-shell:~/code/idris-template]$ idris2 hello.idr -x main
Exception: (while loading libidris2_support.dylib) dlopen(libidris2_support.dylib, 0x0002): tried: '/nix/store/lxfslviarb3h6a2fa9ndwcv37j4dmjls-swift-corefoundation/Library/Frameworks/libidris2_support.dylib' (no such file), '/nix/store/lxfslviarb3h6a2fa9ndwcv37j4dmjls-swift-corefoundation/Library/Frameworks/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/srid/code/idris-template/libidris2_support.dylib' (no such file), '/usr/local/lib/libidris2_support.dylib' (no such file), '/usr/lib/libidris2_support.dylib' (no such file)

also,

[nix-shell:~/code/idris-template]$ idris2 hello.idr -o hello

[nix-shell:~/code/idris-template]$ ./build/exec/hello
Exception: (while loading libidris2_support.dylib) dlopen(libidris2_support.dylib, 0x0002): tried: '/nix/store/lxfslviarb3h6a2fa9ndwcv37j4dmjls-swift-corefoundation/Library/Frameworks/libidris2_support.dylib' (no such file), '/nix/store/lxfslviarb3h6a2fa9ndwcv37j4dmjls-swift-corefoundation/Library/Frameworks/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/srid/code/idris-template/libidris2_support.dylib' (no such file), '/usr/local/lib/libidris2_support.dylib' (no such file), '/usr/lib/libidris2_support.dylib' (no such file)

[nix-shell:~/code/idris-template]$ 

Steps To Reproduce

On a M1 Mac, run nix develop -c make in https://github.com/srid/idris-template/tree/c76e6086012fc1d48b25ddb484f0fa23fe429c57

Notify maintainers

@fabianhjr @wchresta

Metadata

❯ nix-shell -p nix-info --run "nix-info -m"
 - system: `"aarch64-darwin"`
 - host os: `Darwin 21.2.0, macOS 12.1`
 - multi-user?: `yes`
 - sandbox: `no`
 - version: `nix-env (Nix) 2.4`
 - channels(srid): `"darwin"`
 - channels(root): `"nixpkgs-21.11pre333180.98747f27ecf"`
 - nixpkgs: `/nix/var/nix/profiles/per-user/root/channels/nixpkgs`

[srid]

[nix-shell:~/code/idris-template]$ DYLD_LIBRARY_PATH=/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/lib ./build/exec/hello_app/hello.so
Hello world!

[nix-shell:~/code/idris-template]$

[fabianhjr]

Sorry, I cannot help with this; I have neither Apple hardware (nor aarch64/armv8a) nor macOS expertise.

[wchresta]

This should have been fixed with #150521 - can you check if this is the case?

[srid]

I updated Nixpkgs (7ac6901f5e3038d59d3e2576af445fe418291dd8). But unfortunately the issue still exists.

air:idris-template srid$ idris2 hello.idr -x main 
Warning: compiling hole Main.what
Exception: (while loading libidris2_support.dylib) dlopen(libidris2_support.dylib, 0x0002): tried: '/nix/store/lxfslviarb3h6a2fa9ndwcv37j4dmjls-swift-corefoundation/Library/Frameworks/libidris2_support.dylib' (no such file), '/nix/store/lxfslviarb3h6a2fa9ndwcv37j4dmjls-swift-corefoundation/Library/Frameworks/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/srid/code/idris-template/libidris2_support.dylib' (no such file), '/usr/local/lib/libidris2_support.dylib' (no such file), '/usr/lib/libidris2_support.dylib' (no such file)
air:idris-template srid$ tail -2 $(which idris2)
export DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH${DYLD_LIBRARY_PATH:+':'}'/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/lib'
exec -a "$0" "/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/bin/.idris2-wrapped"  "$@"
air:idris-template srid$ 

[srid]

This doesn't look like valid shell syntax to me. Maybe that's the cause of the bug.

export DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH${DYLD_LIBRARY_PATH:+':'}'/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/lib'

[wchresta]

Hmm I'm not sure what's wrong. Seems fine when I test it with both bash and zsh, at least with linux:

zsh$ 
zsh$ echo $DYLD_LIBRARY_PATH

zsh$ export DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH${DYLD_LIBRARY_PATH:+':'}'/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/lib'
zsh$ echo $DYLD_LIBRARY_PATH                                                                                                                        
/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/lib
zsh$ export DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH${DYLD_LIBRARY_PATH:+':'}'/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/lib'
zsh$ echo $DYLD_LIBRARY_PATH                                                                                                                        
/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/lib:/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/lib
zsh$ 

The newly added tests in #151237 also seem to work fine on darwin.

Can you provide the output of idris2 --paths and also cat your idris2 wrapper script:

cat $(which idris2)

[srid]

air:idris-template srid$ idris2 --paths
+ Working Directory      :: "/Users/srid/code/idris-template"
+ Source Directory       :: Nothing
+ Build Directory        :: "build"
+ Local Depend Directory :: "depends"
+ Output Directory       :: "build/exec"
+ Installation Prefix    :: "/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1"
+ Extra Directories      :: [".", "/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/base-0.5.1", "/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/contrib-0.5.1", "/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/network-0.5.1", "/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/prelude-0.5.1", "/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/prelude-0.5.1", "/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/base-0.5.1"]
+ Package Directories    :: []
+ CG Library Directories :: ["/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/lib", "/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/lib", "/Users/srid/code/idris-template"]
+ Data Directories       :: ["/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/support", "/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/support"]
air:idris-template srid$

air:idris-template srid$ which idris2
/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/bin/idris2
air:idris-template srid$ more /nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/bin/idris2
#! /nix/store/3npg6a8nc5vpcyw98v085cmlz7f78kgs-bash-5.1-p12/bin/bash -e
export CHEZ=${CHEZ-'/nix/store/x09jcyffdc42zlkj0achk4ycpq1igxkh-chez-scheme-9.5.6/bin/scheme'}
export IDRIS2_LIBS=$IDRIS2_LIBS${IDRIS2_LIBS:+':'}'/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/lib'
export IDRIS2_DATA=$IDRIS2_DATA${IDRIS2_DATA:+':'}'/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/support'
export IDRIS2_PATH=$IDRIS2_PATH${IDRIS2_PATH:+':'}'/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/base-0.5.1:/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/contrib-0.5.1:/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/network-0.5.1:/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/prelude-0.5.1'
export DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH${DYLD_LIBRARY_PATH:+':'}'/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/idris2-0.5.1/lib'
exec -a "$0" "/nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/bin/.idris2-wrapped"  "$@"
air:idris-template srid$

[cherryblossom000]

I think this is an issue upstream that was fixed by https://github.com/idris-lang/Idris2/pull/2078 (but that PR isn't included in v0.5.1).

If using the Chez backend, Idris generates a script like this:

#!/bin/sh
# @generated by Idris 0.5.1, Chez backend

set -e # exit on any error

if [ "$(uname)" = Darwin ]; then
  DIR=$(zsh -c 'printf %s "$0:A:h"' "$0")
else
  DIR=$(dirname "$(readlink -f -- "$0")")
fi

export LD_LIBRARY_PATH="$DIR/test_app:$LD_LIBRARY_PATH"
export IDRIS2_INC_SRC="$DIR/test_app"
"$DIR/test_app/test.so" "$@"

A workaround is to sed -i '' 's/LD_LIBRARY_PATH/DYLD_LIBRARY_PATH/g' build/exec/test.

[cherryblossom000]

Another workaround it to symlink the libidris2_support.dylib into /usr/local/lib (ln -s /nix/store/3c286s013wsbb6f5mx3vpskfag8w6ql7-idris2-0.5.1/lib/libidris2_support.dylib /usr/local/lib/libidris2_support.dylib). That way the :exec command in the REPL works as well.

[shmish111]

I've just come across this when trying to build idris2 with nix on darwin aarch64. Since idris2 is bootstrapped in the same way as this error occurs it seems it is broken in nixpkgs now for this architecture.

 - system: `"aarch64-darwin"`
 - host os: `Darwin 21.5.0, macOS 12.4`
 - multi-user?: `yes`
 - sandbox: `no`
 - version: `nix-env (Nix) 2.10.3`
 - channels(root): `"nixpkgs"`
 - channels(davidsmith): `"darwin, home-manager, nixpkgs-unstable"`
 - nixpkgs: `/nix/var/nix/profiles/per-user/root/channels/nixpkgs`
 - ```

[mattpolzin]

Can anyone reproduce anything resembling this issue these days with latest nixpkgs unstable which works out to Idris2 v 0.7.0? My guess is this issue can be closed since I am able to use Idris 2 on Apple Silicon via nixpkgs these days, but don't know for sure there are no edge cases to be found.

[mattpolzin]

Now that v0.7.0 of Idris2 is in nixpkgs stable and I'm not aware of any recent examples of this issue, I'll close it out. We can reopen if this problem comes up again.