feat(multivariate): add first-vars degree and finSucc coefficient helpers #315
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: PR Review | |
| on: | |
| pull_request: | |
| types: [opened] | |
| issue_comment: | |
| types: [created] | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.event.issue.number }} | |
| cancel-in-progress: true | |
| jobs: | |
| review: | |
| if: >- | |
| ( | |
| github.event_name == 'pull_request' && | |
| ( | |
| github.event.pull_request.author_association == 'OWNER' || | |
| github.event.pull_request.author_association == 'MEMBER' || | |
| github.event.pull_request.author_association == 'COLLABORATOR' | |
| ) | |
| ) || | |
| ( | |
| github.event_name == 'issue_comment' && | |
| github.event.issue.pull_request && | |
| startsWith(github.event.comment.body, '/review') && | |
| ( | |
| github.event.comment.author_association == 'OWNER' || | |
| github.event.comment.author_association == 'MEMBER' || | |
| github.event.comment.author_association == 'COLLABORATOR' | |
| ) | |
| ) | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 90 | |
| permissions: | |
| contents: read | |
| pull-requests: write | |
| steps: | |
| - name: Extract arguments from comment | |
| id: get_args | |
| if: github.event_name == 'issue_comment' | |
| env: | |
| COMMENT_BODY: ${{ github.event.comment.body }} | |
| run: | | |
| EOF=$(openssl rand -hex 8) | |
| awk -v eof="$EOF" -v gh_out="$GITHUB_OUTPUT" ' | |
| BEGIN { | |
| ext = "" | |
| repo = "" | |
| com = "" | |
| section = "" | |
| } | |
| /^External:/ { section="ext"; next } | |
| /^Internal:/ { section="repo"; next } | |
| /^Comments:/ { section="com"; next } | |
| { | |
| gsub(/\r/, "", $0); | |
| gsub(/^[ \t]+|[ \t]+$/, "", $0); | |
| if ($0 == "" || $0 == "/review") { next } | |
| if (section == "ext") { | |
| sub(/^- +/, ""); | |
| if (ext != "") { ext = ext "," $0 } else { ext = $0 } | |
| } | |
| else if (section == "repo") { | |
| sub(/^- +/, ""); | |
| if (repo != "") { repo = repo "," $0 } else { repo = $0 } | |
| } | |
| else if (section == "com") { | |
| if (com != "") { com = com "\n" $0 } else { com = $0 } | |
| } | |
| } | |
| END { | |
| printf "external_refs=%s\n", ext >> gh_out | |
| printf "repo_context_refs=%s\n", repo >> gh_out | |
| printf "additional_comments<<%s\n", eof >> gh_out | |
| printf "%s\n", com >> gh_out | |
| printf "%s\n", eof >> gh_out | |
| } | |
| ' <<< "$COMMENT_BODY" | |
| shell: bash | |
| - name: Build review instructions | |
| id: build_instructions | |
| env: | |
| USER_COMMENTS: ${{ steps.get_args.outputs.additional_comments }} | |
| run: | | |
| EOF=$(openssl rand -hex 8) | |
| { | |
| echo "final<<${EOF}" | |
| cat <<'PRECEDENT' | |
| Project precedent (CompPoly-specific conventions that override generic CONTRIBUTING.md rules — do NOT flag these as violations): | |
| Variable naming overrides (algebraic context): | |
| - Algebraic carrier types use R, M, G, F (rings, modules, groups, fields), not α, β. | |
| - Polynomial-typed values use p, q (e.g. CPolynomial, CMvPolynomial, CMlPolynomial), not just predicates. | |
| - Indices into vectors, lists, and Fin n use i, j, k regardless of underlying numeric type. | |
| - In algebraic lemma names that mirror Mathlib (e.g. pow_add, npow_add), exponent variables may be a, b. | |
| Style rules marked "preferred but not enforced" in CONTRIBUTING.md (the merged codebase uses both styles freely — do not flag): | |
| - "Use the where syntax for instances" — both `instance ... := ⟨...⟩` and `instance ... where` are accepted. | |
| - "Use manual dot notation for equality" — both `h.symm` and `Eq.symm h` are accepted. | |
| - "Use <| / |> to reduce nesting" — both pipe-style and parens are accepted. | |
| File scope of style rules: | |
| - The 100-character line-length rule applies ONLY to `.lean` source files. Do NOT flag long lines in `.md`, `.yml`, `.toml`, or any other non-Lean files. The enforced linter (`scripts/lint-style.py`) only processes `.lean` files. | |
| Review scope: | |
| - Flag ONLY lines introduced by this PR (the diff). Do not comment on pre-existing code that this PR did not modify. | |
| PRECEDENT | |
| if [ -n "${USER_COMMENTS}" ]; then | |
| printf '\n\nUser-supplied additional context:\n%s\n' "${USER_COMMENTS}" | |
| fi | |
| echo "${EOF}" | |
| } >> $GITHUB_OUTPUT | |
| shell: bash | |
| - uses: alexanderlhicks/lean-review-workflow@main | |
| with: | |
| github_token: ${{ secrets.GITHUB_TOKEN }} | |
| api_key: ${{ secrets.GEMINI_API_KEY }} | |
| provider: gemini | |
| model: gemini-3.1-pro-preview | |
| pr_number: ${{ github.event.issue.number || github.event.pull_request.number }} | |
| external_refs: "${{ steps.get_args.outputs.external_refs }}" | |
| repo_context_refs: "${{ steps.get_args.outputs.repo_context_refs }}" | |
| additional_comments: "${{ steps.build_instructions.outputs.final }}" | |