Initial commit
This commit is contained in:
Lean 4 VS Code Extension
commit
b51a19ee04
22
.github/workflows/create-release.yml
vendored
Normal file
22
.github/workflows/create-release.yml
vendored
Normal file
@ -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 }}
|
||||
21
.github/workflows/lean_action_ci.yml
vendored
Normal file
21
.github/workflows/lean_action_ci.yml
vendored
Normal file
@ -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@v7
|
||||
- uses: leanprover/lean-action@v1
|
||||
- uses: leanprover-community/docgen-action@v1
|
||||
41
.github/workflows/update.yml
vendored
Normal file
41
.github/workflows/update.yml
vendored
Normal file
@ -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
|
||||
1
.gitignore
vendored
Normal file
1
.gitignore
vendored
Normal file
@ -0,0 +1 @@
|
||||
/.lake
|
||||
1
Curso2026.lean
Normal file
1
Curso2026.lean
Normal file
@ -0,0 +1 @@
|
||||
import Curso2026.Basic
|
||||
1
Curso2026/Basic.lean
Normal file
1
Curso2026/Basic.lean
Normal file
@ -0,0 +1 @@
|
||||
def hello := "world"
|
||||
13
README.md
Normal file
13
README.md
Normal file
@ -0,0 +1,13 @@
|
||||
# curso2026
|
||||
|
||||
## 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.
|
||||
96
lake-manifest.json
Normal file
96
lake-manifest.json
Normal file
@ -0,0 +1,96 @@
|
||||
{"version": "1.3.0",
|
||||
"packagesDir": ".lake/packages",
|
||||
"packages":
|
||||
[{"url": "https://github.com/leanprover-community/mathlib4",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "625d8914199bc567cca9b91f90e8e5afafa5ae51",
|
||||
"name": "mathlib",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "v4.36.0-rc1",
|
||||
"inherited": false,
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/leanprover-community/plausible",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "c2d7840c65673533e15b499f25beecdc6227f7d8",
|
||||
"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": "9d39f9bb0c30aa2f6200808805ff16e6ce950890",
|
||||
"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": "b3cc36c295aa5e3e3c0197b09a6556298e710447",
|
||||
"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": "17137fad38a2cc782ff00b323a13c3a991d085ab",
|
||||
"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": "cbdde3aa2665915fb286c48bcd4cdf885c629511",
|
||||
"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": "6d26f8bb4b2bb78f929ad160feac508866821316",
|
||||
"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": "4453b52d2468f4c346a8711d728c0742e7483c9b",
|
||||
"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": "34d2efffcb6dc8d5f3537cf6a7f88bfaa999ec49",
|
||||
"name": "Cli",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "v4.36.0-rc1",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.toml"}],
|
||||
"name": "curso2026",
|
||||
"lakeDir": ".lake",
|
||||
"fixedToolchain": false}
|
||||
18
lakefile.toml
Normal file
18
lakefile.toml
Normal file
@ -0,0 +1,18 @@
|
||||
name = "curso2026"
|
||||
version = "0.1.0"
|
||||
keywords = ["math"]
|
||||
defaultTargets = ["Curso2026"]
|
||||
|
||||
[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.36.0-rc1"
|
||||
|
||||
[[lean_lib]]
|
||||
name = "Curso2026"
|
||||
1
lean-toolchain
Normal file
1
lean-toolchain
Normal file
@ -0,0 +1 @@
|
||||
leanprover/lean4:v4.36.0-rc1
|
||||
Loading…
Reference in New Issue
Block a user