Idris2

Idris2 copied to clipboard

I am following the Idris2 documentation to install Idris on a MacBook M1 Pro 2021 laptop (macOS Monterey v12.2.1) using brew install idris2. I am seeing the following error:

eddy@Edwards-MacBook-Pro Github % brew install idris2
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 have tried installing with --build-from-source however that throws other errors and the docs don't mention this method so I assume it's not necessary to debug further.

Let me know if I can provide any further information!

Error: idris2: no bottle available!

tells me this is a homebrew error and so should be reported there.

As for the build from source, we'd need to know what the errors are to provide help.

tells me this is a homebrew error and so should be reported there.

Fair enough, but can we keep this open for a little while to see if any others have the same issue? Apple Silicon is practically synonymous with build errors so I don't know if this is a local or general issue.

I'll try build with source again and get the errors later!

@Mithaecus have you seen https://github.com/idris-lang/Idris2/issues/2233#issuecomment-1002915184

You need to use the Racket fork of Chez Scheme

The homebrew formula lives at https://github.com/Homebrew/homebrew-core/blob/master/Formula/idris2.rb

Chez doesn't support Apple Silicon yet but there is a draft PR. https://github.com/cisco/ChezScheme/pull/607

@michaelmesser Thanks, I hadn't seen #2233 but it worked correctly. Add /Users/<username>/.idris2/binto your $PATH and you're good to go. As they mentioned you have to install https://github.com/racket/ChezScheme which is a fork that already has M1 support. Once https://github.com/cisco/ChezScheme/pull/607 has been merged and Brew updated feel free to @ me to test it on an M1 MacBook if you'd like someone to check it out :)

It may be possible to modify the formula to use the Racket fork of Chez scheme on ARM. I don't know if there is a formula for the Racket fork of Chez.

Racket's fork of Chez Scheme used to work with Idris 2. The Nix expression still uses it, but it broke. I propose switching the version of Chez Scheme used to Racket's fork for all platforms.

I propose switching the version of Chez Scheme used to Racket's fork for all platforms.

I think it would be preferable to get chez-scheme upstream to integrate the aarch64 support from the racket fork.

See: https://github.com/cisco/ChezScheme/issues/545 and https://github.com/cisco/ChezScheme/issues/544

Note that Mac ChezCheme PR was merged; see https://github.com/cisco/ChezScheme/issues/545#issuecomment-1768915042

This now can be done I suppose