入门

从源代码安装

前置条件

因为Idris 2 是由 Idris 2 自身实现的，所以要启动它，你可以从生成的 Scheme 源码开始构建。要做到这一点，你需要 Chez Scheme （默认的，目前首选，因为它是最快的）或 Racket 。你可以从以下地方获得其中之一：

两者都可以从 MacPorts/Homebrew 和所有主要的 Linux 发行版获得。Windows 需要一些进一步的先决条件，详详见 Windows 的先决条件。

注意：如果你从源文件安装 Chez Scheme，在本地构建它的时候，确保你运行 ./configure --threads 来构建多线程支持。

下载和安装

你可以从 Idris网站下载Idris 2源代码，或者从Github上的 idris-lang/Idris2 获得最新的开发版本。这包括Idris 2的源代码和由此产生的 Scheme 代码。一旦你解压了源代码，你可以按以下方式安装它：

make bootstrap SCHEME=chez

其中 chez 是 Chez Scheme 编译器的可执行名称。这因系统而异，但通常是 scheme ， chezscheme ，或 chezscheme9.5 中的一种。如果你是通过 Racket 构建的，你可以按以下方式安装它：

make bootstrap-racket

一旦你用上述任何一个命令成功启动，你就可以用 make install 命令进行安装。默认情况下，这将安装到 ${HOME}/.idris2 。你可以通过编辑 config.mk 中的选项来改变这个。例如，要安装到 /usr/local ，你可以编辑 IDRIS2_PREFIX ，如下所示：

IDRIS2_PREFIX ?= /usr/local

从包管理器安装

使用 Homebrew 进行安装

如果你是 Homebrew 用户，你可以通过运行以下命令安装 Idris 2 和所有的依赖：

brew install idris2

使用 Yay 进行安装

如果你使用的是基于 Arch 的发行版，你可以通过运行以下命令安装 Idris 2 和所有依赖：

yay -S idris2

检查安装

为了检查安装是否成功，并编写你的第一个 Idris 程序，创建一个名为 hello.idr 的文件，并包含以下文本：

module Main

main : IO ()
main = putStrLn "Hello world"

如果你熟悉 Haskell ，应该相当清楚这个程序在做什么以及如何工作，如果不熟悉，我们将在后面解释细节。你可以通过在 shell 提示符下输入 idris2 hello.idr -o hello 来将程序编译成可执行文件。默认情况下，这将创建一个名为 hello 的可执行程序，它将调用一个生成和编译的 Chez Scheme 程序，在目标目录 build/exec 中，你可以运行它：

$ idris2 hello.idr -o hello
$ ./build/exec/hello
Hello world

请注意，美元符号 $ 表示 shell 提示！ Idris 命令的一些有用的选项是：

-o prog 编译成可执行文件，名为 prog 。
--check 文件类型检查和它的依赖关系，而不启动交互式环境。
--package pkg 添加软件包为依赖项，例如 --package contrib 表示使用 contrib 包。
--help 显示使用摘要和命令行选项。

你可以在编译为可执行文件一节中找到更多关于编译成可执行文件的信息。

交互式环境

在 shell 提示符下输入 idris2 ，就会启动交互式环境。你应该看到类似下面的内容：

$ idris2
     ____    __     _         ___
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.7.0
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
 /___/\__,_/_/  /_/____/   /____/      Type :? for help

Welcome to Idris 2.  Enjoy yourself!
Main>

这给出了一个 ghci 风格的界面，允许对表达式进行求值以及类型检查；定理证明、编译；编辑；以及其他各种操作。命令 :? 给出了一个支持的命令列表。下面，我们看到一个运行的例子，其中 hello.idr 被加载， main 的类型被检查，然后程序被编译为可执行文件 hello ，可在目标目录 build/exec/ 中获得。对文件进行类型检查，如果成功的话，会创建一个文件的字节码版本（在本例中是 build/ttc/hello.ttc ），以加快未来的加载速度。如果源文件发生变化，则重新生成字节码。

$ idris2 hello.idr
     ____    __     _         ___
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.7.0
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
 /___/\__,_/_/  /_/____/   /____/      Type :? for help

Welcome to Idris 2.  Enjoy yourself!
Main> :t main
Main.main : IO ()
Main> :c hello main
File build/exec/hello written
Main> :q
Bye for now!