包

Idris 包括一个简单的构建系统，用于从一个命名的包描述文件中构建包和可执行文件。这些文件可以与 Idris 编译器一起使用，以管理开发过程。

包描述

一个包的描述包括以下内容：

• 一个头，由关键词``package``组成，后面是一个包名。包名可以是任何有效的 Idris 标识符。iPKG 格式也需要一个带引号的版本，接受任何有效的文件名。

• 描述包内容的字段， <field> = <value> 。

至少有一个字段必须是模块字段，其值是一个逗号分隔的模块列表。例如，给定一个 idris 包 maths ，其中有模块 Maths.idr ， Maths.NumOps.idr ， Maths.BinOps.idr ，和 Maths.HexOps.idr ，相应的包文件应该是：

package maths

modules = Maths
        , Maths.NumOps
        , Maths.BinOps
        , Maths.HexOps

运行 idris2 --init 将在当前目录下交互式地创建一个新的包文件。生成的包文件列出了所有可配置的字段，并附有简要说明。

其他包文件的例子可以在 libs 目录下的主Idris资源库中找到，也可以在 `第三方库 <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_中找到 。

使用包文件

Idris 本身知道软件包，并且有特殊的命令来帮助，例如，构建软件包，安装软件包，和清理软件包。 例如，考虑到前面的 maths 包，我们可以按以下方式使用 Idris：

• idris2 --build maths.ipkg 将构建包中的所有模块

• idris2 --install maths.ipkg 将安装这个包，使其他 Idris 库和程序可以访问它。

• idris2 --clean maths.ipkg 将删除所有中间代码和构建时产生的可执行文件。

一旦安装了 math 包，命令行选项 --package maths 使其可以访问（缩写为 -p maths ）。比如：

idris2 -p maths Main.idr

在 Atom 中使用包依赖

如果你在使用 Atom 编辑器，并且有对另一个软件包的依赖，例如对应于 import Lightyear 或 import Pruviloj ，你需要让 Atom 知道它应该被加载。最简单的方法是通过一个 .ipkg 文件来实现。 ipkg 文件的一般内容将在本教程的下一节中描述，但现在这里有一个简单的示例，用于这个微不足道的案例：

• 创建一个文件夹 myProject。

• 添加一个只包含几行的 myProject.ipkg 文件：

package myProject

depends = pruviloj, lightyear

• 在 Atom 中，使用文件菜单，打开文件夹 myProject 。