Skip to content

ci(build_template): validate dump outputs are regular files before upload#39887

Open
adomani wants to merge 3 commits into
masterfrom
ci/upload-artifact-no-symlinks
Open

ci(build_template): validate dump outputs are regular files before upload#39887
adomani wants to merge 3 commits into
masterfrom
ci/upload-artifact-no-symlinks

Conversation

@adomani
Copy link
Copy Markdown
Contributor

@adomani adomani commented May 26, 2026

Follow-up to #39880, adding a check that artifacts produced in CI exist.

…load

Defence in depth: if a future change to the dumper (or to any other
step that touches the post-build cwd) lets PR-controlled code
substitute one of the artifact files with a symlink to something
sensitive on the runner, the existing `actions/upload-artifact`
would follow it and pack the target's contents into the artifact.

`actions/upload-artifact@v7` has no input to disable symlink
following, so add an explicit guard that aborts the step if either
expected output is a symlink or not a regular file.

Today the attack vector isn't directly reachable — the dumper opens
each output via `IO.FS.withFile … .write`, which truncate-writes
through any pre-positioned symlink and so leaves the target with the
real declaration data — but this guard documents the invariant and
catches regressions if the dumper's I/O semantics ever change.
@github-actions
Copy link
Copy Markdown

github-actions Bot commented May 26, 2026

PR summary b8420f3544

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.


No changes to strong technical debt.
No changes to weak technical debt.

Current commit b8420f3544
Reference commit 72a044471f

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
    • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

⚠️ Workflow documentation reminder

This PR modifies files under .github/workflows/.
Please update docs/workflows.md if the workflow inventory, triggers, or behavior changed.

Modified workflow files:

  • .github/workflows/build_template.yml

@github-actions github-actions Bot added the CI Modifies the continuous integration setup or other automation label May 26, 2026
Comment thread .github/workflows/build_template.yml Outdated
@joneugster joneugster added the awaiting-author A reviewer has asked the author a question or requested changes. label May 29, 2026
@joneugster joneugster self-assigned this May 29, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-author A reviewer has asked the author a question or requested changes. CI Modifies the continuous integration setup or other automation

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants