Skip to content

Commit de02e6f

Browse files
quantumshiroquantumshiro
committed
add: lean project
1 parent 1b7e7f4 commit de02e6f

File tree

9 files changed

+201
-0
lines changed

9 files changed

+201
-0
lines changed

‎.github/workflows/create-release.yml‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
name: Create Release
2+
3+
on:
4+
push:
5+
branches:
6+
- 'main'
7+
- 'master'
8+
paths:
9+
- 'lean-toolchain'
10+
11+
jobs:
12+
lean-release-tag:
13+
name: Add Lean release tag
14+
runs-on: ubuntu-latest
15+
permissions:
16+
contents: write
17+
steps:
18+
- name: lean-release-tag action
19+
uses: leanprover-community/lean-release-tag@v1
20+
with:
21+
do-release: true
22+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

‎.github/workflows/lean_action_ci.yml‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
name: Lean Action CI
2+
3+
on:
4+
push:
5+
pull_request:
6+
workflow_dispatch:
7+
8+
# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
9+
permissions:
10+
contents: read # Read access to repository contents
11+
pages: write # Write access to GitHub Pages
12+
id-token: write # Write access to ID tokens
13+
14+
jobs:
15+
build:
16+
runs-on: ubuntu-latest
17+
18+
steps:
19+
- uses: actions/checkout@v4
20+
- uses: leanprover/lean-action@v1
21+
- uses: leanprover-community/docgen-action@v1

‎.github/workflows/update.yml‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
name: Update Dependencies
2+
3+
on:
4+
# schedule: # Sets a schedule to trigger the workflow
5+
# - 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)
6+
workflow_dispatch: # Allows the workflow to be triggered manually via the GitHub interface
7+
8+
jobs:
9+
check-for-updates: # Determines which updates to apply.
10+
runs-on: ubuntu-latest
11+
outputs:
12+
is-update-available: ${{ steps.check-for-updates.outputs.is-update-available }}
13+
new-tags: ${{ steps.check-for-updates.outputs.new-tags }}
14+
steps:
15+
- name: Run the action
16+
id: check-for-updates
17+
uses: leanprover-community/mathlib-update-action@v1
18+
# START CONFIGURATION BLOCK 1
19+
# END CONFIGURATION BLOCK 1
20+
do-update: # Runs the upgrade, tests it, and makes a PR/issue/commit.
21+
runs-on: ubuntu-latest
22+
permissions:
23+
contents: write # Grants permission to push changes to the repository
24+
issues: write # Grants permission to create or update issues
25+
pull-requests: write # Grants permission to create or update pull requests
26+
needs: check-for-updates
27+
if: ${{ needs.check-for-updates.outputs.is-update-available }}
28+
strategy: # Runs for each update discovered by the `check-for-updates` job.
29+
max-parallel: 1 # Ensures that the PRs/issues are created in order.
30+
matrix:
31+
tag: ${{ fromJSON(needs.check-for-updates.outputs.new-tags) }}
32+
steps:
33+
- name: Run the action
34+
id: update-the-repo
35+
uses: leanprover-community/mathlib-update-action/do-update@v1
36+
with:
37+
tag: ${{ matrix.tag }}
38+
# START CONFIGURATION BLOCK 2
39+
on_update_succeeds: pr # Create a pull request if the update succeeds
40+
on_update_fails: issue # Create an issue if the update fails
41+
# END CONFIGURATION BLOCK 2

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
/.lake

‎TOTP.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
import TOTP.Basic

‎TOTP/Basic.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
def hello := "world"

‎lake-manifest.json‎

Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
{"version": "1.1.0",
2+
"packagesDir": ".lake/packages",
3+
"packages":
4+
[{"url": "https://github.com/leanprover-community/mathlib4",
5+
"type": "git",
6+
"subDir": null,
7+
"scope": "leanprover-community",
8+
"rev": "4a2cfa251229e07c20cdfb30efed40a7627fadac",
9+
"name": "mathlib",
10+
"manifestFile": "lake-manifest.json",
11+
"inputRev": "master",
12+
"inherited": false,
13+
"configFile": "lakefile.lean"},
14+
{"url": "https://github.com/leanprover-community/plausible",
15+
"type": "git",
16+
"subDir": null,
17+
"scope": "leanprover-community",
18+
"rev": "240eddc1bb31420fbbc57fe5cc579435c2522493",
19+
"name": "plausible",
20+
"manifestFile": "lake-manifest.json",
21+
"inputRev": "main",
22+
"inherited": true,
23+
"configFile": "lakefile.toml"},
24+
{"url": "https://github.com/leanprover-community/LeanSearchClient",
25+
"type": "git",
26+
"subDir": null,
27+
"scope": "leanprover-community",
28+
"rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
29+
"name": "LeanSearchClient",
30+
"manifestFile": "lake-manifest.json",
31+
"inputRev": "main",
32+
"inherited": true,
33+
"configFile": "lakefile.toml"},
34+
{"url": "https://github.com/leanprover-community/import-graph",
35+
"type": "git",
36+
"subDir": null,
37+
"scope": "leanprover-community",
38+
"rev": "dba7fbc707774d1ba830fd44d7f92a717e9bf57f",
39+
"name": "importGraph",
40+
"manifestFile": "lake-manifest.json",
41+
"inputRev": "main",
42+
"inherited": true,
43+
"configFile": "lakefile.toml"},
44+
{"url": "https://github.com/leanprover-community/ProofWidgets4",
45+
"type": "git",
46+
"subDir": null,
47+
"scope": "leanprover-community",
48+
"rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8",
49+
"name": "proofwidgets",
50+
"manifestFile": "lake-manifest.json",
51+
"inputRev": "v0.0.71",
52+
"inherited": true,
53+
"configFile": "lakefile.lean"},
54+
{"url": "https://github.com/leanprover-community/aesop",
55+
"type": "git",
56+
"subDir": null,
57+
"scope": "leanprover-community",
58+
"rev": "3b779e9d1c73837a3764d516d81f942de391b6f0",
59+
"name": "aesop",
60+
"manifestFile": "lake-manifest.json",
61+
"inputRev": "master",
62+
"inherited": true,
63+
"configFile": "lakefile.toml"},
64+
{"url": "https://github.com/leanprover-community/quote4",
65+
"type": "git",
66+
"subDir": null,
67+
"scope": "leanprover-community",
68+
"rev": "f85ad59c9b60647ef736719c23edd4578f723806",
69+
"name": "Qq",
70+
"manifestFile": "lake-manifest.json",
71+
"inputRev": "master",
72+
"inherited": true,
73+
"configFile": "lakefile.toml"},
74+
{"url": "https://github.com/leanprover-community/batteries",
75+
"type": "git",
76+
"subDir": null,
77+
"scope": "leanprover-community",
78+
"rev": "eebfdee629c3f3298929216d61839d4702524d42",
79+
"name": "batteries",
80+
"manifestFile": "lake-manifest.json",
81+
"inputRev": "main",
82+
"inherited": true,
83+
"configFile": "lakefile.toml"},
84+
{"url": "https://github.com/leanprover/lean4-cli",
85+
"type": "git",
86+
"subDir": null,
87+
"scope": "leanprover",
88+
"rev": "cacb481a1eaa4d7d4530a27b606c60923da21caf",
89+
"name": "Cli",
90+
"manifestFile": "lake-manifest.json",
91+
"inputRev": "main",
92+
"inherited": true,
93+
"configFile": "lakefile.toml"}],
94+
"name": "TOTP",
95+
"lakeDir": ".lake"}

‎lakefile.toml‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
name = "TOTP"
2+
version = "0.1.0"
3+
keywords = ["math"]
4+
defaultTargets = ["TOTP"]
5+
6+
[leanOptions]
7+
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
8+
autoImplicit = false
9+
relaxedAutoImplicit = false
10+
weak.linter.mathlibStandardSet = true
11+
maxSynthPendingDepth = 3
12+
13+
[[require]]
14+
name = "mathlib"
15+
scope = "leanprover-community"
16+
17+
[[lean_lib]]
18+
name = "TOTP"

‎lean-toolchain‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
leanprover/lean4:v4.23.0-rc2

0 commit comments

Comments
 (0)