Skip to content
Merged
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
3 changes: 3 additions & 0 deletions .github/actionlint.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
self-hosted-runner:
labels:
- nscloud-ubuntu-22.04-amd64-8x16
16 changes: 16 additions & 0 deletions .github/workflows/actionlint.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
name: Lint GitHub Actions workflows

on: [pull_request, merge_group]

jobs:
actionlint:
name: "Lint GitHub Actions workflows"
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v5

- name: Run actionlint
uses: reviewdog/action-actionlint@v1
with:
fail_level: any
actionlint_flags: ""
6 changes: 3 additions & 3 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ jobs:
set -o pipefail
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
./elan-init -y --default-toolchain none
echo "$HOME/.elan/bin" >> $GITHUB_PATH
echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

- uses: actions/checkout@v5

Expand All @@ -38,7 +38,7 @@ jobs:

- name: Compute short SHA
id: shortSHA
run: echo "short_sha=$(git rev-parse --short HEAD)" >> $GITHUB_OUTPUT
run: echo "short_sha=$(git rev-parse --short HEAD)" >> "$GITHUB_OUTPUT"

- name: Cache .lake
uses: actions/cache@v4
Expand Down Expand Up @@ -198,7 +198,7 @@ jobs:
manual.pdf
html-manual.zip

- uses: "marvinpinto/action-automatic-releases@latest"
- uses: "marvinpinto/action-automatic-releases@v1.2.1"
if: github.ref_type != 'tag' && github.ref == 'refs/heads/main'
with:
repo_token: "${{ secrets.GITHUB_TOKEN }}"
Expand Down
8 changes: 7 additions & 1 deletion .github/workflows/consistent-subverso-manifests.yml
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ jobs:
name: SubVerso version consistency
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- uses: actions/checkout@v5

- name: Check for consistent Subverso versions in all manifests
run: |
Expand All @@ -36,10 +36,16 @@ jobs:

# Show all Subverso versions in the repository
echo "SubVerso versions in all manifests:"
# $file is a jq variable (set via --arg), not a shell variable
# SC2016 (expressions don't expand in single quotes) is a false positive here
# shellcheck disable=SC2016
find . -name lake-manifest.json -print0 | xargs -0 jq --arg file input_filename '.packages[] | select(.name == "subverso") | {"file": $file, "subverso": .rev}'
echo ""

# Check that all non-root manifests use one of the two valid revisions
# $root and $demod are jq variables (set via --arg), not shell variables
# SC2016 (expressions don't expand in single quotes) is a false positive here
# shellcheck disable=SC2016
find . -name lake-manifest.json -not -path ./lake-manifest.json -print0 | \
xargs -0 jq -e --arg root "$ROOT_REV" --arg demod "$DEMOD_REV" \
'all(.packages[] | select(.name == "subverso") | .rev; . == $root or . == $demod)'
12 changes: 6 additions & 6 deletions .github/workflows/update-nightly.yml
Original file line number Diff line number Diff line change
Expand Up @@ -45,27 +45,27 @@ jobs:
id: last-working
run: |
TOOLCHAIN="$(cut -f2 -d: ./lean-toolchain)"
echo "version=$TOOLCHAIN" >> $GITHUB_OUTPUT
echo "version=$TOOLCHAIN" >> "$GITHUB_OUTPUT"

- name: Get latest release tag from leanprover/lean4-nightly
id: latest-available
run: |
RELEASE_TAG="$(curl -s "https://api.github.com/repos/leanprover/lean4-nightly/releases" | jq -r '.[0].tag_name')"
echo "RELEASE_TAG=$RELEASE_TAG" >> "${GITHUB_ENV}"
echo "version=$RELEASE_TAG" >> $GITHUB_OUTPUT
echo "version=$RELEASE_TAG" >> "$GITHUB_OUTPUT"

- name: Check if update needed
id: check-update
run: |
if [ "${{ steps.last-working.outputs.version }}" = "${{ steps.latest-available.outputs.version }}" ]; then
echo "No update needed - versions match"
echo "✅ Nightly version ${{ steps.last-working.outputs.version }} is already up to date"
echo "✅ Nightly version \`${{ steps.last-working.outputs.version }}\` is already up to date" >> $GITHUB_STEP_SUMMARY
echo "update-needed=false" >> $GITHUB_OUTPUT
echo "✅ Nightly version \`${{ steps.last-working.outputs.version }}\` is already up to date" >> "$GITHUB_STEP_SUMMARY"
echo "update-needed=false" >> "$GITHUB_OUTPUT"
else
echo "Update needed: ${{ steps.last-working.outputs.version }} -> ${{ steps.latest-available.outputs.version }}"
echo "Update needed: \`${{ steps.last-working.outputs.version }}\` -> \`${{ steps.latest-available.outputs.version }}\`" >> $GITHUB_STEP_SUMMARY
echo "update-needed=true" >> $GITHUB_OUTPUT
echo "Update needed: \`${{ steps.last-working.outputs.version }}\` -> \`${{ steps.latest-available.outputs.version }}\`" >> "$GITHUB_STEP_SUMMARY"
echo "update-needed=true" >> "$GITHUB_OUTPUT"
fi

# This job tries to update nightly-testing, and pushes if successful
Expand Down
Loading