Agda User Manual v2.6.2.2

# 《Agda User Manual v2.6.2.2》总结 ## 1. 概述 Agda是一款支持类型论的功能性编程语言，其手册介绍了类型检查、编译和编辑系统的使用及相关资源。手册目前尚未完成，用户可通过GitHub参与贡献。 ## 2. 工具 ### 2.1 命令行选项 Agda提供多种命令行选项，用于定制编译和类型检查行为： - **库管理**： - `--include-path={DIR}`：指定导入路径。 - `--library={LIB}`：使用指定的库。 - `--no-default-libraries`或`--no-libraries`：禁用默认/所有库文件。 - `--local-interfaces`：在源文件旁存储接口文件，避免集中管理。 - **缓存**： - `--caching`或`--no-caching`：启用或禁用类型检查缓存，默认启用。 - **调试与打印**： - `--no-unicode`：禁用Unicode字符输出。 - `--show-implicit`/`--show-irrelevant`：显示隐含/不相关参数。 - `--verbose={N}`：设置冗长级别。 - **模式与投影**： - `--copatterns`：启用/禁用copattern匹配，默认启用。 - `--postfix-projections`：将后缀投影作为默认。 - **编译选项**： - `--compile-dir`：指定编译输出目录。 - `--with-compiler`：设置编译器路径，默认为GHC。 - `--no-main`：避免将模块视为程序入口。 - **代码高亮**： - `--html`、`--latex`、`--vim`：生成不同格式的高亮代码。 - `--css`、`--html-dir`、`--latex-dir`：定制输出路径和样式。 - **依赖与克隆**： - `--dependency-graph`：生成依赖图。 - `--count-clusters`：统计扩展图形集群，用于LaTeX生成。 ## 3. 库管理 Agda的包管理系统支持多库协同工作： - **库文件结构**： - 包含名称、依赖、导入路径和默认标志。 - 使用`.agda-lib`文件定义，示例： ```yaml name: library-name include: source/directory ``` - **配置文件**： - `AGDA_DIR/libraries`列出所有库： - 格式：`path/library-name.agda-lib` - 默认位置：~/.agda（Unix）或C:\Users\USERNAME\AppData\Roaming\agda（Windows）. - `AGDA_DIR/defaults`指定默认库： - 内容：`library-name` ## 4. 贡献指南 用户可通过GitHub Fork仓库并提交PR参与开发： - **开发者工具**： - 使用reStructuredText编写文档，位于`doc/user-manual`。 - 本地渲染需安装Sphinx，并运行： ```bash pip install --user -r doc/user-manual/requirements.txt ``` - **文档更新**： - 内容自动发布至[agda.readthedocs.io](https://agda.readthedocs.io)。 ## 5. 核心贡献者 主要贡献者包括Nils Anders Danielsson、Andrea Vezzosi、James Chapman、Olle Fredriksson等，他们在语言特性、编译器和库建设方面做出了重大贡献。 通过以上总结，用户能快速了解Agda的主要功能、配置方式及如何贡献代码和文档。