Clarify installation instructions on macOS (M1)

[ornamentist]

When following the standard installation instructions there are a few gotchas for installation on macOS with an M1 processor:

Using homebrew brew install idris2 is currently not working:

brew install idris2
Running `brew update --preinstall`...
...
Error: idris2: no bottle available!
You can try to install from source with:
  brew install --build-from-source idris2
Please note building from source is unsupported. You will encounter build
failures with some formulae. If you experience any issues please create pull
requests instead of asking for help on Homebrew's GitHub, Twitter or any other
official channels.

I understand this is an issue for the Homebrew maintainer of that brew and not one for the official project, although it does have a bearing on what comes next.

Moving to installation from source with Chez scheme, the formula is also currently not working:

brew install chezscheme
Error: chezscheme: no bottle available!
You can try to install from source with:
  brew install --build-from-source chezscheme
Please note building from source is unsupported. You will encounter build
failures with some formulae. If you experience any issues please create pull
requests instead of asking for help on Homebrew's GitHub, Twitter or any other
official channels.

Again this is not the responsibility of the Idris2 developers, but it leads to installing from source with Racket.

brew search racket
==> Formulae
minimal-racket           rack                     tracker                  packetq

==> Casks
brackets                                           racket ✔
Warning: Use minimal-racket instead of deprecated racket

It's not clear whether minimal racket is enough to build Idris2 so I went with the full racket install. I cloned the Idris2 repository and did a gmake bootstrap-racket which now complains about a missing gmp.h.

GMP is installed via Homebrew but the make commands are not finding gmp.h so I modified the config.mk file to add -I/opt/homebrew/include to the CFLAGS variable. This allowed the build to complete.

A gmake install installed everything in the local directory and not the config.mk prefix, so I changed the PREFIX make variable to /Users/stu/.idris2 which did work. This may be because I'm running fish shell and not bash.

Finally, when I run the idris2 script I get a idris2 -o hello hello.idr env: scheme: No such file or directory error. I'm guessing there's a make variable somewhere that points to a scheme executable which Racket doesn't provide? I tried linking the racket executable to scheme too:

~> ln -s (which racket) ~/.local/bin/scheme
~> scheme
Welcome to Racket v8.3 [cs].
> ^D
~> idris2 -o hello hello.idr
build/exec/hello_app/compileChez:1:0: #%top-interaction: unbound identifier;
 also, no #%app syntax transformer is bound
  at: #%top-interaction
  in: (#%top-interaction parameterize ((optimize-level 3) (compile-file-message #f)) (compile-program "/Users/stu/projects/numerous/idris/build/exec/hello_app/hello.ss"))
  location...:
   build/exec/hello_app/compileChez:1:0

Which looks like idris2 wants the Chez scheme executable even though it was built with Racket?

Should I treat the macos/M1/homebrew/racket combination as unsupported just for now? I suspect the maintainers have enough on their plate already.

[ornamentist]

Okay,

Following https://www.reddit.com/r/Idris/comments/pc5lib/success_building_native_idris2_on_an_m1_mac/ I followed these steps for a successful installation:

Firstly, install the Racket fork of Chez Scheme, not Cisco Chez Scheme or Racket:

cd ~/tmp
git clone git@github.com:racket/ChezScheme.git
cd ChezScheme
git submodule init
git submodule update
arch=tarm64osx
./configure --pb
make ${arch}.bootquick
./configure --threads
make
sudo make install
sudo chown $(whoami) ${arch}/petite.1 ${arch}/scheme.1

Now install Idris2:

brew install gmp
cd ~/tmp
git clone https://github.com/idris-lang/Idris2.git
cd Idris2
export CPATH="/opt/homebrew/include"
make bootstrap SCHEME=scheme
make install

Thanks also to the pointers on Discord.

[gallais]

Which looks like idris2 wants the Chez scheme executable even though it was built with Racket?

By default idris2 will use chezscheme to compile .idr files. You have to explicitly
request the racket code generator if you want to use racket by passing --cg racket
to idris2.

Using the chezscheme code generator & trying to compile the result with racket (by symlinking
racket for chez) is bound to fail.

[kevzettler]

I tried following @ornamentist guides to compile racket/ChezScheme and getting the same error on #1032

kevzettler@Kevs-MacBook-Pro-3 Idris2 % make bootstrap SCHEME=scheme
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/libidris2_support.so/libidris2_support.dylib/g; s|__PREFIX__|/Users/kevzettler/code/Idris2/bootstrap-build|g' \
		bootstrap/idris2_app/idris2.ss \
		> bootstrap-build/idris2_app/idris2-boot.ss
/bin/sh ./bootstrap-stage1-chez.sh
Bootstrapping SCHEME=scheme IDRIS2_VERSION=0.5.1
Building idris2-boot from idris2-boot.ss
compiling idris2_app/idris2-boot.ss with output to idris2_app/idris2-boot.so
IDRIS2_CG="chez" /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=chez 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
Exception: (while loading libidris2_support.dylib) dlopen(libidris2_support.dylib, 0x0002): 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)
make[2]: *** [all] Error 255
make[1]: *** [prelude] Error 2
make: *** [bootstrap] Error 2
kevzettler@Kevs-MacBook-Pro-3 Idris2 %

[Syzygies]

I have updated my guide for Apple silicon:

Building Idris2 for Apple silicon as of August 2022

[dunhamsteve]

Some of the issues that Syzygies struggled with are fixed post 0.5.1. It's been a year and a lot of stuff has been fixed since then. Perhaps there should be a new release of Idris.

For M1 / M2 macs, the bootstrap does work on the latest development version with the special chez scheme described above, but there are no instructions for this in INSTALL.md and the official Idris website directs people to the 0.5.1 tar file.

I'll submit a PR to update the INSTALL.md.

[c4augustus]

Note that installing gmp via MacPorts puts it in a different location than what is assumed for homebrew. I made a branch commit in my own fork of Idris2 to address this: https://github.com/c4augustus/Idris2/commit/15a2b7039c72135d11017e93d78b568ed9e780d1

I build for macOS M1 using the Racket fork of ChezScheme and this fix worked for running the idris2 REPL as well as building executables. However, I still get the "'gmp.h' file not found" when trying to build to backend C source using refc, so somehow I need to get those CFLAGS over to its build process.

[dunhamsteve]

Yeah, I needed both of these in the environment to build with the C backend on M1 macs:

export CPATH=/opt/homebrew/include:/opt/homebrew/lib
export IDRIS2_LIBS=/opt/homebrew/lib

The IDRIS2_LIBS is needed for the refc backend. I tracked it down by looking at how the compiler was building the command to invoke the C compiler. It's the clibdirs (lib_dirs dirs) line in the code below (from CC.idr):

     let runcc = escapeCmd $
         [cc, "-Werror"] ++ sharedFlag ++ [objectFile,
              "-o", outFile,
              supportFile,
              "-lidris2_refc",
              "-L" ++ refcDir
              ] ++ clibdirs (lib_dirs dirs) ++ [
              "-lgmp", "-lm"]