Success building native Idris2 on an M1 Mac

This page summarizes the projects mentioned and recommended in the original post on /r/Idris

InfluxDB - Power Real-Time Data Analytics at Scale
Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
www.influxdata.com
featured
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com
featured
  • ChezScheme

    Chez Scheme (by racket)

  • I succeeding in installing a native arm64 Idris2 on an M1 Mac. I wish that I had found clear directions all in one place. I would be happy to contribute such directions, after experts have commented on what I did. Where should these directions go? As of this writing, the official Chez Scheme is not arm64 native, but the Racket fork of Chez Scheme is arm64 native. I first installed Racket's Chez Scheme (9.5.5.5), which appears to support Idris2. https://github.com/racket/ChezScheme/ It is likely that a full Racket installation will also put this somewhere, but I could not find it. Chez Scheme uses idiosyncratic machine types, which take some sleuthing to find. Once one has a working scheme, `(machine-type)` evaluates to the machine type, but there is a chicken-and-egg problem here. At a command line, `arch` prints the machine architecture, `i386` or `arm64`. The Chez Scheme machine type for an `i386` Mac is `ta6osx`. The Chez Scheme machine type for an `arm64` M1 Mac is `tarm64osx`. The full build instructions for Chez Scheme on an M1 Mac become arch=tarm64osx ./configure --pb make ${arch}.bootquick ./configure --threads make sudo make install sudo chown $(whoami) ${arch}/petite.1 ${arch}/scheme.1 The final `chown` keeps this directory from interfering with synchronization software such as `unison`. The Makefile is a bit sloppy about cleaning up ownership, and leaves these files assigned to `root`. I found that `make clean` did not sufficiently restore the Chez Scheme build directory to be used on a different architecture, so my script unpacks the build directory from scratch. I probably missed the correct scorched earth incantation; I know without diving into code that starting with a virgin build directory works. Now, a bootstrap build of Idris2 requires two tweaks. https://www.idris-lang.org/pages/download.html First, the build needs `gmp` which I installed via Homebrew. However, Homebrew provides the file `/opt/homebrew/include/gmp.h` on an M1 Mac, rather than `/usr/local/include/gmp.h` as on other Macs. The build uses `/usr/bin/cc` which knows about `/usr/local/include` but not `/opt/homebrew/include`. One needs to set the `CPATH` environment variable. One therefore builds with the commands export CPATH="/opt/homebrew/include" make bootstrap SCHEME=scheme make install Apparently Homebrew had an `#M1too` moment where they were convinced that it was poor practice to use `/usr/local` because others do, so they switched to `/opt/homebrew` for M1 Macs. I never had a problem with this, but I don't relish having recurring problems separately teaching every language in my programming zoo how to find libraries provided by Homebrew. I wish I could find the tortuous discussion leading to this decision, for I'm sure it would be delightful reading, and might shed light on this. There is a final problem: The Idris2 build is unaware of the Racket Scheme machine type. As I start with virgin build directories for each machine, I found it simplest to globally replace every occurrence of `ta6osx` by `tarm64osx`. This works. One should perhaps add `arm64osx` and `tarm64osx` to the existing code, alongside `ta6osx`. I don't fully understand the naming conventions (one wants to guess in advance what the official Chez Scheme will choose when it supports M1 Macs), or the code I was modifying, so I didn't test this.

  • InfluxDB

    Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

    InfluxDB logo
NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts