Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions .github/dependabot.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
version: 2 # Specifies the version of the Dependabot configuration file format

updates:
# Configuration for dependency updates
- package-ecosystem: "github-actions" # Specifies the ecosystem to check for updates
directory: "/" # Specifies the directory to check for dependencies; "/" means the root directory
schedule:
# Check for updates to GitHub Actions every month
interval: "monthly"
74 changes: 74 additions & 0 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,74 @@
name: Compile blueprint

on:
push:
branches:
- master
paths:
- '**/*.lean'
pull_request:
branches:
- master
paths:
- '**/*.lean'
- 'lean-toolchain'
- 'lakefile.toml'
- 'lake-manifest.json'
workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface

# Cancel previous runs if a new commit is pushed to the same PR or branch
concurrency:
group: ${{ github.ref }} # Group runs by the ref (branch or PR)
cancel-in-progress: true # Cancel any ongoing runs in the same group

# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages and modify PR labels
permissions:
contents: read # Read access to repository contents
pages: write # Write access to GitHub Pages
id-token: write # Write access to ID tokens
issues: write # Write access to issues
pull-requests: write # Write access to pull requests

jobs:
build_project:
runs-on: ubuntu-latest
name: Build project
steps:
- name: Add 'awaiting-CI' label
if: >
github.event_name == 'pull_request'
run: |
curl --request POST \
--url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels \
--header 'authorization: Bearer ${{ secrets.PAT_TOKEN }}' \
--header 'Content-Type: application/json' \
--data '["awaiting-CI"]'

- name: Checkout project
uses: actions/checkout@v4
with:
fetch-depth: 0 # Fetch all history for all branches and tags

- name: Install elan
run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y

- name: Cache build artifacts
uses: actions/cache@v4
with:
path: |
.lake/build
key: LakeBuild-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
restore-keys: LakeBuild-

- name: Build project
run: ~/.elan/bin/lake build

- name: Remove 'awaiting-CI' label
if: >
always() &&
github.event_name == 'pull_request'
run: |
curl --request DELETE \
--url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/awaiting-CI \
--header 'authorization: Bearer ${{ secrets.PAT_TOKEN }}' \
--header 'Content-Type: application/json'
22 changes: 22 additions & 0 deletions .github/workflows/toolchain-update.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
name: Update Dependencies

on:
schedule: # Sets a schedule to trigger the workflow
- cron: "0 8 */10 * *" # Every 10 days at 08:00 AM UTC (for more info on the cron syntax 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:
update_lean:
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
steps:
- name: Checkout code
uses: actions/checkout@v4
- name: Update project
uses: oliver-butterley/lean-update@v1-alpha
with:
on_update_succeeds: pr # Create a pull request if the update succeeds
on_update_fails: issue # Create an issue if the update fails