From ad0082e18bd46635f1f15177a2c4bc9f14ac72ce Mon Sep 17 00:00:00 2001 From: Codex Bot Date: Thu, 5 Nov 2026 00:20:18 +0800 Subject: [PATCH] Import project source and Git ignore rules [skip ci] --- .github/workflows/create-release.yml | 22 +++++++ .github/workflows/lean_action_ci.yml | 21 ++++++ .github/workflows/update.yml | 41 ++++++++++++ .gitignore | 5 ++ MyMathProject.lean | 1 + MyMathProject/Basic.lean | 1 + README.md | 13 ++++ lake-manifest.json | 96 ++++++++++++++++++++++++++++ lakefile.toml | 18 ++++++ lean-toolchain | 1 + 10 files changed, 219 insertions(+) create mode 100644 .github/workflows/create-release.yml create mode 100644 .github/workflows/lean_action_ci.yml create mode 100644 .github/workflows/update.yml create mode 100644 .gitignore create mode 100644 MyMathProject.lean create mode 100644 MyMathProject/Basic.lean create mode 100644 README.md create mode 100644 lake-manifest.json create mode 100644 lakefile.toml create mode 100644 lean-toolchain diff --git a/.github/workflows/create-release.yml b/.github/workflows/create-release.yml new file mode 100644 index 0000000..6dacf77 --- /dev/null +++ b/.github/workflows/create-release.yml @@ -0,0 +1,22 @@ +name: Create Release + +on: + push: + branches: + - 'main' + - 'master' + paths: + - 'lean-toolchain' + +jobs: + lean-release-tag: + name: Add Lean release tag + runs-on: ubuntu-latest + permissions: + contents: write + steps: + - name: lean-release-tag action + uses: leanprover-community/lean-release-tag@v1 + with: + do-release: true + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml new file mode 100644 index 0000000..db09247 --- /dev/null +++ b/.github/workflows/lean_action_ci.yml @@ -0,0 +1,21 @@ +name: Lean Action CI + +on: + push: + pull_request: + workflow_dispatch: + +# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages +permissions: + contents: read # Read access to repository contents + pages: write # Write access to GitHub Pages + id-token: write # Write access to ID tokens + +jobs: + build: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v5 + - uses: leanprover/lean-action@v1 + - uses: leanprover-community/docgen-action@v1 diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml new file mode 100644 index 0000000..96b7622 --- /dev/null +++ b/.github/workflows/update.yml @@ -0,0 +1,41 @@ +name: Update Dependencies + +on: + # schedule: # Sets a schedule to trigger the workflow + # - cron: "0 8 * * *" # Every day at 08:00 AM UTC (see https://docs.github.com/en/actions/writing-workflows/choosing-when-your-workflow-runs/events-that-trigger-workflows#schedule) + workflow_dispatch: # Allows the workflow to be triggered manually via the GitHub interface + +jobs: + check-for-updates: # Determines which updates to apply. + runs-on: ubuntu-latest + outputs: + is-update-available: ${{ steps.check-for-updates.outputs.is-update-available }} + new-tags: ${{ steps.check-for-updates.outputs.new-tags }} + steps: + - name: Run the action + id: check-for-updates + uses: leanprover-community/mathlib-update-action@v1 + # START CONFIGURATION BLOCK 1 + # END CONFIGURATION BLOCK 1 + do-update: # Runs the upgrade, tests it, and makes a PR/issue/commit. + runs-on: ubuntu-latest + permissions: + contents: write # Grants permission to push changes to the repository + issues: write # Grants permission to create or update issues + pull-requests: write # Grants permission to create or update pull requests + needs: check-for-updates + if: ${{ needs.check-for-updates.outputs.is-update-available == 'true' }} + strategy: # Runs for each update discovered by the `check-for-updates` job. + max-parallel: 1 # Ensures that the PRs/issues are created in order. + matrix: + tag: ${{ fromJSON(needs.check-for-updates.outputs.new-tags) }} + steps: + - name: Run the action + id: update-the-repo + uses: leanprover-community/mathlib-update-action/do-update@v1 + with: + tag: ${{ matrix.tag }} + # START CONFIGURATION BLOCK 2 + on_update_succeeds: pr # Create a pull request if the update succeeds + on_update_fails: issue # Create an issue if the update fails + # END CONFIGURATION BLOCK 2 diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..7460395 --- /dev/null +++ b/.gitignore @@ -0,0 +1,5 @@ +/.lake + +.DS_Store +.env +.env.* diff --git a/MyMathProject.lean b/MyMathProject.lean new file mode 100644 index 0000000..2a0bc1f --- /dev/null +++ b/MyMathProject.lean @@ -0,0 +1 @@ +import MyMathProject.Basic diff --git a/MyMathProject/Basic.lean b/MyMathProject/Basic.lean new file mode 100644 index 0000000..99415d9 --- /dev/null +++ b/MyMathProject/Basic.lean @@ -0,0 +1 @@ +def hello := "world" diff --git a/README.md b/README.md new file mode 100644 index 0000000..b8f1d84 --- /dev/null +++ b/README.md @@ -0,0 +1,13 @@ +# my_math_project + +## GitHub configuration + +To set up your new GitHub repository, follow these steps: + +* Under your repository name, click **Settings**. +* In the **Actions** section of the sidebar, click "General". +* Check the box **Allow GitHub Actions to create and approve pull requests**. +* Click the **Pages** section of the settings sidebar. +* In the **Source** dropdown menu, select "GitHub Actions". + +After following the steps above, you can remove this section from the README file. diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..1d9cedf --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,96 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "5ed2965256430c3649e86755f9576b54eca72435", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.34.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707", + "name": "LeanSearchClient", + "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": "e928b72544873815af278d38681b31c0293588e3", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "355695d523e41d0554926416cba2a2b3544fbbc9", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.34.0", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "my_math_project", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..f73a61c --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,18 @@ +name = "my_math_project" +version = "0.1.0" +keywords = ["math"] +defaultTargets = ["MyMathProject"] + +[leanOptions] +pp.unicode.fun = true # pretty-prints `fun a ↦ b` +relaxedAutoImplicit = false +weak.linter.mathlibStandardSet = true +maxSynthPendingDepth = 3 + +[[require]] +name = "mathlib" +scope = "leanprover-community" +rev = "v4.34.0" + +[[lean_lib]] +name = "MyMathProject" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..12359f9 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.34.0