CoqPilot 项目安装与使用教程

1. 项目目录结构及介绍

CoqPilot 是一个开源项目，旨在帮助自动化 Coq 证明的编写。项目的主要目录结构如下：

• .github/: 包含 GitHub 工作流程文件。
• .vscode/: 包含 Visual Studio Code 的配置文件。
• dataset/: 存储数据集。
• etc/: 存储一些杂项配置或脚本。
• src/: 源代码目录，包含项目的核心逻辑。
• .gitignore: 指定 Git 忽略的文件和目录。
• .gitmodules: 如果项目包含子模块，此文件会列出它们。
• .nvmrc: 指定 Node.js 的版本。
• .prettierrc.json: Prettier 的配置文件。
• .vscodeignore: Visual Studio Code 忽略的文件和目录。
• CHANGELOG.md: 记录项目的历史更新和修改。
• CNAME: 用于自定义项目页面的域名。
• LICENSE.md: 项目使用的许可证信息。
• README.md: 项目说明文件。
• _config.yml: 可能用于配置项目站点的一些元数据。
• eslint.config.mjs: ESLint 的配置文件。
• package-lock.json: 记录 Node.js 项目依赖的精确版本。
• package.json: 定义 Node.js 项目的依赖和脚本。
• tsconfig.json: TypeScript 的配置文件。

2. 项目的启动文件介绍

CoqPilot 项目的启动主要是通过 npm 脚本来完成的。在项目根目录下，你可以通过以下命令来编译和运行项目：

npm run compile # 编译项目
npm run start # 启动项目

这些脚本定义在 package.json 文件中，通常会使用 Node.js 来执行。

3. 项目的配置文件介绍

CoqPilot 的配置主要通过 settings.json 文件来完成。以下是一些主要的配置选项：

• coqpilot.contextTheoremsRankerType: 选择定理排名器的类型，用于选择用于证明生成的定理。
• coqpilot.loggingVerbosity: 设置日志的详细程度。
• coqpilot.coqLspServerPath: 指定 coq-lsp 服务器的路径。
• coqpilot.predefinedProofsModelsParameters: 预定义证明的模型参数配置。
• coqpilot.openAiModelsParameters: OpenAI 模型的参数配置。
• coqpilot.grazieModelsParameters: Grazie 平台模型的参数配置。
• coqpilot.lmStudioModelsParameters: LM Studio 模型的参数配置。

这些配置项允许用户根据需要调整项目的行为和性能。确保在修改配置后重新启动项目以应用更改。