[Agda] Agda on Apple Silicon?

[Martin Escardo]

Good. The cabal installation also produced native code. (Something that 
typed checked in 4m30s now typechecks in 4m.) Martin

On 20/06/2021 13:25, liang.ting.chen.tw at gmail.com wrote:
> The latest GHC 8.10.5 now supports the native code generation for Apple 
> M1 (arm64), and homebrew has updated its formula to use GHC 8.10.5 for 
> building Agda.
> 
> https://formulae.brew.sh/formula/agda#default 
> <https://formulae.brew.sh/formula/agda#default>
> 
> So, on macOS, installing it via homebrew just works again.
> 
> Best regards,
> Liang-Ting
> 
> On Sun, Jun 20, 2021 at 19:53 Martin Escardo <m.escardo at cs.bham.ac.uk 
> <mailto:m.escardo at cs.bham.ac.uk>> wrote:
> 
>     Now just following the cabal installation instructions in the Agda wiki
>     works for the apple m1 chip. I did this to install the new version of
>     Agda. M.
> 
>     On 19/04/2021 05:27, asai at is.ocha.ac.jp <mailto:asai at is.ocha.ac.jp>
>     wrote:
>      > Thank you for all the information!  I could install agda (2.6.1.3)
>      > successfully.  For record, I write what I did (following Martin's
>      > message):
>      >
>      > softwareupdate --install-rosetta
>      > arch -x86_64 /bin/bash -c "$(curl -fsSL
>     https://raw.githubusercontent.com/Homebrew/install/master/install.sh
>     <https://raw.githubusercontent.com/Homebrew/install/master/install.sh>)"
>      > arch -x86_64 /usr/local/bin/brew install agda
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
> 
> -- 
> --
> Dr Liang-Ting Chen
> Institute of Information Science
> Academia Sinica, Taiwan
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>