From a7dfc781fd375a5c569baa9717f5daea9433963f Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 15 Sep 2025 11:15:39 +0200 Subject: [PATCH] initial commit --- .github/workflows/create-release.yml | 22 +++++++ .github/workflows/lean_action_ci.yml | 21 ++++++ .github/workflows/update.yml | 41 ++++++++++++ .gitignore | 1 + ColloquiumLean.lean | 1 + ColloquiumLean/Basic.lean | 1 + README.md | 13 ++++ lake-manifest.json | 95 ++++++++++++++++++++++++++++ lakefile.toml | 18 ++++++ lean-toolchain | 1 + 10 files changed, 214 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 ColloquiumLean.lean create mode 100644 ColloquiumLean/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..4962322 --- /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@v4 + - 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..9beea73 --- /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 }} + 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..bfb30ec --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/ColloquiumLean.lean b/ColloquiumLean.lean new file mode 100644 index 0000000..a7d7d34 --- /dev/null +++ b/ColloquiumLean.lean @@ -0,0 +1 @@ +import ColloquiumLean.Basic diff --git a/ColloquiumLean/Basic.lean b/ColloquiumLean/Basic.lean new file mode 100644 index 0000000..99415d9 --- /dev/null +++ b/ColloquiumLean/Basic.lean @@ -0,0 +1 @@ +def hello := "world" diff --git a/README.md b/README.md new file mode 100644 index 0000000..43495c6 --- /dev/null +++ b/README.md @@ -0,0 +1,13 @@ +# colloquium-lean + +## 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..597776a --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,95 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "e2a81062ed182504d3c853c09109e93b7916e97a", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "a22e7c1fa7707fb7ea75f2f9fd6b14de2b7b87a9", + "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": "99657ad92e23804e279f77ea6dbdeebaa1317b98", + "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": "7fca1d4a190761bac0028848f73dc9a59fcb4957", + "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": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.71", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "247ff80701c76760523b5d7c180b27b7708faf38", + "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": "9b703a545097978aef0e7e243ab8b71c32a9ff65", + "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": "d117e2c28cba42e974bc22568ac999492a34e812", + "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": "41c5d0b8814dec559e2e1441171db434fe2281cc", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "«colloquium-lean»", + "lakeDir": ".lake"} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..6685d85 --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,18 @@ +name = "colloquium-lean" +version = "0.1.0" +keywords = ["math"] +defaultTargets = ["ColloquiumLean"] + +[leanOptions] +pp.unicode.fun = true # pretty-prints `fun a ↦ b` +autoImplicit = false +relaxedAutoImplicit = false +weak.linter.mathlibStandardSet = true +maxSynthPendingDepth = 3 + +[[require]] +name = "mathlib" +scope = "leanprover-community" + +[[lean_lib]] +name = "ColloquiumLean" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..7f254a9 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.23.0