diff --git a/.github/dependabot.yml b/.github/dependabot.yml new file mode 100644 index 0000000..a02a559 --- /dev/null +++ b/.github/dependabot.yml @@ -0,0 +1,9 @@ +version: 2 # Specifies the version of the Dependabot configuration file format + +updates: + # Configuration for dependency updates + - package-ecosystem: "github-actions" # Specifies the ecosystem to check for updates + directory: "/" # Specifies the directory to check for dependencies; "/" means the root directory + schedule: + # Check for updates to GitHub Actions every weekday + interval: "monthly" \ No newline at end of file diff --git a/.github/workflows/lint.yml b/.github/workflows/lint.yml new file mode 100644 index 0000000..62a9e0d --- /dev/null +++ b/.github/workflows/lint.yml @@ -0,0 +1,30 @@ +name: Lint Style + +on: + push: + branches: ["main"] # Trigger the workflow on pushes to the "main" branch (replace "main" with your default branch if different) + pull_request: + branches: ["main"] # Trigger the workflow on pull requests targeting the "main" branch (replace "main" with your default branch if different) + workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface + +# Set permissions for the workflow +permissions: + contents: read # Grant read access to repository contents + pages: write # Grant write access to GitHub Pages + id-token: write # Grant write access to ID tokens + +jobs: + style_lint: + runs-on: ubuntu-latest + steps: + - name: Check for long lines + if: always() # Ensure the step runs regardless of the success or failure of previous steps + run: | + # Find Lean files with lines longer than 100 characters, excluding URLs + ! (find Project -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://') + + - name: Don't 'import Mathlib', use precise imports + if: always() # Ensure the step runs regardless of the success or failure of previous steps + run: | + # Find and disallow any file that imports the entire Mathlib, encouraging precise imports instead + ! (find Project -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$') diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..4e412e6 --- /dev/null +++ b/.gitignore @@ -0,0 +1,38 @@ +## macOS +.DS_Store +## Lake +.lake/* +.cache/* +## Blueprint +/blueprint/print/print.log +/blueprint/web/ +/blueprint/src/web.paux +/blueprint/src/web.bbl +/blueprint/print/ +## Docs +docs/_includes/sorries.md +## TeX +*.aux +*.lof +*.log +*.lot +*.fls +*.out +*.toc +*.fmt +*.fot +*.cb +*.cb2 +.*.lb +*.bbl +*.bcf +*.blg +*-blx.aux +*-blx.bib +*.run.xml +*.fdb_latexmk +*.synctex +*.synctex(busy) +*.synctex.gz +*.synctex.gz(busy) +*.pdfsync diff --git a/.vscode/extensions.json b/.vscode/extensions.json new file mode 100644 index 0000000..acf12cd --- /dev/null +++ b/.vscode/extensions.json @@ -0,0 +1,12 @@ +{ + // Learn about workspace recommendations at: + // https://go.microsoft.com/fwlink/?LinkId=827846 + + // The extension identifier format is ${publisher}.${name} + // Example: vscode.csharp + + // List of extensions that should be recommended for users of this workspace + "recommendations": [ + "leanprover.lean4" // Extension for Lean 4 support + ] +} diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 0000000..8151de4 --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,18 @@ +{ + // Configure editor to insert spaces when pressing Tab + "editor.insertSpaces": true, + // Set the number of spaces per tab + "editor.tabSize": 2, + // Display vertical rulers at specified character column for readability + "editor.rulers": [100], + // Set the default file encoding to UTF-8 + "files.encoding": "utf8", + // Use Unix-style line endings ('\n') by default + "files.eol": "\n", + // Ensure a final newline at the end of files + "files.insertFinalNewline": true, + // Trim final newlines at the end of files + "files.trimFinalNewlines": true, + // Remove any trailing whitespace on save + "files.trimTrailingWhitespace": true +} \ No newline at end of file diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 0000000..51c2255 --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,7 @@ +# Contributing to [Project] + +Thank you for your interest in contributing to [Project]! We welcome contributions from the +community and appreciate your efforts to improve the project. Please follow the guidelines below +to ensure a smooth contribution process. + +... \ No newline at end of file diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..261eeb9 --- /dev/null +++ b/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/Project.lean b/Project.lean new file mode 100644 index 0000000..570fa40 --- /dev/null +++ b/Project.lean @@ -0,0 +1 @@ +import Project.Example diff --git a/Project/Example.lean b/Project/Example.lean new file mode 100644 index 0000000..e69de29 diff --git a/Project/ForMathlib/README.md b/Project/ForMathlib/README.md new file mode 100644 index 0000000..1219fe3 --- /dev/null +++ b/Project/ForMathlib/README.md @@ -0,0 +1,3 @@ +# ForMathlib + +This folder contains `.lean` files with new declarations to be upstreamed to Mathlib. diff --git a/Project/Mathlib/README.md b/Project/Mathlib/README.md new file mode 100644 index 0000000..4b01692 --- /dev/null +++ b/Project/Mathlib/README.md @@ -0,0 +1,3 @@ +# Mathlib + +This folder contains `.lean` files with declarations missing from existing Mathlib developments. \ No newline at end of file diff --git a/README.md b/README.md new file mode 100644 index 0000000..66c30bd --- /dev/null +++ b/README.md @@ -0,0 +1,190 @@ +# Lean 4 Project Template + +[![License: Apache 2.0](https://img.shields.io/badge/License-Apache_2.0-lightblue.svg)](https://opensource.org/licenses/Apache-2.0) + +This repository contains a template for blueprint-driven formalization projects in Lean 4. + +## Tutorial Talk Video + +This is the video recording of the tutorial talk I presented at the Hausdorff Research Institute for Mathematics ([HIM](https://www.mathematics.uni-bonn.de/him)) in Bonn. + +It was designed for mathematicians at all levels to provide a comprehensive introduction to the design, management, and implementation of blueprint-driven formalisation projects in Lean, with almost no prerequisite knowledge of Git, GitHub, continuous integration systems, and other technical tools. + +[![HIM 2024 Tutorial Talk](https://img.youtube.com/vi/KyuyTsLgkMY/maxresdefault.jpg)](https://youtu.be/KyuyTsLgkMY) + +## Install Lean 4 + +Ensure that you have a functioning Lean 4 installation. If you do not, please follow +the [Lean installation guide](https://leanprover-community.github.io/get_started.html). + +## Use this Template + +To create a new repository using this template, ensure you are on the correct repository page ([LeanProject](https://github.com/pitmonticone/LeanProject)) and then follow these steps: + +1. Click the **Use this template** button located at the top right of the repository page. +2. Click the **Create a new repository** button. +3. Select the account or organization where you want to create it, choose a name for the new +repository, and click the **Create repository** button. + +## Configure GitHub Pages + +To set up GitHub Pages for your repository, follow these steps: + +1. Go to the **Settings** tab of your repository. +2. In the left sidebar, click on the **Pages** section. +3. In the **Source** dropdown, select `GitHub Actions`. + +## Clone this Repository + +To clone this repository to your local machine, please refer to the relevant section of the GitHub documentation [here](https://docs.github.com/en/repositories/creating-and-managing-repositories/cloning-a-repository). + +## Repository Layout + +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. + - [`lint.yml`](.github/workflows/lint.yml) is the style lint workflow triggered on push + and pull request events. + - [`dependabot.yml`](.github/dependabot.yml) is the configuration file to automate CI 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. +- [`Project`](Project) should contain the Lean code files. + - [`Mathlib`](Project/Mathlib) should contain `.lean` files with declarations missing from + existing Mathlib developments. + - [`ForMathlib`](Project/ForMathlib) should contain `.lean` files with new declarations to + be upstreamed to Mathlib. + - [`Example.lean`](Project/Example.lean) is a sample Lean file. +- [`scripts`](scripts) contains scripts to update Mathlib ensuring that the latest version is fetched and integrated into the development environment. +- [`.gitignore`](.gitignore) specifies files and folders to be ignored by Git. +and environment. +- [`CONTRIBUTING.md`](CONTRIBUTING.md) should provide the guidelines for contributing to the +project. +- [`lakefile.toml`](lakefile.toml) 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. + +## Customize this Template + +To tailor this template to your specific project, follow these steps: + +1. Ensure your terminal is in the project directory by running the following command: + ```bash + cd path/to/your/project + ``` +2. Execute the customization script by running: + ```bash + python3 scripts/customize_template.py NewProject + ``` + where `NewProject` must be replaced by the name of your project. + +The script [`customize_template.py`](scripts/customize_template.py) will automatically rename the project folder and update the necessary files and configurations to match the new project name. + +## Blueprint + +### 0. Selected Real-World Collaborative Projects + +- [Fermat's Last Theorem for Exponent 3](https://pitmonticone.github.io/FLT3/) +- [Polynomial Freiman-Ruzsa Conjecture](https://github.com/teorth/pfr) +- [Fermat's Last Theorem](https://imperialcollegelondon.github.io/FLT/) +- [Carleson Operators on Doubling Metric Measure Spaces](http://florisvandoorn.com/carleson/) +- [Bonn Collaborative Formalization Seminar Series in Analysis](https://github.com/fpvandoorn/BonnAnalysis) +- [Prime Number Theorem and More](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd) + +For more examples of completed and ongoing Lean projects and libraries, please +see the [Lean Reservoir](https://reservoir.lean-lang.org). + +### 1. Install Dependencies + +Verify your Python installation by running: + +```bash +python3 --version +``` + +and your Pip installation by running: + +```bash +pip3 --version +``` + +If you don't have a Python environment, you can install one by following the instructions in the +[Python installation guide](https://www.python.org/downloads/). + +To install the necessary dependencies, follow the instructions in the +[PyGraphViz installation guide](https://pygraphviz.github.io/documentation/stable/install.html). + +### 2. Install LeanBlueprint Package + +Assuming you have a properly configured Python environment, install LeanBlueprint by running: + +```bash +pip install leanblueprint +``` + +If you have an existing installation of LeanBlueprint, you can upgrade to the latest version by +running: + +```bash +pip install -U leanblueprint +``` + +### 3. Configure Blueprint + +To set up the blueprint for your project, run: + +```bash +leanblueprint new +``` + +Then, follow the prompts and answer the questions as you like, except for a few specific +questions which should be answered as indicated below to ensure compatibility with this template. + +Respond affirmatively with `y` to the following prompt: + +```console +Proceed with blueprint creation? [y/n] +``` + +Respond affirmatively with `y` to the following prompt: + +```console +Modify lakefile and lake-manifest to allow checking declarations exist? [y/n] (y) +``` + +Respond affirmatively with `y` to the following prompt: + +```console +Modify lakefile and lake-manifest to allow building the documentation? [y/n] (y): +``` + +If you want to generate a Jekyll-based home page for the project, respond +affirmatively with `y` to the following prompt: + +```console +Do you want to create a home page for the project, with links to the blueprint, the API documentation and the repository? [y/n]: +``` + +Respond affirmatively with `y` to the following prompt: + +```console +Configure continuous integration to compile blueprint? [y/n] (y): +``` + +For more details about the LeanBlueprint package and its commands, please refer to its +[documentation](https://github.com/PatrickMassot/leanblueprint/tree/master#starting-a-blueprint). + +After configuring the blueprint, please wait for the GitHub Action workflow to finish. +You can keep track of the progress in the **Actions** tab of your repository. + +## Projects Using this Template + +- [Infinity Cosmos](https://github.com/emilyriehl/infinity-cosmos) led by +[Emily Riehl](https://github.com/emilyriehl). +- [Analytic Number Theory Exponent Database](https://github.com/teorth/expdb) led by +[Terence Tao](https://github.com/teorth) +- [Groupoid Model of Homotopy Type Theory](https://github.com/sinhp/GroupoidModelofHoTTinLean4) +led by [Sina Hazratpour](https://github.com/sinhp) +- [Soundness of FRI](https://github.com/BoltonBailey/FRISoundness) led by [Bolton Bailey](https://github.com/BoltonBailey) diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..db57ae2 --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,75 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "d747f070e42dd21e2649b75090f5b0d45c6ec8e0", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "9339d48cc3b7431b6353af47f303691e9d4da229", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "a96aee5245720f588876021b6a0aa73efee49c76", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.41", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "add4983f36eb4aa1f8b4700300e6fd8edd0b6bdc", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": null, + "inherited": false, + "configFile": "lakefile.lean"}], + "name": "Project", + "lakeDir": ".lake"} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..281da52 --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,14 @@ +name = "Project" +defaultTargets = ["Project"] + +[leanOptions] +pp.unicode.fun = true +autoImplicit = false +relaxedAutoImplicit = false + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4.git" + +[[lean_lib]] +name = "Project" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..e7a4f40 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.11.0-rc2 diff --git a/scripts/customize_template.py b/scripts/customize_template.py new file mode 100644 index 0000000..4b2b2c7 --- /dev/null +++ b/scripts/customize_template.py @@ -0,0 +1,83 @@ +import os +import shutil +import sys + +def replace_text_in_file(filepath, old_text, new_text): + """ + Replace all occurrences of old_text with new_text in the specified file. + + Arguments: + filepath (str): The path to the file where text needs to be replaced. + old_text (str): The text to be replaced. + new_text (str): The text to replace with. + """ + with open(filepath, 'r') as file: + filedata = file.read() + + filedata = filedata.replace(old_text, new_text) + + with open(filepath, 'w') as file: + file.write(filedata) + +def rename_directory(old_name, new_name): + """ + Rename a directory from old_name to new_name. + + Arguments: + old_name (str): The current name of the directory. + new_name (str): The new name for the directory. + """ + if os.path.exists(old_name): + os.rename(old_name, new_name) + +# def remove_file(filepath): +# """ +# Remove the specified file. + +# Arguments: +# filepath (str): The path to the file to be removed. +# """ +# if os.path.exists(filepath): +# os.remove(filepath) + +def main(project_name): + """ + Perform all the customization steps for the template. + + Arguments: + project_name (str): The name of the new project. + """ + # Define paths to the files and directories to be modified + lint_yml_path = '.github/workflows/lint.yml' + project_folder = 'Project' + example_file = os.path.join(project_folder, 'Example.lean') + contributing_md = 'CONTRIBUTING.md' + lakefile_toml = 'lakefile.toml' + project_lean = 'Project.lean' + + # Replace 'Project' with the actual project name in the necessary files + replace_text_in_file(lint_yml_path, 'Project', project_name) + replace_text_in_file(lakefile_toml, 'Project', project_name) + + # Rename 'Project' folder to match the project name + rename_directory(project_folder, project_name) + + # Notify the user to customize 'CONTRIBUTING.md' manually + print(f"Please customize {contributing_md} manually to set up the contribution guidelines for your project.") + + # Rename 'Project.lean' to match the project name and update imports + if os.path.exists(project_lean): + new_project_lean = f"{project_name}.lean" + os.rename(project_lean, new_project_lean) + replace_text_in_file(new_project_lean, 'Project', project_name) + +if __name__ == "__main__": + # Check if the script is executed with the correct number of command-line arguments + if len(sys.argv) != 2: + print("Usage: python customize_template.py ") + sys.exit(1) + + # Get the project name from the command-line arguments + project_name = sys.argv[1] + # Call the main function to perform the customization + main(project_name) diff --git a/scripts/update_mathlib.bat b/scripts/update_mathlib.bat new file mode 100644 index 0000000..48cd735 --- /dev/null +++ b/scripts/update_mathlib.bat @@ -0,0 +1,12 @@ +@echo off +rem Update Mathlib and the Lean toolchain. + +rem Download the latest lean-toolchain file from the Mathlib4 repository +curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain + +rem Update the Mathlib dependencies and ensure doc-gen is also updated +rem The `-Kenv=dev` flag ensures that the development environment is updated, including doc-gen +lake -Kenv=dev update + +rem Retrieve and cache the latest Mathlib dependencies +lake exe cache get \ No newline at end of file diff --git a/scripts/update_mathlib.sh b/scripts/update_mathlib.sh new file mode 100644 index 0000000..f24c177 --- /dev/null +++ b/scripts/update_mathlib.sh @@ -0,0 +1,11 @@ +# Update Mathlib and the Lean toolchain. + +# Download the latest lean-toolchain file from the Mathlib4 repository +curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain + +# Update the Mathlib dependencies and ensure doc-gen is also updated +# The `-Kenv=dev` flag ensures that the development environment is updated, including doc-gen +lake -Kenv=dev update + +# Retrieve and cache the latest Mathlib dependencies +lake exe cache get \ No newline at end of file