<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">It should also be possible to use the ordinary x86_64 releases using rosetta2. I'm not sure how to tell brew to do that.<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On 18 Apr 2021, at 22:24, Ettore Aldrovandi <<a href="mailto:aldrovandi@math.fsu.edu" class="">aldrovandi@math.fsu.edu</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><meta http-equiv="Content-Type" content="text/html; charset=utf-8" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><meta http-equiv="Content-Type" content="text/html; charset=utf-8" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Hi, <div class=""><br class=""></div><div class="">building Agda from source on homebrew requires building ghc, which is not supported on Silicon (yet), although that might change soon, see <a href="https://www.haskell.org/ghc/blog/20210309-apple-m1-story.html" class="">https://www.haskell.org/ghc/blog/20210309-apple-m1-story.html</a>. I don’t know what happens if you try building ghc first with the <font face="Osaka-Mono" class="">“—HEAD”</font><font face="AgmenaPro-Regular" class="">flag. </font></div><div class=""><br class=""></div><div class="">—Ettore</div><div class=""><br class=""><div class="">
<div dir="auto" style="letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="font-variant-ligatures: normal; font-variant-position: normal; font-variant-caps: normal; font-variant-numeric: normal; font-variant-alternates: normal; font-variant-east-asian: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="font-variant-ligatures: normal; font-variant-position: normal; font-variant-caps: normal; font-variant-numeric: normal; font-variant-alternates: normal; font-variant-east-asian: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="font-variant-ligatures: normal; font-variant-position: normal; font-variant-caps: normal; font-variant-numeric: normal; font-variant-alternates: normal; font-variant-east-asian: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="font-variant-ligatures: normal; font-variant-position: normal; font-variant-caps: normal; font-variant-numeric: normal; font-variant-alternates: normal; font-variant-east-asian: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class=""><font face="Osaka" class=""><span style="font-size: 12px;" class="">Ettore Aldrovandi</span></font></div><div class=""><font face="Osaka" class=""><span style="font-size: 12px;" class="">Department of Mathematics, Florida State University</span></font></div><div class=""><font face="Osaka" class=""><span style="font-size: 12px;" class="">1017 Academic Way * <a href="http://www.math.fsu.edu/~ealdrov" class="">http://www.math.fsu.edu/~ealdrov</a></span></font></div><div class=""><font face="Osaka" class=""><span style="font-size: 12px;" class="">Tallahassee, FL 32306-4510, USA * * aldrovandi at math dot fsu dot edu</span></font></div></div></div></div></div></div></div></div></div></div>
</div>
<div class=""><br class=""><blockquote type="cite" class=""><div class="">On Apr 18, 2021, at 05:44, Kenichi Asai <<a href="mailto:asai@is.ocha.ac.jp" class="">asai@is.ocha.ac.jp</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">What is the easy way to install agda on Apple Silicon mac? I used to<br class="">install via homebrew, but homebrew (for native Apple Silicon) tells me<br class="">I need to build from source, and if I do:<br class=""><br class="">brew install --build-from-source agda<br class=""><br class="">I am told to build ghc from source, too, which fails. Thanks in advance!<br class=""><br class="">-- <br class="">Kenichi Asai<br class="">_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class=""><a href="https://lists.chalmers.se/mailman/listinfo/agda" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class=""><br class=""></div></div></blockquote></div><br class=""></div></div></div>_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">https://lists.chalmers.se/mailman/listinfo/agda<br class=""></div></blockquote></div><br class=""></body></html>