入门¶
前提需求¶
在安装 Idris 之前,你需要确认是否拥有所有必须的库和工具。你需要:
- 近期版本的 GHC 。目前测试过的最早版本为 7.10.3.
- GNU 多精度运算库 (GMP) 可从 MacPorts/Homebrew 和所有主流 Linux 发行版中获取。
下载并安装¶
如果你满足所有的前提需求,那么安装 Idris 的最简方式就是在命令行输入:
cabal update; cabal install idris
这会安装 Hackage 中的最新版本及其所有依赖。如果你想要最新开发版的话, 可以在 GitHub 上找到它, 然后根据构建指令来安装。
如果你之前从未安装过使用 Cabal 的东西,Idris 可能不在你的 PATH 中。
如果 Idris 可执行文件无法找到,请将 ~/.cabal/bin
添加到 $PATH
环境变量中。Mac OS X 用户则需要添加 ~/Library/Haskell/bin
,Windows
用户通常会发现 Cabal 将程序安装在 %HOME%\AppData\Roaming\cabal\bin
中。
为了检查安装是否成功,你需要编写第一个程序。请创建一个名为 hello.idr
的文件,
其中包含以下文本:
module Main
main : IO ()
main = putStrLn "Hello world"
如果你熟悉 Haskell,那会很清楚这段程序在做什么,是如何做的;
如果你对它感到陌生,我们稍后会详细地解释。你可以在命令行中输入
idris hello.idr -o hello
来将程序编译成可执行文件。
这会创建一个名为 hello
的可执行文件,你可以运行它:
$ idris hello.idr -o hello
$ ./hello
Hello world
请注意,美元符号 $
表示命令行。下面是一些常用的 Idris 命令行选项:
-o prog
编译成名为prog
的可执行文件。--check
无需启动交互式环境就对文件及其依赖进行类型检查。--package pkg
将包添加为依赖,例如通过--package contrib
来使用 contrib 包。--help
显示用法摘要和命令行选项。
交互式环境¶
在命令行中输入 idris
来启动交互式环境。你会看到如下内容:
$ idris
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 1.3.1
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Idris>
它会提供一个 ghci
风格的界面,可以像类型检查那样求值表达式、进行定理证明、
编译、编辑、以及执行多种其它操作。命令 :?
会列出所支持的命令。在以下示例中,
hello.idr
已被加载,main
的类型已通过检查,之后该程序被编译成了可执行的 hello
。
在对某文件类型检查时,如果通过,就会创建它的的字节码版本(本例中为 hello.ibc
)
以提升未来的加载速度。在源文件被修改之后,字节码会重新生成。
$ idris hello.idr
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 1.3.1
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Type checking ./hello.idr
*hello> :t main
Main.main : IO ()
*hello> :c hello
*hello> :q
Bye bye
$ ./hello
Hello world