Skip to content

Commit c921cd4

Browse files
vyorkinvyorkin
committed
Let's go
1 parent 4685dc9 commit c921cd4

File tree

10 files changed

+213
-0
lines changed

10 files changed

+213
-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@v5
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 == 'true' }}
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

‎README.md‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
# tpil4
2+
3+
## GitHub configuration
4+
5+
To set up your new GitHub repository, follow these steps:
6+
7+
* Under your repository name, click **Settings**.
8+
* In the **Actions** section of the sidebar, click "General".
9+
* Check the box **Allow GitHub Actions to create and approve pull requests**.
10+
* Click the **Pages** section of the settings sidebar.
11+
* In the **Source** dropdown menu, select "GitHub Actions".
12+
13+
After following the steps above, you can remove this section from the README file.

‎Tpil4.lean‎

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

‎Tpil4/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": "056b90728ebef1bfa9677cb0151dbd7112262116",
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": "156c416202d8afc1c2ff45ceb4d42ac9b9ecf089",
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": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
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": "451499ea6e97cee4c8979b507a9af5581a849161",
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": "fb8ed0a85a96e3176f6e94b20d413ea72d92576d",
49+
"name": "proofwidgets",
50+
"manifestFile": "lake-manifest.json",
51+
"inputRev": "v0.0.77",
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": "ca519018e8bdc34d7bb4ecf0c8d39634a8c15300",
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": "95c2f8afe09d9e49d3cacca667261da04f7f93f7",
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": "091ff2379c7f0998aba1dc031a578810d44b9f3f",
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": "72ae7004d9f0ddb422aec5378204fdd7828c5672",
89+
"name": "Cli",
90+
"manifestFile": "lake-manifest.json",
91+
"inputRev": "v4.25.0-rc2",
92+
"inherited": true,
93+
"configFile": "lakefile.toml"}],
94+
"name": "tpil4",
95+
"lakeDir": ".lake"}

‎lakefile.toml‎

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

‎lean-toolchain‎

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

0 commit comments

Comments
 (0)