Skip to content

Commit e53896c

Browse files
pitmonticonepitmonticone
committed
Create repository
0 parents  commit e53896c

22 files changed

+734
-0
lines changed

‎.github/dependabot.yml

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
version: 2 # Specifies the version of the Dependabot configuration file format
2+
3+
updates:
4+
# Configuration for dependency updates
5+
- package-ecosystem: "github-actions" # Specifies the ecosystem to check for updates
6+
directory: "/" # Specifies the directory to check for dependencies; "/" means the root directory
7+
schedule:
8+
# Check for updates to GitHub Actions every month
9+
interval: "monthly"

‎.github/workflows/build-project.yml

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
name: Build CHANGE
2+
3+
on:
4+
push:
5+
branches:
6+
- main
7+
paths:
8+
- '**/*.lean'
9+
- 'lean-toolchain'
10+
- 'lakefile.toml'
11+
- 'lake-manifest.json'
12+
pull_request:
13+
branches:
14+
- main
15+
paths:
16+
- '**/*.lean'
17+
- 'lean-toolchain'
18+
- 'lakefile.toml'
19+
- 'lake-manifest.json'
20+
workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface
21+
22+
# Cancel previous runs if a new commit is pushed to the same PR or branch
23+
concurrency:
24+
group: ${{ github.ref }} # Group runs by the ref (branch or PR)
25+
cancel-in-progress: true # Cancel any ongoing runs in the same group
26+
27+
# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages and modify PR labels
28+
permissions:
29+
contents: read # Read access to repository contents
30+
pages: write # Write access to GitHub Pages
31+
id-token: write # Write access to ID tokens
32+
33+
jobs:
34+
build_project:
35+
runs-on: ubuntu-latest
36+
name: Build project
37+
steps:
38+
- name: Checkout project
39+
uses: actions/checkout@v4
40+
with:
41+
fetch-depth: 0 # Fetch all history for all branches and tags
42+
43+
- name: Install elan
44+
run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
45+
46+
- name: Get Mathlib cache
47+
run: ~/.elan/bin/lake exe cache get || true
48+
49+
- name: Cache build artifacts
50+
uses: actions/cache@v4
51+
with:
52+
path: .lake/build
53+
key: LakeBuild-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
54+
restore-keys: LakeBuild-
55+
56+
- name: Build project
57+
run: ~/.elan/bin/lake build CHANGE

‎.github/workflows/create-release.yml

Lines changed: 68 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
name: Create Release
2+
3+
on:
4+
push:
5+
branches:
6+
- main
7+
paths:
8+
- 'lean-toolchain'
9+
10+
jobs:
11+
create_release:
12+
runs-on: ubuntu-latest
13+
14+
steps:
15+
- name: Checkout code
16+
uses: actions/checkout@v4
17+
with:
18+
fetch-depth: 2 # Fetch the last two commits for comparison
19+
20+
- name: Check if lean-toolchain has changed
21+
id: check_file_change
22+
run: |
23+
# Check if the lean-toolchain file was modified in the last commit
24+
if git diff --name-only HEAD~1 HEAD | grep -q "^lean-toolchain$"; then
25+
echo "CHANGED=true" >> $GITHUB_ENV
26+
else
27+
echo "CHANGED=false" >> $GITHUB_ENV
28+
fi
29+
30+
- name: Exit if lean-toolchain did not change
31+
if: env.CHANGED != 'true'
32+
run: echo "No changes in lean-toolchain. Skipping release."
33+
34+
- name: Read Lean version from lean-toolchain
35+
if: env.CHANGED == 'true'
36+
id: get_version
37+
run: |
38+
# Extract the version from the lean-toolchain file (everything after the colon)
39+
LEAN_VERSION=$(cut -d ':' -f2 < lean-toolchain | tr -d '[:space:]')
40+
echo "tag_name=${LEAN_VERSION}" >> $GITHUB_ENV
41+
42+
- name: Create Git tag
43+
if: env.CHANGED == 'true'
44+
run: |
45+
git config user.name "github-actions[bot]"
46+
git config user.email "github-actions[bot]@users.noreply.github.com"
47+
git tag -a ${{ env.tag_name }} -m "Release ${{ env.tag_name }}"
48+
git push origin ${{ env.tag_name }}
49+
50+
- name: Create GitHub Release
51+
if: env.CHANGED == 'true'
52+
uses: actions/github-script@v7
53+
env:
54+
tag_name: ${{ env.tag_name }}
55+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
56+
with:
57+
script: |
58+
const tagName = process.env.tag_name;
59+
const releaseName = `${tagName}`;
60+
await github.rest.repos.createRelease({
61+
owner: context.repo.owner,
62+
repo: context.repo.repo,
63+
tag_name: tagName,
64+
name: releaseName,
65+
body: `Automated release for Lean version ${tagName}`,
66+
draft: false,
67+
prerelease: false
68+
});

‎.github/workflows/update-dependencies.yml

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
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+
update_lean:
10+
runs-on: ubuntu-latest
11+
permissions:
12+
contents: write # Grants permission to push changes to the repository
13+
issues: write # Grants permission to create or update issues
14+
pull-requests: write # Grants permission to create or update pull requests
15+
steps:
16+
- name: Checkout code
17+
uses: actions/checkout@v4
18+
- name: Update project
19+
uses: oliver-butterley/lean-update@v1-alpha
20+
with:
21+
on_update_succeeds: pr # Create a pull request if the update succeeds
22+
on_update_fails: issue # Create an issue if the update fails

‎.gitignore

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
## macOS
2+
.DS_Store
3+
## Lake
4+
.lake/*
5+
.cache/*
6+
## Blueprint
7+
/blueprint/print/print.log
8+
/blueprint/web/
9+
/blueprint/src/web.paux
10+
/blueprint/src/web.bbl
11+
/blueprint/print/
12+
## TeX
13+
*.aux
14+
*.lof
15+
*.log
16+
*.lot
17+
*.fls
18+
*.out
19+
*.toc
20+
*.fmt
21+
*.fot
22+
*.cb
23+
*.cb2
24+
.*.lb
25+
*.bbl
26+
*.bcf
27+
*.blg
28+
*-blx.aux
29+
*-blx.bib
30+
*.run.xml
31+
*.fdb_latexmk
32+
*.synctex
33+
*.synctex(busy)
34+
*.synctex.gz
35+
*.synctex.gz(busy)
36+
*.pdfsync

‎.vscode/extensions.json

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
{
2+
// Learn about workspace recommendations at:
3+
// https://go.microsoft.com/fwlink/?LinkId=827846
4+
5+
// The extension identifier format is ${publisher}.${name}
6+
// Example: vscode.csharp
7+
8+
// List of extensions that should be recommended for users of this workspace
9+
"recommendations": [
10+
"leanprover.lean4" // Extension for Lean 4 support
11+
]
12+
}

‎.vscode/settings.json

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
{
2+
// Configure editor to insert spaces when pressing Tab
3+
"editor.insertSpaces": true,
4+
// Set the number of spaces per tab
5+
"editor.tabSize": 2,
6+
// Display vertical rulers at specified character column for readability
7+
"editor.rulers": [100],
8+
// Set the default file encoding to UTF-8
9+
"files.encoding": "utf8",
10+
// Use Unix-style line endings ('\n') by default
11+
"files.eol": "\n",
12+
// Ensure a final newline at the end of files
13+
"files.insertFinalNewline": true,
14+
// Trim final newlines at the end of files
15+
"files.trimFinalNewlines": true,
16+
// Remove any trailing whitespace on save
17+
"files.trimTrailingWhitespace": true,
18+
// Select read-only files
19+
"files.readonlyInclude": {
20+
"**/.elan/**": true,
21+
"**/.lake/**": true
22+
},
23+
"files.exclude": {
24+
"**/.gitignore": true,
25+
"**/.lake": true,
26+
"**/LICENSE": true,
27+
"**/images": true,
28+
},
29+
// "workbench.colorTheme": "Visual Studio Light"
30+
}

‎CHANGE.lean

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

‎CHANGE/Test.lean

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
/-
2+
Copyright (c) 2024 Pietro Monticone. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Pietro Monticone
5+
-/
6+
import Mathlib.Tactic
7+
8+
/-!
9+
# Test Lean 4 Environment
10+
11+
This file serves as a basic test to verify that Lean 4 is correctly installed and configured.
12+
By evaluating the expression `2 ^ 5` and checking the correctness of a simple example, you can confirm that:
13+
14+
1. The Lean 4 environment is functioning properly.
15+
2. The `Mathlib` library is correctly imported and available for use.
16+
3. The `#eval` command is working as expected, providing the correct output.
17+
4. Tactics such as `simp` are operating correctly in proofs.
18+
-/
19+
20+
/- Evaluating a simple arithmetic expression to test the Lean environment. -/
21+
#eval 3 ^ 3 -- Expected output: 27
22+
23+
/-- A basic example to verify that the `simp` tactic is functioning correctly. -/
24+
example (x : ℝ) : x - x = 0 := by simp -- The `simp` tactic simplifies the expression to `0`

0 commit comments

Comments
 (0)