8000 Fix protected runner context check by Mnehmos · Pull Request #32 · Mnehmos/MathOS · GitHub
[go: up one dir, main page]
Skip to content
8000

Fix protected runner context check #32

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Mnehmos merged 1 commit into from
Jul 20, 2026
Merged

Fix protected runner context check #32

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
4 changes: 2 additions & 2 deletions scripts/publication-candidate.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ readonly MAX_SAFE_JSON_INTEGER=9007199254740991
readonly REPOSITORY="Mnehmos/MathOS"
readonly WORKFLOW_PATH=".github/workflows/publication.yml"
readonly SOURCE_REF="refs/heads/main"
readonly RUNNER_ENVIRONMENT="github_hosted"
readonly REPORT_RUNNER_ENVIRONMENT="github_hosted"
readonly LEAN_TOOLCHAIN="leanprover/lean4:v4.32.0"
readonly DECLARATION_NAME="MathOS.Publication.smoke"
readonly MODULE_FIXTURE="fixtures/publication/Smoke.lean"
Expand Down Expand Up @@ -111,7 +111,7 @@ done
|| die "$EXIT_CONTEXT" "publication workflow ref does not bind the protected main workflow"
[[ "$PUBLICATION_SOURCE_REF" == "$SOURCE_REF" ]] \
|| die "$EXIT_CONTEXT" "publication source ref must be exactly refs/heads/main"
[[ "$PUBLICATION_RUNNER_ENVIRONMENT" == "$RUNNER_ENVIRONMENT" ]] \
[[ "$PUBLICATION_RUNNER_ENVIRONMENT" == "$REPORT_RUNNER_ENVIRONMENT" ]] \
|| die "$EXIT_CONTEXT" "publication runner environment does not match policy"
[[ "$PUBLICATION_SOURCE_COMMIT_SHA" =~ ^[0-9a-f]{40}$ ]] \
|| die "$EXIT_CONTEXT" "publication source commit must be one lowercase 40-hex Git identity"
Expand Down
Loading
0