包
Idris 提供了一套基于包描述文件的构建系统。这些文件可与 Idris 编译器配合使用，用于管理 Idris 程序和包的开发流程。
包描述
一个包的描述包括以下内容：
包描述文件的开头由关键字
package和包名组成。包名可以是任意合法的 Idris 标识符。iPKG 格式还支持带引号的版本，可接受任意合法的文件名。用于描述包内容的字段，格式为
<field> = <value>
包可以描述库（library）、可执行文件（executable）或两者兼有，并应包含版本号。对于库包，必须包含 modules 字段，其值为要安装的模块名列表（用逗号分隔）。例如，一个名为 test 的库，其源文件包含 Foo.idr 和 Bar.idr 两个模块，描述如下：
package test
version = 0.0.1
modules = Foo, Bar
安装后，该包会位于目录 test-0.1 下。如果未指定版本号，则默认为 0。
其他包文件的例子可以在 libs 目录下的主Idris资源库中找到，也可以在 `第三方库 <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_中找到 。
元数据（Metadata）
iPKG 格式支持与包相关的额外元数据。可用的附加字段有：
brief = "<text>"，字符串字面量，包含包的简要描述。version = <version number>，语义化版本号，必须为用点分隔的整数（如1.0.0、0.3.0、3.1.4等）。langversion <version constraints>，具体可用约束见下方depends字段。例如：langversion >= 0.5.1 && < 1.0.0readme = "<file>"，README 文件的位置。license = "<text>"，字符串描述许可证信息。authors = "<text>"，作者信息。maintainers = "<text>"，维护者信息。homepage = "<url>"，包相关的网站。sourceloc = "<url>"，源代码所在的 DVCS 地址。bugtracker = "<url>"，项目缺陷跟踪系统的地址。
目录（Directories）
sourcedir = "<dir>"，用于查找 Idris 源文件的目录。builddir = "<dir>"，用于存放已检查模块和代码生成器产物的目录。outputdir = "<dir>"，代码生成器输出可执行文件的目录。
常用字段（Common Fields）
在 ipkg 文件中还可能包含以下常用字段：
executable = <output>，指定要生成的可执行文件名。可执行文件名可以是任意合法的 Idris 标识符。iPKG 格式还支持带引号的版本，可接受任意合法的文件名。可执行文件默认放在
build/exec目录下。可通过指定outputdir字段更改其位置。main = <module>，指定主模块名。当存在executable字段时，必须指定该字段。opts = "<idris options>，用于向 Idris 传递编译选项。depends = <pkg description> (',' <pkg description>)+，逗号分隔的依赖包名列表。pkg_description为包名，后可跟可选的版本约束。版本约束用&&分隔，可使用<、<=、>、>=、==等运算符。例如，以下为合法的包描述：
使用包文件
假设有一个 Idris 包文件 test.ipkg，可通过以下方式与 Idris 编译器配合使用：
idris2 --build test.ipkg会构建包中的所有模块。idris2 --install test.ipkg会将包安装到全局 Idris 库目录（即$IDRIS2_PREFIX/idris-<version>/），使其modules字段中的模块可被其他 Idris 库和程序访问。注意，这不会安装任何可执行文件，仅安装库模块。idris2 --clean test.ipkg会清理中间构建文件。idris2 --mkdoc test.ipkg会为该包生成 HTML 文档，输出到build/docs。
安装 test 包后，可以通过命令行选项 --package test``（可简写为 ``-p test）访问。例如：
idris -p test Main.idr
Idris 会在哪里查找包？
已编译的包是包含已编译 TTC 文件的目录（参见 构建制品 部分）。源文件 *.idr 的目录结构会被保留到 TTC 文件中。
已编译的包可以全局安装（如上所述，位于 $IDRIS2_PREFIX/idris-<version>/），也可以本地安装（位于项目顶层工作目录下的 depends 子目录）。通过 -p pkgname 或包的 depends 字段指定的包会按如下顺序查找：
首先，Idris 会在
depends/pkgname-<version>中查找满足版本约束的包。如果本地未找到包，Idris 会在
$IDRIS2_PREFIX/idris-<version>/pkgname-<version>中查找。
在每种情况下，如果有多个版本满足约束，将选择版本号最高的那个。如果目录名中省略了包版本，则视为版本 0。
支持文件安装目录（Support file install directories）
如上所述，包可以全局或本地安装，以供其他项目依赖。在这两种情况下，Idris 2 会对包安装根目录下的两个特殊目录进行特殊处理，当其他 Idris 包依赖该包时会用到。
这两个目录分别是 lib 和 data。
下文中我们将这两个目录分别称为 pkgname-<version>/lib 和 pkgname-<version>/data。在所有情况下，这些文件夹可以位于依赖项目的本地 depends 目录下，也可以全局安装（可通过 idris2 --libdir 查询全局安装目录）。
库文件（Library files）
Idris 会在 pkgname-<version>/lib 目录下查找库文件。库文件是在依赖你库的可执行文件运行时需要存在的文件。也就是说，这些文件不会被内置到可执行文件中，而是在构建时链接或引用，并在运行时加载。常见的例子是共享对象文件（在 Linux 系统中通常为 .so，在 Mac OS 系统中为 .dylib）。
使用 Scheme 或 Refc 后端构建时，你可能希望包使用 Idris 2 的 C FFI，并依赖于 C 支持文件。FFI 接口的详细内容另有文档，这里不再赘述。当你有了用 C 编写的支持文件后，可以通过包的构建后钩子（post-build hook）生成 so 文件。然后，在安装后钩子（post-install hook）中，将该 so 文件复制到 Idris 安装包的 lib 子目录下。当可执行文件依赖你的包时，Idris 会将 lib 目录下的共享对象文件复制到可执行文件的构建目录。
数据文件（Data files）
Idris 会在 pkgname-<version>/data 目录下查找数据文件。数据文件的用途较为灵活。其中一个重要用例是为 Javascript FFI 添加支持文件。Javascript 支持文件与 C 支持文件不同，前者会被 内嵌 到可执行文件中，而不是与其并列安装。FFI 接口的详细内容另有文档，这里仅简要介绍如何通过 data 目录实现 JS 支持文件的端到端打包。
使用 NodeJS 后端构建时，可以通过 FFI 模式 node:support:my_func,my_lib 引用外部支持 JS 文件中定义的函数。该模式会促使 Idris 在所有已知的 data 目录下查找 js 文件夹及其中名为 my_lib.js 的文件。因此，你可以为包指定安装后钩子，将所需的支持 JS 文件复制到 pkgname-<version>/data/js 文件夹中，以便 Idris 之后将这些支持文件内嵌到依赖你包的 JS 可执行文件中。
注释（Comments）
包文件支持使用 Idris 标准的单行注释
--和多行注释{- -}格式。