Mac OS的Agda安装

1. 安装Homebrew, 教程百度或者Google;

2. 打开终端, 输入命令brew install agda , 很快就会安装完毕, 此时Haskell也已会安装;

3. 上述命令执行接触后应该会有输出:

   To use the Agda standard library by default:
     mkdir -p ~/.agda
     echo /usr/local/lib/agda/standard-library.agda-lib >>~/.agda/libraries
     echo standard-library >>~/.agda/defaults
   

   依次在命令行中, 执行上面的三个命令;

4. 创建一个Hello.agda文件, 其内容为

   module Hello where
   
   open import IO
   
   main = run (putStrLn "Hello, World!")
   

   然后通过执行agda --compile Hello.agda, 如果执行成功, 得到执行文件Hello, 执行./Hello得到输出Hello, World!, 则agda安装成功.

5. 如果在执行agda --compile Hello.agda时得到Could not find module ‘Numeric.IEEE’, 则执行下面三条命令:

   brew install cabal-install # 安装cabal, 若有则不需要安装
   cabal update
   cabal install --lib ieee754
   

   在编译应该就会通过.

关于ieee754的安装参考1

关于ieee754的安装参考2