chore: bump toolchain to v4.30.0-rc1 #259

Workflow file for this run

.github/workflows/validate_mathlib_ci_paths.yml at 5e3472c

	# Sanity checks for mathlib-ci usage in workflow files
	#
	# 1. Prevent CI breakages caused by stale or mistyped `CI_SCRIPTS_DIR` paths
	# in workflow files by validating references against a fresh checkout of
	# `leanprover-community/mathlib-ci`.
	# On workflow changes, this job scans `.github/workflows/*.{yml,yaml}`
	# for `$CI_SCRIPTS_DIR/...` and `${CI_SCRIPTS_DIR}/...` literals (excluding comments
	# and this validator file), then fails if any referenced path is missing or escapes
	# the checked out scripts directory.
	#
	# 2. Ensure workflow files do not check out `leanprover-community/mathlib-ci`
	# directly and instead use the local `get-mathlib-ci` action.
	#
	# The logic is fairly naive and the point is to prevent mistakes rather than a bulletproof validation of all possible dynamic path constructions, but it should catch common typos and missing files in mathlib-ci.
	name: Validate mathlib-ci script paths

	on:
	# Validate references whenever workflow files change.
	pull_request:
	paths:
	- '.github/workflows/**'
	workflow_dispatch:

	permissions:
	contents: read

	jobs:
	validate-ci-scripts-paths:
	runs-on: ubuntu-latest
	steps:
	- name: Checkout
	uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

	- name: Checkout local actions
	uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
	with:
	ref: ${{ github.workflow_sha }}
	fetch-depth: 1
	sparse-checkout: .github/actions
	path: workflow-actions
	- name: Get mathlib-ci
	id: get_mathlib_ci
	uses: ./workflow-actions/.github/actions/get-mathlib-ci
	with:
	ref: master # Check paths against the latest version of the repo, which should be 'the objective' version for any workflow

	# We scan literal "$CI_SCRIPTS_DIR/..." and "${CI_SCRIPTS_DIR}/..."
	# references in workflow text and check those paths in the checked out mathlib-ci ref; dynamically
	# constructed paths or non-default variable names are not covered by this best-effort check,
	# but this should catch common typos and missing files in mathlib-ci.
	- name: Validate CI_SCRIPTS_DIR references
	env:
	CI_SCRIPTS_DIR: ${{ steps.get_mathlib_ci.outputs.scripts_dir }}
	shell: python
	run: \|
	import os
	import re
	import sys
	from collections import defaultdict
	from pathlib import Path

	workflows_dir = Path(".github/workflows")
	scripts_dir = Path(os.environ["CI_SCRIPTS_DIR"])

	# Match both ${CI_SCRIPTS_DIR}/... and $CI_SCRIPTS_DIR/... forms.
	pattern = re.compile(r"(?:\$\{CI_SCRIPTS_DIR\}\|\$CI_SCRIPTS_DIR)/([A-Za-z0-9._/-]+)")
	references = defaultdict(list)

	def strip_yaml_comment(line: str) -> str:
	"""Strip YAML comments, preserving # characters inside quotes."""
	in_single = False
	in_double = False
	escaped = False
	for i, ch in enumerate(line):
	if in_double:
	if escaped:
	escaped = False
	elif ch == "\\":
	escaped = True
	elif ch == '"':
	in_double = False
	elif in_single:
	if ch == "'":
	in_single = False
	else:
	if ch == '"':
	in_double = True
	elif ch == "'":
	in_single = True
	elif ch == "#":
	return line[:i]
	return line

	workflow_files = sorted(workflows_dir.glob(".yml")) + sorted(workflows_dir.glob(".yaml"))
	for workflow in workflow_files:
	# Skip this validator workflow to avoid matching its own example strings.
	if workflow.name == "validate_mathlib_ci_paths.yml":
	continue
	for line_number, line in enumerate(workflow.read_text().splitlines(), start=1):
	if line.lstrip().startswith("#"):
	continue
	content = strip_yaml_comment(line)
	for match in pattern.finditer(content):
	rel_path = match.group(1)
	if rel_path == "...":
	continue
	references[rel_path].append(f"{workflow}:{line_number}")

	missing = []
	scripts_root = scripts_dir.resolve()
	for rel_path, locations in sorted(references.items()):
	full_path = (scripts_dir / rel_path).resolve()
	# Reject any path that escapes the checked out scripts directory.
	if scripts_root not in full_path.parents and full_path != scripts_root:
	missing.append((rel_path, locations))
	continue
	if not full_path.exists():
	missing.append((rel_path, locations))

	if missing:
	print("Validation failures:")
	print("Missing paths in mathlib-ci checkout:")
	for rel_path, locations in missing:
	print(f"- {rel_path}")
	print(f" used at: {', '.join(locations)}")
	sys.exit(1)

	print(f"Validated {len(references)} CI_SCRIPTS_DIR reference(s).")

	# Ensure workflow files do not check out leanprover-community/mathlib-ci
	# directly. They should use the local get-mathlib-ci action instead.
	# Parsing is intentionally lightweight: scan lines, strip YAML comments,
	# and use indentation to stay within one step's `with:` block.
	- name: Validate mathlib-ci checkout usage
	shell: python
	run: \|
	import re
	import sys
	from pathlib import Path

	workflows_dir = Path(".github/workflows")

	def strip_yaml_comment(line: str) -> str:
	"""Strip YAML comments, preserving # characters inside quotes."""
	in_single = False
	in_double = False
	escaped = False
	for i, ch in enumerate(line):
	if in_double:
	if escaped:
	escaped = False
	elif ch == "\\":
	escaped = True
	elif ch == '"':
	in_double = False
	elif in_single:
	if ch == "'":
	in_single = False
	else:
	if ch == '"':
	in_double = True
	elif ch == "'":
	in_single = True
	elif ch == "#":
	return line[:i]
	return line

	def leading_spaces(line: str) -> int:
	"""Return indentation width using plain leading spaces."""
	return len(line) - len(line.lstrip(" "))

	def collect_mathlib_ci_checkouts(workflow, workflow_text):
	"""Find direct `actions/checkout` steps that target `mathlib-ci`."""
	lines = workflow_text.splitlines()
	results = []

	for i, raw_line in enumerate(lines):
	content = strip_yaml_comment(raw_line).rstrip()
	repo_match = re.match(r"^\srepository:\s(.?)\s$", content)
	if not repo_match:
	continue

	repository = strip_yaml_comment(repo_match.group(1)).strip()
	if len(repository) >= 2 and repository[0] == repository[-1] and repository[0] in {"'", '"'}:
	repository = repository[1:-1]
	if not repository.endswith("/mathlib-ci"):
	continue

	repo_indent = leading_spaces(content)
	step_uses_checkout = False
	j = i
	while j >= 0:
	# Walk upward to the containing `-` step and confirm it is an
	# `actions/checkout` step before treating this as a checkout ref.
	previous = strip_yaml_comment(lines[j]).rstrip()
	if not previous.strip():
	j -= 1
	continue
	if re.match(r"^\s*-\s+", previous) and leading_spaces(previous) < repo_indent:
	for k in range(j, i + 1):
	candidate = strip_yaml_comment(lines[k]).rstrip()
	if re.match(r"^\suses:\sactions/checkout@", candidate):
	step_uses_checkout = True
	break
	break
	j -= 1

	if not step_uses_checkout:
	continue

	results.append(
	{
	"workflow": workflow.name,
	"repository_line": i + 1,
	}
	)
	return results

	workflow_files = sorted(workflows_dir.glob(".yml")) + sorted(workflows_dir.glob(".yaml"))
	errors = []
	for workflow in workflow_files:
	# Skip this validator workflow to avoid validating its checkout.
	if workflow.name == "validate_mathlib_ci_paths.yml":
	continue
	workflow_text = workflow.read_text()
	checkout_steps = collect_mathlib_ci_checkouts(workflow, workflow_text)
	for step in checkout_steps:
	errors.append(
	f"{workflow}:{step['repository_line']} checks out mathlib-ci directly; "
	"use `./workflow-actions/.github/actions/get-mathlib-ci` instead."
	)

	if errors:
	print("Validation failures:")
	for error in errors:
	print(error)
	sys.exit(1)

	print("Validated that workflow files use the local get-mathlib-ci action.")

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

chore: bump toolchain to v4.30.0-rc1 #259

Workflow file

chore: bump toolchain to v4.30.0-rc1 #259

Uh oh!

Workflow file for this run