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
16 changes: 8 additions & 8 deletions .github/workflows/bench-main.yml
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ jobs:
# Lake and cargo artifacts live on the sticky disk; sccache serves the
# workspace crates cargo rebuilds after every fresh checkout (see
# ci.yml), under entries the native codegen flags keep apart from CI's.
- uses: runs-on/action@dfae4d98c5537a0dc7bbb7e6b9211f30ba240f6d # v2.4.0
- uses: runs-on/action@284bff869d4a825f778ac7c38e50f1e31ef198fd # v2.6.0
with:
sccache: s3
sticky_cache: |
Expand All @@ -71,7 +71,7 @@ jobs:
- uses: $/.github/actions/setup-rust-toolchain
with:
use-github-cache: "false"
- uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
- uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
with:
auto-config: false
build: true
Expand Down Expand Up @@ -100,7 +100,7 @@ jobs:
outputs:
matrix: ${{ steps.matrix.outputs.matrix }}
steps:
- uses: runs-on/action@dfae4d98c5537a0dc7bbb7e6b9211f30ba240f6d # v2.4.0
- uses: runs-on/action@284bff869d4a825f778ac7c38e50f1e31ef198fd # v2.6.0
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
with:
persist-credentials: false
Expand All @@ -111,7 +111,7 @@ jobs:
fail-on-cache-miss: true
- run: echo "$HOME/.local/bin" >> $GITHUB_PATH
# Provision the toolchain so `ix` finds libleanshared (no package build).
- uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
- uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
with:
auto-config: false
build: false
Expand Down Expand Up @@ -167,7 +167,7 @@ jobs:
# The compile workspace's `.lake` persists on the sticky disk: its
# Lake packages, the Mathlib oleans `cache get` fetched, and the env's
# own build, so later runs replay instead of refetching and rebuilding.
- uses: runs-on/action@dfae4d98c5537a0dc7bbb7e6b9211f30ba240f6d # v2.4.0
- uses: runs-on/action@284bff869d4a825f778ac7c38e50f1e31ef198fd # v2.6.0
with:
sticky_cache: |
custom,path=${{ env.COMPILE_DIR }}/.lake
Expand All @@ -187,7 +187,7 @@ jobs:
# for envs that import Mathlib (Mathlib, FLT) — the shared
# Benchmarks/Compile package depends on mathlib, so without this
# guard InitStd/Lean would download it for nothing.
- uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
- uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
with:
lake-package-directory: ${{ env.COMPILE_DIR }}
auto-config: false
Expand Down Expand Up @@ -294,7 +294,7 @@ jobs:
matrix:
params: ${{ fromJson(needs.plan.outputs.matrix) }}
steps:
- uses: runs-on/action@dfae4d98c5537a0dc7bbb7e6b9211f30ba240f6d # v2.4.0
- uses: runs-on/action@284bff869d4a825f778ac7c38e50f1e31ef198fd # v2.6.0
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
with:
persist-credentials: false
Expand All @@ -311,7 +311,7 @@ jobs:
# Provision the toolchain so the staged binaries find libleanshared
# (no package build). use-github-cache off: nothing to cache here, and
# parallel matrix jobs share a key and would race the cache save.
- uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
- uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
with:
auto-config: false
build: false
Expand Down
38 changes: 19 additions & 19 deletions .github/workflows/bench-pr.yml
Original file line number Diff line number Diff line change
Expand Up @@ -198,7 +198,7 @@ jobs:
# Lake and cargo artifacts live on the sticky disk; sccache serves the
# workspace crates cargo rebuilds after every fresh checkout (see
# ci.yml), under entries the native codegen flags keep apart from CI's.
- uses: runs-on/action@dfae4d98c5537a0dc7bbb7e6b9211f30ba240f6d # v2.4.0
- uses: runs-on/action@284bff869d4a825f778ac7c38e50f1e31ef198fd # v2.6.0
with:
sccache: s3
sticky_cache: |
Expand All @@ -217,7 +217,7 @@ jobs:
with:
use-github-cache: "false"
# A persistent hit still needs the matching toolchain for libleanshared.
- uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
- uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
with:
auto-config: false
build: ${{ steps.bins.outputs.cache-hit != 'true' }}
Expand Down Expand Up @@ -262,7 +262,7 @@ jobs:
tar -C "$HOME/.local/bin" -cf benchmark-binaries.tar
ix bench-typecheck
- name: Upload run binaries
uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7.0.2
with:
name: benchmark-binaries
path: benchmark-binaries.tar
Expand Down Expand Up @@ -354,7 +354,7 @@ jobs:
ref: ${{ needs.build.outputs.revision }}
# The job runs PR code; never leave the token in .git.
persist-credentials: false
- uses: runs-on/action@dfae4d98c5537a0dc7bbb7e6b9211f30ba240f6d # v2.4.0
- uses: runs-on/action@284bff869d4a825f778ac7c38e50f1e31ef198fd # v2.6.0
with:
sticky_cache: |
custom,path=Benchmarks/Compile/.lake
Expand Down Expand Up @@ -403,7 +403,7 @@ jobs:
fi
- name: Download run binaries
if: steps.compile-source.outputs.rebuild == 'true'
uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2
with:
name: benchmark-binaries
- name: Unpack run binaries
Expand All @@ -423,7 +423,7 @@ jobs:
# cache fetch has to run from that directory.
- name: Provision Lean toolchain
if: steps.compile-source.outputs.rebuild == 'true'
uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
with:
lake-package-directory: Benchmarks/Compile
auto-config: false
Expand Down Expand Up @@ -471,7 +471,7 @@ jobs:
compile-hardware.txt
key: ${{ env.BENCH_CACHE }}-bench-pr-row-${{ needs.build.outputs.revision }}-${{ matrix.env }}
- name: Upload run environment
uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7.0.2
with:
name: benchmark-env-${{ matrix.env }}
path: |
Expand Down Expand Up @@ -512,7 +512,7 @@ jobs:
steps:
# sccache for the from-scratch base build below: its workspace crates
# are what the base's own bench-main run compiled (see ci.yml).
- uses: runs-on/action@dfae4d98c5537a0dc7bbb7e6b9211f30ba240f6d # v2.4.0
- uses: runs-on/action@284bff869d4a825f778ac7c38e50f1e31ef198fd # v2.6.0
with:
sccache: s3
- uses: mozilla-actions/sccache-action@fc920bf0ec8de6ee65d409111f7ec508035751ba # v0.0.11
Expand All @@ -539,7 +539,7 @@ jobs:
# cache restore reuses ~/.local/bin). The PR's `ix bench` drives BOTH
# sides; `--repo` picks whose tools get measured.
- name: Download run binaries
uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2
with:
name: benchmark-binaries
- name: Place PR binaries
Expand All @@ -557,14 +557,14 @@ jobs:
# compiles an env — the `.ixe` and compile row come from the compile
# job's run-scoped artifact.
- name: Provision Lean toolchain
uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
with:
lake-package-directory: .
auto-config: false
build: false
use-github-cache: false
- name: Download run environment
uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2
with:
name: benchmark-env-${{ matrix.params.env }}
# ---------- PR side ----------
Expand Down Expand Up @@ -779,7 +779,7 @@ jobs:
label: Base benchmark binary build CPU
- name: Build base (ix, bench-typecheck)
if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached != 'true'
uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
with:
lake-package-directory: base
auto-config: false
Expand Down Expand Up @@ -904,7 +904,7 @@ jobs:

- name: Upload table
if: always()
uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7.0.2
with:
name: table-${{ env.LABEL }}
path: out/table-${{ env.LABEL }}.md
Expand Down Expand Up @@ -933,13 +933,13 @@ jobs:
permissions:
contents: read
steps:
- uses: runs-on/action@dfae4d98c5537a0dc7bbb7e6b9211f30ba240f6d # v2.4.0
- uses: runs-on/action@284bff869d4a825f778ac7c38e50f1e31ef198fd # v2.6.0
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
with:
ref: ${{ needs.build.outputs.revision }}
persist-credentials: false
- name: Download run binaries
uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2
with:
name: benchmark-binaries
- name: Unpack run binaries
Expand All @@ -948,13 +948,13 @@ jobs:
tar -C "$HOME/.local/bin" -xf benchmark-binaries.tar
echo "$HOME/.local/bin" >> "$GITHUB_PATH"
# Provision the toolchain so `ix` finds libleanshared (no package build).
- uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
- uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
with:
auto-config: false
build: false
use-github-cache: false
- name: Download tables
uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2
with:
path: tables
pattern: table-*
Expand All @@ -973,7 +973,7 @@ jobs:
--base-label "${BASE_REF:-${BASE_SHA::7}}" \
--repo-url "${{ github.server_url }}/${{ github.repository }}" \
--run-id "${{ github.run_id }}" --out comment-body.md
- uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
- uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7.0.2
with:
name: comment-body
path: comment-body.md
Expand All @@ -995,7 +995,7 @@ jobs:
- name: Download comment body
if: needs.assemble.result == 'success'
continue-on-error: true
uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2
with:
name: comment-body
# A failed stage prepends a warning header to the report (quoting
Expand Down
6 changes: 3 additions & 3 deletions .github/workflows/bencher-plots.yml
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ jobs:
# CPU family as the benchmark builds.
runs-on: runs-on=${{ github.run_id }}-sync-plots-${{ github.run_attempt }}/cpu=32/family=r8i.8xlarge/spot=false/image=ubuntu26-full-x64/volume=100gb/extras=s3-cache
steps:
- uses: runs-on/action@dfae4d98c5537a0dc7bbb7e6b9211f30ba240f6d # v2.4.0
- uses: runs-on/action@284bff869d4a825f778ac7c38e50f1e31ef198fd # v2.6.0
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
with:
persist-credentials: false
Expand All @@ -48,12 +48,12 @@ jobs:
fail-on-cache-miss: true
- run: echo "$HOME/.local/bin" >> $GITHUB_PATH
# Provision the toolchain so `ix` finds libleanshared (no build).
- uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
- uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
with:
auto-config: false
build: false
use-github-cache: false
- uses: bencherdev/bencher@f80847436d7157936b40525db4c2a1064124f04a # v0.6.13
- uses: bencherdev/bencher@24c333d7030390d2f3e130569386f4f1f8577113 # v0.6.15
# Plot create/delete needs those permissions on the ix project: a
# user-scoped `bencher_user_*` key (the report-upload token the bench
# workflows use may be run-scoped and unable to manage plots).
Expand Down
14 changes: 7 additions & 7 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ jobs:
# cargo rebuilds after every fresh checkout because their mtimes moved,
# come back as cache hits. RunsOn configures it before anything can
# start an sccache server.
- uses: runs-on/action@dfae4d98c5537a0dc7bbb7e6b9211f30ba240f6d # v2.4.0
- uses: runs-on/action@284bff869d4a825f778ac7c38e50f1e31ef198fd # v2.6.0
with:
sccache: s3
sticky_cache: |
Expand All @@ -48,7 +48,7 @@ jobs:
# default lib — fails CI. A push to main already passed the tests in
# the merge queue; that run only exists to snapshot the build
# products, so the tests are skipped there.
- uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
- uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
with:
build-args: "--wfail -v"
test: ${{ github.event_name != 'push' }}
Expand Down Expand Up @@ -88,7 +88,7 @@ jobs:
# cargo rebuilds after every fresh checkout because their mtimes moved,
# come back as cache hits. RunsOn configures it before anything can
# start an sccache server.
- uses: runs-on/action@dfae4d98c5537a0dc7bbb7e6b9211f30ba240f6d # v2.4.0
- uses: runs-on/action@284bff869d4a825f778ac7c38e50f1e31ef198fd # v2.6.0
with:
sccache: s3
sticky_cache: |
Expand All @@ -99,11 +99,11 @@ jobs:
with:
codegen: portable
use-github-cache: "false"
- uses: taiki-e/install-action@83ac0ad63c0167e6f06796fab0fce28db1bf3db0 # v2.87.22
- uses: taiki-e/install-action@68a389c788b2cd04016ce8c80ee23b80d2ab3d68 # v2.88.1
with:
tool: nextest
# Install Lean for rust-bindgen step
- uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
- uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
with:
auto-config: false
use-github-cache: false
Expand Down Expand Up @@ -152,7 +152,7 @@ jobs:
# instance role need checking first), and an `NVCC` wrapper running
# `sccache nvcc` for the kernels, which multi-stark's build script
# must compile with `-c` per source for sccache to cache them.
- uses: runs-on/action@dfae4d98c5537a0dc7bbb7e6b9211f30ba240f6d # v2.4.0
- uses: runs-on/action@284bff869d4a825f778ac7c38e50f1e31ef198fd # v2.6.0
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
with:
persist-credentials: false
Expand All @@ -171,7 +171,7 @@ jobs:
path: .lake
key: lake-cuda-13.3.1-ubuntu26-x86-64-v4-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'rust-toolchain.toml') }}-${{ github.sha }}
restore-keys: lake-cuda-13.3.1-ubuntu26-x86-64-v4-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'rust-toolchain.toml') }}-
- uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
- uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
with:
auto-config: false
use-github-cache: false
Expand Down
10 changes: 5 additions & 5 deletions .github/workflows/codeql.yml
Original file line number Diff line number Diff line change
Expand Up @@ -62,11 +62,11 @@ jobs:
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
with:
persist-credentials: false
- uses: github/codeql-action/init@2892aa5e19bbd11bc0cff5427e3b750a04d9e3c2 # v4.38.2
- uses: github/codeql-action/init@9b3254085494b55a0f7c4c2b3d2d52cc712ce370 # v4.39.1
with:
languages: actions
build-mode: none
- uses: github/codeql-action/analyze@2892aa5e19bbd11bc0cff5427e3b750a04d9e3c2 # v4.38.2
- uses: github/codeql-action/analyze@9b3254085494b55a0f7c4c2b3d2d52cc712ce370 # v4.39.1
with:
category: "/language:actions"

Expand All @@ -80,15 +80,15 @@ jobs:
security-events: write
packages: read
steps:
- uses: runs-on/action@dfae4d98c5537a0dc7bbb7e6b9211f30ba240f6d # v2.4.0
- uses: runs-on/action@284bff869d4a825f778ac7c38e50f1e31ef198fd # v2.6.0
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
with:
persist-credentials: false
- uses: github/codeql-action/init@2892aa5e19bbd11bc0cff5427e3b750a04d9e3c2 # v4.38.2
- uses: github/codeql-action/init@9b3254085494b55a0f7c4c2b3d2d52cc712ce370 # v4.39.1
with:
languages: rust
build-mode: none
dependency-caching: true
- uses: github/codeql-action/analyze@2892aa5e19bbd11bc0cff5427e3b750a04d9e3c2 # v4.38.2
- uses: github/codeql-action/analyze@9b3254085494b55a0f7c4c2b3d2d52cc712ce370 # v4.39.1
with:
category: "/language:rust"
Loading
Loading