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

Mac m1 libc not found #1219

Closed ceberly closed 2 years ago

ceberly commented 3 years ago

Similar to a couple other people, I've been trying to use idris2 on an macbook m1.

I've tried using the Racket fork of Chez Scheme as well as the Racket bootstrap of Idris2, and in both cases I end up getting this error at the end of bootstrap phase:

--- snip ---
make -C libs/prelude IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/Users/chris/extsrc/Idris2/libs/prelude/build/ttc:/Users/chris/extsrc/Idris2/libs/base/build/ttc:/Users/chris/extsrc/Idris2/libs/contrib/build/ttc:/Users/chris/extsrc/Idris2/libs/network/build/ttc:/Users/chris/extsrc/Idris2/libs/test/build/ttc"
../../build/exec/idris2 --build prelude.ipkg
Exception: (while loading libc.so) dlopen(libc.so, 2): image not found
make[2]: *** [all] Error 255
make[1]: *** [prelude] Error 2
make: *** [bootstrap-racket] Error 2

Seems like a weird error but I figured I would post here while i'm digging into it.

gallais commented 3 years ago

Should this go in #1032? Seems to be the same problem with a different .so.

ceberly commented 3 years ago

I think this is actually a problem with Chez scheme looking for libraries in the incorrect location. I am trying to diagnose whats going on before I close this issue.

ceberly commented 3 years ago

So, I actually was able to fix this and get Idris2 running. The issue was the bootstrap code does not know about the tarm64osx machine type which is created by Racket's fork of Chez Scheme: https://github.com/racket/ChezScheme

This is the diff with my fork of Idris: https://github.com/idris-lang/Idris2/compare/master...ceberly:master

I am not at all familiar with the Idris2 build system, and so I do not know whether this qualifies as something that should be made into an actual PR. But I will leave it here if anyone has any opinions or runs into the same issue.

ceberly commented 3 years ago

Just a note, make test does not work, it fails with the same issue as #1032

benhormann commented 3 years ago

Shouldn't it be .dylib? @ceberly Have you tried adding include ../../config.mk to libs/*/Makefile, and ../config.mk to tests/Makefile?

ceberly commented 3 years ago

@benhormann yes, in my diff (https://github.com/idris-lang/Idris2/compare/master...ceberly:master) i am causing the build file to use the *.dylib version if you are using Racket's fork of chez scheme.

I will try the config thing later today ...

codimension commented 2 years ago

I was able to install Idris (after working around another issue) today on my M1 Mac with the Racket backend, and didn't come across this issue. Was able to run compiled executables and REPL, so maybe this can be closed?

andrevidela commented 2 years ago

Same here, I'll close it for now, feel free to reopen if this shows up again