Mercurial > hg > Members > kono > Proof > automaton
view a02/agda-install.ind @ 252:9fc9e19f2c37
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 29 Jun 2021 20:03:32 +0900 |
parents | 26407ce19d66 |
children | 407684f806e4 |
line wrap: on
line source
-title: Agda の install の方法 Homebrew を使うのが良いそうです。 brew install agda GHCが入ってないなら、 brew install ghc install 先がどこかは、 /usr/local/Cellar/agda/2.6.1/lib/agda などになるので、 brew install の指示通りに ~/.agda に以下のファイルを置きます defaults libraries defaults の中には standard-library libraries の中には /usr/local/Cellar/agda/2.5.2/lib/agda/standard-library.agda-lib --VS-code plugin から agda-mode を探して install test.agda を作って module test where open import Data.Nat a : ? a = 1 として C-C C-L が通れば Ok --Emacs Emacs を先に入れます。 brew tap caskroom/cask brew cask install emacs ~/.emacs.d/init.el に以下のファイルを置きます。あるいは自分のinit.el に適当に追加します。 中のpathは正しいものに置き換えます。 <a href="init.el"> init.el </a> GUI 側で使わないと文字化けすることがあるようです。Terminal で使いたい時には、 <a href="https://github.com/hamano/locale-eaw"> locale eaw </a> が必要です。 Emacs から使うので、Emacs も勉強しよう。 <a href="http://ie.u-ryukyu.ac.jp/%7Ekono/howto/mule.html"> Emacs の使い方 </a> C-C control と C を同時に押す M-X esc を押してから X を押す C-X C-F で、Agda1.agda file を開けます。 M-X help-for-help M で、Agda のコマンドの一覧が出ます。C-X o で buffer を切り替えて読みます。 Space Emacs というのもあるらしい。 --vim <a ref="https://github.com/derekelkins/agda-vim"> agda-vim</a> が使えます。