Skip to content

Commit

Permalink
Update index.md
Browse files Browse the repository at this point in the history
  • Loading branch information
@pitmonticone
pitmonticone committed Jul 30, 2024
1 parent 0100130 commit cc277bb
Showing 1 changed file with 32 additions and 32 deletions.
64 changes: 32 additions & 32 deletions docs/index.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,25 +12,25 @@ This repository contains a template for blueprint-based formalization projects i

The template repository is organized as follows (listing the main folders and files):

- [`.github`](.github) contains GitHub-specific configuration files and workflows.
- [`workflows`](.github/workflows) contains GitHub Actions workflow files.
- [`push_pr.yml`](.github/workflows/push_pr.yml) is the workflow triggered on pull request events.
- [`push.yml`](.github/workflows/push.yml) is the workflow triggered on push events.
- [`dependabot.yml`](.github/dependabot.yml) is the configuration to automate dependency updates.
- [`.vscode`](.vscode) contains Visual Studio Code configuration files
- [`extensions.json`](.vscode/extensions.json) recommends VS Code extensions for the project.
- [`settings.json`](.vscode/settings.json) defines the project-specific settings for VS Code.
- [`docs`](docs) contains the project website files.
- [`Project`](Project) should contain the Lean code files.
- [`Mathlib`](Project/Mathlib) should contain `.lean` files with declarations missing from existing Mathlib developments.
- [`Prereqs`](Project/Prereqs) should contain `.lean` files with new declarations to be upstreamed to Mathlib.
- [`Example.lean`](Project/Example.lean) is a sample Lean file.
- [`.gitignore`](.gitignore) specifies files and folders to be ignored by Git.
- [`.gitpod.yml`](.gitpod.yml) is the configuration file for Gitpod, defining workspace setup and environment.
- [`CONTRIBUTING.md`](CONTRIBUTING.md) should provide the guidelines for contributing to the project.
- [`lake-manifest.json`](lake-manifest.json) is the manifest file for the Lake build system, detailing dependencies and project metadata.
- [`lakefile.lean`](lakefile.lean) is the configuration file for the Lake build system used in Lean projects.
- [`lean-toolchain`](lean-toolchain) specifies the Lean version and toolchain used for the project.
- [`.github`](../.github) contains GitHub-specific configuration files and workflows.
- [`workflows`](../.github/workflows) contains GitHub Actions workflow files.
- [`push_pr.yml`](../.github/workflows/push_pr.yml) is the workflow triggered on pull request events.
- [`push.yml`](../.github/workflows/push.yml) is the workflow triggered on push events.
- [`dependabot.yml`](../.github/dependabot.yml) is the configuration to automate dependency updates.
- [`.vscode`](../.vscode) contains Visual Studio Code configuration files
- [`extensions.json`](../.vscode/extensions.json) recommends VS Code extensions for the project.
- [`settings.json`](../.vscode/settings.json) defines the project-specific settings for VS Code.
- [`docs`](../docs) contains the project website files.
- [`Project`](../Project) should contain the Lean code files.
- [`Mathlib`](../Project/Mathlib) should contain `.lean` files with declarations missing from existing Mathlib developments.
- [`Prereqs`](../Project/Prereqs) should contain `.lean` files with new declarations to be upstreamed to Mathlib.
- [`Example.lean`](../Project/Example.lean) is a sample Lean file.
- [`.gitignore`](../.gitignore) specifies files and folders to be ignored by Git.
- [`.gitpod.yml`](../.gitpod.yml) is the configuration file for Gitpod, defining workspace setup and environment.
- [`CONTRIBUTING.md`](../CONTRIBUTING.md) should provide the guidelines for contributing to the project.
- [`lake-manifest.json`](../lake-manifest.json) is the manifest file for the Lake build system, detailing dependencies and project metadata.
- [`lakefile.lean`](../lakefile.lean) is the configuration file for the Lake build system used in Lean projects.
- [`lean-toolchain`](../lean-toolchain) specifies the Lean version and toolchain used for the project.

## Use this Template

Expand All @@ -44,26 +44,26 @@ To create a new repository using this template, follow these steps:

To tailor this template to your specific project, you need to:

- [`push_pr.yml`](.github/workflows/push_pr.yml):
- [`push_pr.yml`](../.github/workflows/push_pr.yml):
- Find and replace `Project` with your actual project name.
- Select the default branch of your project repository (e.g. `main`) to enable the workflow triggered on pull requests targeting it
- [`push.yml`](.github/workflows/push.yml):
- Uncomment [these lines](.github/workflows/push.yml#L3-L4) and select the default branch of your project repository (e.g. `main`) to enable the workflow triggered on push events.
- [`push.yml`](../.github/workflows/push.yml):
- Uncomment [these lines](../.github/workflows/push.yml#L3-L4) and select the default branch of your project repository (e.g. `main`) to enable the workflow triggered on push events.
- Find and replace `Project` with your actual project name.
- [`docs/_layouts/default.html`](docs/_layouts/default.html): Find and replace `[ADD MAINTAINERS NAMES]` with the actual maintainers' names.
- [`docs/_config.yml`](docs/_config.yml):
- [`docs/_layouts/default.html`](../docs/_layouts/default.html): Find and replace `[ADD MAINTAINERS NAMES]` with the actual maintainers' names.
- [`docs/_config.yml`](../docs/_config.yml):
- Replace `Title` with the actual title for the project website.
- Replace `Description` with the actual description for the project website.
- Replace `https://pitmonticone.github.io/LeanProject/` with the actual URL for the project website.
- Replace `pitmonticone/LeanProject` with the actual GitHub repository.
- [`docs/index.md`](docs/index.md): Customise the content of the project website.
- [`Project`](Project): Rename the folder to match your actual project name.
- [`Project/Example.lean`](Project/Example.lean): Remove it and replace it with your actual project code.
- [`scripts/mk_all.sh`](scripts/mk_all.sh): Find and replace `Project` with your actual project name.
- [`CONTRIBUTING.md`](CONTRIBUTING.md): Customise the guidelines for contributing to the project.
- [`lake-manifest.json`](lake-manifest.json): Find and replace `Project` with your actual project name.
- [`lakefile.lean`](lakefile.lean): Find and replace `Project` with your actual project name.
- [`Project.lean`](Project.lean): Rename the file and the imports to match your actual project name.
- [`docs/index.md`](../docs/index.md): Customise the content of the project website.
- [`Project`](../Project): Rename the folder to match your actual project name.
- [`Project/Example.lean`](../Project/Example.lean): Remove it and replace it with your actual project code.
- [`scripts/mk_all.sh`](../scripts/mk_all.sh): Find and replace `Project` with your actual project name.
- [`CONTRIBUTING.md`](../CONTRIBUTING.md): Customise the guidelines for contributing to the project.
- [`lake-manifest.json`](../lake-manifest.json): Find and replace `Project` with your actual project name.
- [`lakefile.lean`](../lakefile.lean): Find and replace `Project` with your actual project name.
- [`Project.lean`](../Project.lean): Rename the file and the imports to match your actual project name.


## Configure GitHub Pages
Expand Down

0 comments on commit cc277bb

Please sign in to comment.