项目与导入

本指南介绍了如何创建新工作区、导入现有仓库，以及通过链接加入共享项目。ReasLab 支持为不同使用场景量身定制的多种专业项目模板。

登录后进入此页，展示你所具有的项目。

• ① 创建项目：通过侧栏的 New Project、Import Git 或模板库创建项目。
• ② 项目管理 tab：在此 tab 管理你的项目。
• ③ 过滤：在项目管理 tab 中，可以切换项目的过滤方式，包括所有项目、你所拥有的项目、分享给你的项目和归档的项目。你的项目可以归档，分享给你的项目可以离开共享。
• ④ Updates / Feedback：Updates 查看产品公告；Feedback 提交反馈，会作为 GitHub issue 创建。

创建新项目

ReasLab 提供了多种启动方式，无论您是想从零开始还是使用预配置的环境，都能找到合适的入口。

1. 创建空白项目 (New Project)

适用于通用的科学写作或自定义工程结构。通常点击 Dashboard 侧栏的 New Project。New Project 页面提供两个 tab：Blank Project 用于从零开始新建，Import from ZIP 用于上传已有的项目压缩包。

Blank Project（从零新建）

• ① 点击此按钮切换到新建项目的 tab。
• ② 在此输入项目名称（Project Name）。
• ③④ 在此区域进行项目配置：
  • ③ 选择 Project Type：Modeling、Theorem Proving 或 LaTeX。
  • ④ 选择 Theorem Proving 后，设置 Lean Toolchain Version，并可选 Include Mathlib。
• ⑤ 一切完成后，点击此按钮创建新项目。

Import from ZIP（从 ZIP 导入）

上传一个 .zip 压缩包，即可直接由其创建新项目。无需输入名称或选择类型：项目名称根据上传的文件名自动推导，项目类型（定理证明、LaTeX 或建模）会根据压缩包内容自动识别。

• ① 切换到 Import from ZIP tab。
• ② 点击上传或拖拽一个 .zip 压缩包（最大 95 MB）。上传后立即开始解压，完成后自动跳转到新建的项目。

如果已存在同名项目，系统会自动追加一小段随机后缀以保证名称唯一。

2. 通过数学建模模板创建

专为竞赛参与者设计，模板自带题目背景和报告结构。

• ① 按钮可以导航到数学建模模板区，包括上方和左方的按钮。
• ② 可以根据 categories 筛选合适的模板。
• ③ 是具体可以选择的模板，进入后可以预览模板内容，点击 Use Template 使用模板创建相应的项目。

3. 通过优化建模模板创建

快速引导带有数学模型和求解器配置的优化问题。系统内内置了 9 大优化问题类别以及 173 种子类的优化问题模板。您可以使用树状视图快速定位，最后点击 Use Template 创建属于自己的项目。

• ① 按钮可以导航到优化建模模板区，包括上方和左方的按钮。
• ② 可以根据 categories 筛选合适的模板。
• ③ 是具体可以选择的模板，进入后可以预览模板内容，点击 Use Template 使用模板创建相应的项目。

4. 通过 Lean (定理证明) 模板创建

使用预配置的 Lean 4 环境启动形式化验证项目。

• ① 导航到 Lean 模板库，左方和上方各一个按钮。
• ② 选择模板，点击 Use Template 使用模板创建项目。

从 Git 导入

可通过以下方式将已有仓库导入 ReasLab：

• ① 进入 Git tab，切换到 Git 导入界面。
• ② 输入仓库信息，输入 Git 地址，并进行项目配置，来导入项目。
• ③ 绑定自己的 GitHub 账号，从账号中直接读取项目列表，无需手动粘贴地址。现存系统将锚定于获取其设置为主分支 (Default Branch) 的资源树作为基础母版。

如需更高级的 Git 操作（分支管理、提交历史、冲突解决），请参阅 Git 集成指南。

通过分享链接加入

• 如果您拥有其他成员提供的高权限分享链接，直接在浏览器中打开链接并在登录账号后，即可按授予的权限（如查看、编辑、管理等）加入并在多人协作模式下共同工作。

详细请参阅 协作。