|
127
|
1 -title: Agda の install の方法
|
|
|
2
|
|
|
3 Homebrew を使うのが良いそうです。
|
|
|
4
|
|
|
5
|
|
|
6 brew install agda
|
|
|
7
|
|
|
8 GHCが入ってないなら、
|
|
|
9
|
|
|
10 brew install ghc
|
|
|
11
|
|
|
12 install 先がどこかは、
|
|
|
13
|
|
141
|
14 /usr/local/Cellar/agda/2.6.1/lib/agda
|
|
127
|
15
|
|
|
16 などになるので、
|
|
|
17
|
|
141
|
18 brew install の指示通りに ~/.agda に以下のファイルを置きます
|
|
127
|
19
|
|
|
20 defaults libraries
|
|
|
21
|
|
|
22 defaults の中には
|
|
|
23
|
|
|
24 standard-library
|
|
|
25
|
|
|
26 libraries の中には
|
|
|
27 /usr/local/Cellar/agda/2.5.2/lib/agda/standard-library.agda-lib
|
|
|
28
|
|
141
|
29 --VS-code
|
|
|
30
|
|
|
31 plugin から agda-mode を探して install
|
|
|
32
|
|
|
33 test.agda を作って
|
|
|
34
|
|
|
35 module test where
|
|
|
36 open import Data.Nat
|
|
|
37 a : ?
|
|
|
38 a = 1
|
|
|
39
|
|
|
40 として C-C C-L が通れば Ok
|
|
|
41
|
|
|
42 --Emacs
|
|
|
43
|
|
163
|
44 Emacs を先に入れます。
|
|
|
45
|
|
|
46 brew tap caskroom/cask
|
|
|
47 brew cask install emacs
|
|
|
48
|
|
127
|
49 ~/.emacs.d/init.el に以下のファイルを置きます。あるいは自分のinit.el に適当に追加します。
|
|
|
50 中のpathは正しいものに置き換えます。
|
|
|
51
|
|
|
52 <a href="init.el"> init.el </a>
|
|
|
53
|
|
|
54 GUI 側で使わないと文字化けすることがあるようです。Terminal で使いたい時には、
|
|
|
55
|
|
|
56 <a href="https://github.com/hamano/locale-eaw"> locale eaw </a>
|
|
|
57
|
|
|
58 が必要です。
|
|
|
59
|
|
|
60 Emacs から使うので、Emacs も勉強しよう。
|
|
|
61
|
|
138
|
62 <a href="http://ie.u-ryukyu.ac.jp/%7Ekono/howto/mule.html"> Emacs の使い方 </a>
|
|
127
|
63
|
|
|
64 C-C control と C を同時に押す
|
|
|
65 M-X esc を押してから X を押す
|
|
|
66
|
|
|
67 C-X C-F で、Agda1.agda file を開けます。
|
|
|
68
|
|
|
69 M-X help-for-help M で、Agda のコマンドの一覧が出ます。C-X o で buffer を切り替えて読みます。
|
|
|
70
|
|
163
|
71 Space Emacs というのもあるらしい。
|
|
127
|
72
|
|
|
73 --vim
|
|
|
74
|
|
|
75 <a ref="https://github.com/derekelkins/agda-vim"> agda-vim</a>
|
|
|
76
|
|
|
77 が使えます。
|
|
|
78
|
