调试编译器（Debugging The Compiler）
性能（Performance）
编译器提供了 --timing 标志，用于输出编译过程中收集的时间信息。
输出内容会以逆时间顺序记录操作（及其子操作）完成所用的累计时间。子级通过连续的 + 符号表示。
日志（Logging）
编译器在运行过程中会以不同级别记录各种类别的信息。
日志级别由两部分组成：
以点分隔的主题路径，例如 scope.let
一个表示详细程度的自然数，例如 5
如果用户通过如下方式请求日志：
%logging "scope" 5
他们会获得所有以 scope 开头且详细级别小于等于 5 的日志。通过组合不同的日志指令，用户既可以获取所有内容的简要信息，也可以聚焦于某个子系统的详细信息。例如：
%logging 1
%logging "scope.let" 10
这样会输出编译器各阶段的基本信息，并详细输出关于 let 绑定作用域检查的信息。
你可以通过命令行设置日志级别：
--log <level>
也可以在 REPL 中设置：
:log <string category> <level>
:logging <string category> <level>
可用的日志类别可通过以下命令行参数查看：
--help logging
REPL 命令
要在 REPL 中查看更多调试信息，可以设置以下选项。
命令 |
描述 |
|---|---|
|
显示指定名称的调试信息 |
|
显示隐式参数的值 |
编译器标志（Compiler Flags）
有一些"隐藏"的编译器标志可以帮助揭示 Idris 的内部工作机制。
命令 |
描述 |
|---|---|
|
将 case tree 输出到指定文件 |
|
将 lambda lifted tree 输出到指定文件 |
|
将 ANF 输出到指定文件 |
|
将 VM 代码输出到指定文件 |
|
执行更多 elaborator 检查（目前为 LinearCheck 中的转换检查） |
输出格式（Output Formats）
调试输出（Debug Output）
调用 :di <name> 会输出所选术语的调试信息。具体包括：
主题 |
描述 |
|---|---|
全名（Full Name(s)） |
术语的完全限定名。 |
多重性（Multiplicity） |
术语的多重性。 |
可擦除参数（Erasable Arguments） |
会被擦除的内容。 |
可去标签参数类型（Detaggable argument types） |
|
特殊参数（Specialised arguments） |
|
可推断参数（Inferrable arguments） |
|
已编译版本（Compiled version） |
|
编译时链接术语（Compile time linked terms） |
|
运行时链接术语（Runtime linked terms） |
|
标志（Flags） |
|
规模变化图（Size change graph） |