Skip to content

Commit 00ad714

Browse files
kencykekencyke
authored
Merge pull request #3 from kencyke/bump-v4.25.1
Bump lean to v4.25.1
2 parents bd487ea + af4f6e0 commit 00ad714

File tree

14 files changed

+2832
-40
lines changed

14 files changed

+2832
-40
lines changed

‎.devcontainer/Dockerfile‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,3 +7,12 @@ RUN SNIPPET="export PROMPT_COMMAND='history -a' && export HISTFILE=/commandhisto
77
&& touch /commandhistory/.bash_history \
88
&& chown -R $USERNAME /commandhistory \
99
&& echo "$SNIPPET" >> "/home/$USERNAME/.bashrc"
10+
11+
RUN apt-get update && \
12+
apt install -y ripgrep
13+
14+
USER vscode
15+
WORKDIR /home/vscode
16+
17+
RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.25.1
18+
ENV PATH="/home/vscode/.elan/bin:${PATH}"

‎.devcontainer/devcontainer.json‎

Lines changed: 22 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,16 @@
77
"dockerfile": "Dockerfile"
88
},
99
// Features to add to the dev container. More info: https://containers.dev/features.
10-
// "features": {},
11-
"postStartCommand": "bash .devcontainer/setup-lean.sh",
10+
"features": {
11+
"ghcr.io/devcontainers/features/python:1": {
12+
"version": "3.13",
13+
"toolsToInstall": "uv"
14+
},
15+
"ghcr.io/devcontainers/features/node:1": {
16+
"version": "22"
17+
}
18+
},
19+
"postStartCommand": "rm -rf .lake/ && lake exe cache get && npm ci",
1220
"mounts": [
1321
"source=lean-project-commandhistory,target=/commandhistory,type=volume"
1422
],
@@ -17,36 +25,38 @@
1725
"vscode": {
1826
"extensions": [
1927
"leanprover.lean4",
20-
"github.copilot",
21-
"github.copilot-chat"
28+
// Opt out of extensions installed via features
29+
"-dbaeumer.vscode-eslint",
30+
"-ms-python.python",
31+
"-ms-python.vscode-pylance",
32+
"-ms-python.autopep8"
2233
],
2334
"settings": {
2435
"terminal.integrated.allowChords": false,
2536
"files.eol": "\n",
2637
"files.insertFinalNewline": true,
2738
"editor.renderWhitespace": "all",
2839
"editor.formatOnSave": true,
29-
// "github.copilot.chat.localeOverride": "ja",
30-
// "github.copilot.chat.agent.thinkingTool": true,
31-
// "chat.agent.maxRequests": 50,
40+
"github.copilot.chat.agent.thinkingTool": true,
41+
"chat.agent.maxRequests": 50,
42+
"chat.tools.autoApprove": true,
3243
"chat.tools.terminal.autoApprove": {
3344
"lean": true,
3445
"lake": true,
3546
"elan": true,
3647
"echo": true,
3748
"cd": true,
3849
"ls": true,
39-
"cat": true,
4050
"pwd": true,
4151
"find": true,
4252
"grep": true,
4353
"head": true,
44-
"xargs": true
54+
"xargs": true,
55+
"sed": true,
56+
"nl": true,
57+
"rg": true
4558
}
4659
}
4760
}
48-
},
49-
"remoteEnv": {
50-
"PATH": "${containerEnv:PATH}:/home/vscode/.elan/bin"
5161
}
5262
}

‎.devcontainer/setup-lean.sh‎

Lines changed: 0 additions & 5 deletions
This file was deleted.

‎.gitignore‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1 +1,3 @@
11
/.lake
2+
node_modules/
3+
lefthook-local.yml

‎.lefthook/prepare-commit-msg/commitizen.sh‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
#!/usr/bin/bash
2+
3+
set -eu
4+
5+
first_line=$(head -n1 $1)
6+
if [[ "${first_line}" != "" ]]; then
7+
exit 0
8+
fi
9+
10+
exec < /dev/tty && node_modules/.bin/cz --hook || true

‎.npmrc‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
save-exact=true

‎AGENT.md‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
# AGENTS.md
2+
3+
## Important Instructions
4+
5+
- Do not add files.
6+
- Do not remove files.
7+
- Do not use `git checkout`and `git reset`.
8+
- Do not use `python` command.
9+
- Do not use `cat` to overwrite a file.
10+
- Do not modify `lakefile.toml`.
11+
- Never use `axiom` and `set_option` for any reason!
12+
- When `lemma` or `thorem` is too long, devide it into multiple `lemma`s.
13+
- Never give up simply because it is complicated or time-consuming; instead, try to implement the missing lemmas step by step.
14+
- Use `$...$` or `$$...$$` for LaTeX math formatting in markdown.
15+
- Use `conj` as complex conjugate when declaring `open ComplexConjugate`.
16+
- Use `simp` when referring `try 'simp' instead of 'simpa'`.
17+
- Fix indentation when referring `expected '{' or indented tactic sequence`.
18+
- Do not use tabs. Use spaces instead.

‎README.md‎

Lines changed: 22 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,28 @@
11
# lean-project
22

3+
```bash
4+
$ lake build
5+
Build completed successfully (574 jobs).
36
```
4-
$ lake build Project/Example.lean
5-
Build completed successfully.
6-
```
7-
If you need further information, see https://lean-lang.org/.
87

9-
## Customize Copilot Instructions
8+
## How to use
9+
10+
1. Create a repository from this template.
11+
2. Confirm lint settings in `package.json`, `.lefthook/`, and `lefthook.yml`.
12+
3. Remove `Project.lean` and `Project/`.
13+
4. Make your project files, then update `lakefile.toml`.
14+
5. Bump lean version in `.devcontainer/Dockerfile`, `lakefile.toml`, and `lean-toolchain`.
15+
6. Reomve `lake-manifest.json` and `.lake/`.
16+
7. Execute `lake exe cache get`.
17+
18+
## Recommend to use
19+
20+
### VSCode Extensions
21+
22+
- [ms-vscode-remote.remote-containers](https://marketplace.visualstudio.com/items?itemName=ms-vscode-remote.remote-containers)
23+
- [github.copilot](https://marketplace.visualstudio.com/items?itemName=GitHub.copilot)
24+
- [github.copilot-chat](https://marketplace.visualstudio.com/items?itemName=GitHub.copilot-chat)
1025

11-
Make sure your vscode settings `github.copilot.chat.codeGeneration.useInstructionFiles` is `true`, and add `.github/copilot-instructions.md`. If you need further information, see below:
12-
- https://code.visualstudio.com/docs/copilot/copilot-customization
13-
- https://code.visualstudio.com/docs/copilot/reference/copilot-settings
26+
### MCP Servers
1427

15-
If you want to customize chatmode, for example, see https://burkeholland.github.io/posts/beast-mode-3-1/.
28+
- https://github.com/oOo0oOo/lean-lsp-mcp

‎lake-manifest.json‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -5,17 +5,17 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "leanprover-community",
8-
"rev": "928758ac3743dc7f171fc66f450506723896f1c5",
8+
"rev": "0df2e3c2047ada0d7a2e33dbc6ba2788a44a6062",
99
"name": "mathlib",
1010
"manifestFile": "lake-manifest.json",
11-
"inputRev": "v4.22.0-rc4",
11+
"inputRev": "v4.25.1",
1212
"inherited": false,
1313
"configFile": "lakefile.lean"},
1414
{"url": "https://github.com/leanprover-community/plausible",
1515
"type": "git",
1616
"subDir": null,
1717
"scope": "leanprover-community",
18-
"rev": "c37191eba2da78393070da8c4367689d8c4276e4",
18+
"rev": "0203092c2e5e26edf967000f0e177cf31c72e17a",
1919
"name": "plausible",
2020
"manifestFile": "lake-manifest.json",
2121
"inputRev": "main",
@@ -25,7 +25,7 @@
2525
"type": "git",
2626
"subDir": null,
2727
"scope": "leanprover-community",
28-
"rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
28+
"rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
2929
"name": "LeanSearchClient",
3030
"manifestFile": "lake-manifest.json",
3131
"inputRev": "main",
@@ -35,7 +35,7 @@
3535
"type": "git",
3636
"subDir": null,
3737
"scope": "leanprover-community",
38-
"rev": "4241928fd3ebae83a037a253e39d9b773e34c3b4",
38+
"rev": "3611075024b3529e5798e53c733671039f06f0bd",
3939
"name": "importGraph",
4040
"manifestFile": "lake-manifest.json",
4141
"inputRev": "main",
@@ -45,17 +45,17 @@
4545
"type": "git",
4646
"subDir": null,
4747
"scope": "leanprover-community",
48-
"rev": "96c67159f161fb6bf6ce91a2587232034ac33d7e",
48+
"rev": "135329b50b116dcc2c021c318c365e82a048856f",
4949
"name": "proofwidgets",
5050
"manifestFile": "lake-manifest.json",
51-
"inputRev": "v0.0.67",
51+
"inputRev": "v0.0.80",
5252
"inherited": true,
5353
"configFile": "lakefile.lean"},
5454
{"url": "https://github.com/leanprover-community/aesop",
5555
"type": "git",
5656
"subDir": null,
5757
"scope": "leanprover-community",
58-
"rev": "0a136f764a5dfedc4498e93ad8e297cff57ba2fc",
58+
"rev": "a2e4d9e9aebdbdce1ce6b6f0a19dd49e0120c990",
5959
"name": "aesop",
6060
"manifestFile": "lake-manifest.json",
6161
"inputRev": "master",
@@ -65,7 +65,7 @@
6565
"type": "git",
6666
"subDir": null,
6767
"scope": "leanprover-community",
68-
"rev": "1ef3dac0f872ca6aaa7d02e015427e06dd0b6195",
68+
"rev": "9bff22d64abde45944c7b1f55bce6c89dd8307e6",
6969
"name": "Qq",
7070
"manifestFile": "lake-manifest.json",
7171
"inputRev": "master",
@@ -75,7 +75,7 @@
7575
"type": "git",
7676
"subDir": null,
7777
"scope": "leanprover-community",
78-
"rev": "e96b5eca4fcfe2e0e96a1511a6cd5747515aba82",
78+
"rev": "ffad3f5b7ebe1ac3e09779ec8a863a5138c1246c",
7979
"name": "batteries",
8080
"manifestFile": "lake-manifest.json",
8181
"inputRev": "main",
@@ -85,10 +85,10 @@
8585
"type": "git",
8686
"subDir": null,
8787
"scope": "leanprover",
88-
"rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329",
88+
"rev": "cd188c6ecfbf6c00cf639e4d4fb18bf773ce8c2c",
8989
"name": "Cli",
9090
"manifestFile": "lake-manifest.json",
91-
"inputRev": "main",
91+
"inputRev": "v4.25.1",
9292
"inherited": true,
9393
"configFile": "lakefile.toml"}],
9494
"name": "Project",

‎lakefile.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,4 +8,4 @@ name = "Project"
88
[[require]]
99
name = "mathlib"
1010
scope = "leanprover-community"
11-
rev = "v4.22.0-rc4"
11+
rev = "v4.25.1"

0 commit comments

Comments
 (0)