Agdaでコンパイル
Agdaではじめてコンパイルしてみたので、そのやり方メモ。環境はWindows7。
emacs上でコードを書く
module HelloAgdaWorld where open import IO.Primitive open import Foreign.Haskell open import Data.String main : IO Unit main = putStrLn (toCostring "Hello, Agda world!")
追加インストール
ここをみたらC-c C-x C-cでコンパイルできるとあったのでやってみるも、IO.FFIがないと言われてエラー。ググってみたら、これがまさに原因だと思い。追加のHaskellコードのインストール。
C:\Users\Shuji\Documents\agdalib\lib-0.7\ffi>cabal install Config file path source is default config file. Config file C:\Users\Shuji\AppData\Roaming\cabal\config not found. Writing default configuration to C:\Users\Shuji\AppData\Roaming\cabal\config Warning: The package list for 'hackage.haskell.org' does not exist. Run 'cabal update' to download it. Resolving dependencies... Configuring agda-lib-ffi-0.0.2... Building agda-lib-ffi-0.0.2... Preprocessing library agda-lib-ffi-0.0.2... [1 of 2] Compiling IO.FFI ( IO\FFI.hs, dist\build\IO\FFI.o ) [2 of 2] Compiling Data.FFI ( Data\FFI.hs, dist\build\Data\FFI.o ) In-place registering agda-lib-ffi-0.0.2... Installing library in C:\Users\Shuji\AppData\Roaming\cabal\agda-lib-ffi-0.0.2\ghc-7.6.3 Registering agda-lib-ffi-0.0.2... Installed agda-lib-ffi-0.0.2 C:\Users\Shuji\Documents\agdalib\lib-0.7\ffi>
