Skip to content

ci: rename style_guide_path to additional_instructions_path#267

Merged
alexanderlhicks merged 1 commit into
masterfrom
feat/rename-additional-instructions
May 19, 2026
Merged

ci: rename style_guide_path to additional_instructions_path#267
alexanderlhicks merged 1 commit into
masterfrom
feat/rename-additional-instructions

Conversation

@alexanderlhicks

Copy link
Copy Markdown
Collaborator

Tracks the upstream rename in alexanderlhicks/lean-summary-workflow. The input semantics are unchanged for this fork — the new name better reflects that the file passed in can be any deployment-supplied instructions, not just a style guide.

Merge ordering: the upstream lean-summary-workflow PR renaming the input must land before this PR.

Description

Briefly describe your changes, and link any issues if appropriate.

Fixes # (issue number)

Checklist

  • My code follows the mathlib naming and code style conventions
  • I have updated PORTING.md as appropriate
  • I have added my name to the authors section of any appropriate files

Generative AI Guidelines

AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review.
Please carefully review your code to ensure it meets the following standards.

  • Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library.
  • have statements that do not aid readability or code reuse should be inlined.
  • Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line.
  • In general, proofs should not perform substantially more case splitting than their Rocq counterparts.

In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations.
We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work.

Tracks the upstream rename in alexanderlhicks/lean-summary-workflow.
The input semantics are unchanged for this fork — the new name better
reflects that the file passed in can be any deployment-supplied
instructions, not just a style guide.

Merge ordering: the upstream lean-summary-workflow PR renaming the
input must land before this PR.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@github-actions

Copy link
Copy Markdown

🤖 PR Summary

Infrastructure / CI: Renames style_guide_path to additional_instructions_path in .github/workflows/summary.yml to synchronize with naming changes in the upstream lean-summary-workflow repository and reflect its usage for general deployment-supplied instructions.


Statistics

Metric Count
📝 Files Changed 1
Lines Added 1
Lines Removed 1

Lean Declarations

  • No declarations were added, removed, or affected.

sorry Tracking

  • No sorrys were added, removed, or affected.

🎨 **Style Guide Adherence**

All changes adhere to the style guide.


📄 **Per-File Summaries**
  • .github/workflows/summary.yml: Updates the summary workflow by renaming the style_guide_path configuration parameter to additional_instructions_path to align with the underlying action's updated interface.

Last updated: 2026-05-19 15:38 UTC.

@github-actions

Copy link
Copy Markdown

🤖 AI Review

No Lean files were changed in this PR.

@alexanderlhicks
alexanderlhicks merged commit e53cf76 into master May 19, 2026
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant