Skip to content

chore(deps): bump leanprover/lean-action from 1.6.2 to 1.7.0 in the actions group - #114

Merged
hyperpolymath merged 1 commit into
mainfrom
dependabot/github_actions/actions-5c801928ed
Nov 2, 2026
Merged

hyperpolymath merged 1 commit into
mainfrom
dependabot/github_actions/actions-5c801928ed

Conversation

@dependabot

@dependabot dependabot Bot commented on behalf of github Nov 1, 2026

Copy link
Copy Markdown
Contributor

Bumps the actions group with 1 update: leanprover/lean-action.

Updates leanprover/lean-action from 1.6.2 to 1.7.0

Release notes

Sourced from leanprover/lean-action's releases.

v1.7.0

Changed

  • set MATHLIB_CACHE_GET_URL to https://cache.mathlib.org/mathlib4 for lake exe cache get, so Mathlib cache clients that read this variable download from cache.mathlib.org. A value that the workflow sets takes precedence. An empty value unsets the variable, so the cache client uses its own default endpoint

Fixed

  • pass --no-modify-path to elan-init so installing elan no longer edits the runner's persistent environment (HKCU\Environment\PATH on Windows, ~/.profile and friends elsewhere). lean-action already puts $HOME/.elan/bin on $GITHUB_PATH, so this is a no-op on GitHub-hosted runners; on self-hosted runners it stops every job from accumulating PATH entries that outlive it
Changelog

Sourced from leanprover/lean-action's changelog.

Changelog

All notable changes to lean-action will be documented in this file.

The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.

Unreleased

v1.7.0 - 2026-10-27

Changed

  • set MATHLIB_CACHE_GET_URL to https://cache.mathlib.org/mathlib4 for lake exe cache get, so Mathlib cache clients that read this variable download from cache.mathlib.org. A value that the workflow sets takes precedence. An empty value unsets the variable, so the cache client uses its own default endpoint

Fixed

  • pass --no-modify-path to elan-init so installing elan no longer edits the runner's persistent environment (HKCU\Environment\PATH on Windows, ~/.profile and friends elsewhere). lean-action already puts $HOME/.elan/bin on $GITHUB_PATH, so this is a no-op on GitHub-hosted runners; on self-hosted runners it stops every job from accumulating PATH entries that outlive it

v1.6.2 - 2026-10-12

Fixed

  • save the GitHub cache after testing and linting so their build artifacts can be reused, preserving caching after test or lint failures and skipping saves on an exact cache hit

v1.6.1 - 2026-10-02

Changed

  • pin the actions/cache steps, and all actions used by this repository's workflows, to full commit SHAs, so that lean-action works in organizations that require SHA-pinned actions

v1.6.0 - 2026-08-22

Added

  • new leanchecker-args input to pass arguments to lake env leanchecker, e.g. leanchecker-args: "-v" for verbose output or explicit module prefixes such as leanchecker-args: "MyPkg.Core" to narrow the set of modules checked
  • new axiom-audit input to audit the project's axioms with axiom-audit: fail if any declaration depends on an axiom outside the allowlist (catches sorry, native_decide, and home-rolled axioms). Default: false
  • new axiom-audit-allow input for the allowlist (default: propext,Classical.choice,Quot.sound)
  • new axiom-audit-root input to set the audited root namespace (default: the lakefile's library name)
  • new axiom-audit-status output parameter
  • new lint-args input to specify arguments to pass to lake lint

... (truncated)

Commits

Dependabot compatibility score

Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.


Dependabot commands and options

You can trigger Dependabot actions by commenting on this PR:

  • @dependabot rebase will rebase this PR
  • @dependabot recreate will recreate this PR, overwriting any edits that have been made to it
  • @dependabot show <dependency name> ignore conditions will show all of the ignore conditions of the specified dependency
  • @dependabot ignore <dependency name> major version will close this group update PR and stop Dependabot creating any more for the specific dependency's major version (unless you unignore this specific dependency's major version or upgrade to it yourself)
  • @dependabot ignore <dependency name> minor version will close this group update PR and stop Dependabot creating any more for the specific dependency's minor version (unless you unignore this specific dependency's minor version or upgrade to it yourself)
  • @dependabot ignore <dependency name> will close this group update PR and stop Dependabot creating any more for the specific dependency (unless you unignore this specific dependency or upgrade to it yourself)
  • @dependabot unignore <dependency name> will remove all of the ignore conditions of the specified dependency
  • @dependabot unignore <dependency name> <ignore condition> will remove the ignore condition of the specified dependency and ignore conditions

Bumps the actions group with 1 update: [leanprover/lean-action](https://github.com/leanprover/lean-action).


Updates `leanprover/lean-action` from 1.6.2 to 1.7.0
- [Release notes](https://github.com/leanprover/lean-action/releases)
- [Changelog](https://github.com/leanprover/lean-action/blob/main/CHANGELOG.md)
- [Commits](leanprover/lean-action@24581d7...fe40864)

---
updated-dependencies:
- dependency-name: leanprover/lean-action
  dependency-version: 1.7.0
  dependency-type: direct:production
  update-type: version-update:semver-minor
  dependency-group: actions
...

Signed-off-by: dependabot[bot] <support@github.com>
@dependabot dependabot Bot added dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code labels Nov 1, 2026
@dependabot
dependabot Bot requested a review from hyperpolymath as a code owner November 1, 2026 17:40
@coderabbitai

coderabbitai Bot commented Nov 1, 2026 •

Copy link
Copy Markdown
Contributor

Important

Review skipped

This PR was authored by a bot without an assigned CodeRabbit review seat. Ask an organization administrator to assign a seat to the bot. See the seat-assignment guide. After the seat is assigned, request a review again.

Run configuration
  • Source mode: Auto
  • Repository: Unavailable
  • Branch: Unavailable
  • File: No configuration file from this repository applied
  • Commit: Unavailable
  • Layers: Organization UI
  • Review profile: ASSERTIVE
  • Plan: Advanced
  • Run ID: 5a4b31e9-645a-408c-8024-5b665507f366

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

  • Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

@github-actions

github-actions Bot commented Nov 1, 2026

Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 42 issues detected

Severity Count
🔴 Critical 0
🟠 High 20
🟡 Medium 22
View findings
[
  {
    "reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/label-triage.yml",
    "level": "epi",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "triage",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/label-triage.yml",
          "end_line": 0,
          "start_line": 0
        },
        "rule": "workflow_audit/missing_timeout_minutes",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/labels.yml",
    "level": "epi",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "sync",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/labels.yml",
          "end_line": 0,
          "start_line": 0
        },
        "rule": "workflow_audit/missing_timeout_minutes",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 262,
    "reason": "job `scan` in .github/workflows/hypatia-scan.yml references `secrets.*` but does not install `step-security/harden-runner` or declare its egress — review outbound-egress monitoring; it holds the credential next to fetched code (a piped installer or a dependency install/build)",
    "type": "RE001",
    "file": ".github/workflows/hypatia-scan.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/hypatia-scan.yml",
          "end_line": 262,
          "start_line": 262
        },
        "rule": "research_extensions/RE001",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": null,
    "reason": "workflow .github/workflows/dependabot-automerge.yml has top-level `permissions:` with `contents: write` AND performs a write (push/commit/release/PR). It is over-broad, but narrowing the workflow level alone WOULD BREAK IT — no job declares its own `permissions:`.",
    "type": "WH002",
    "file": ".github/workflows/dependabot-automerge.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/dependabot-automerge.yml",
          "end_line": 0,
          "start_line": 0
        },
        "rule": "workflow_hardening/WH002",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 47,
    "reason": "workflow .github/workflows/label-triage.yml:47 job `triage` has no `timeout-minutes:` — defaults to 360 min on hang",
    "type": "WH006",
    "file": ".github/workflows/label-triage.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/label-triage.yml",
          "end_line": 47,
          "start_line": 47
        },
        "rule": "workflow_hardening/WH006",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 33,
    "reason": "workflow .github/workflows/labels.yml:33 job `sync` has no `timeout-minutes:` — defaults to 360 min on hang",
    "type": "WH006",
    "file": ".github/workflows/labels.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/labels.yml",
          "end_line": 33,
          "start_line": 33
        },
        "rule": "workflow_hardening/WH006",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 12,
    "reason": "workflow .github/workflows/mirror.yml:12 uses `secrets: inherit` — forwards every caller secret to the reusable workflow",
    "type": "WH008",
    "file": ".github/workflows/mirror.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/mirror.yml",
          "end_line": 12,
          "start_line": 12
        },
        "rule": "workflow_hardening/WH008",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 18,
    "reason": "workflow .github/workflows/secret-scanner.yml:18 uses `secrets: inherit` — forwards every caller secret to the reusable workflow",
    "type": "WH008",
    "file": ".github/workflows/secret-scanner.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/secret-scanner.yml",
          "end_line": 18,
          "start_line": 18
        },
        "rule": "workflow_hardening/WH008",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 16,
    "reason": "workflow .github/workflows/scorecard.yml:16 uses `secrets: inherit` — forwards every caller secret to the reusable workflow",
    "type": "WH008",
    "file": ".github/workflows/scorecard.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/scorecard.yml",
          "end_line": 16,
          "start_line": 16
        },
        "rule": "workflow_hardening/WH008",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": null,
    "reason": "workflow .github/workflows/hypatia-scan.yml uploads SARIF to code scanning but masks the scanner's failure (`|| true` / `|| echo 0`) and never asserts the findings artefact is a non-empty array. When the scanner fails, this uploads a SARIF with zero results, and GitHub AUTO-CLOSES every previously-open alert for that category — silently, with the job green.",
    "type": "WH014",
    "file": ".github/workflows/hypatia-scan.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "high",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/hypatia-scan.yml",
          "end_line": 0,
          "start_line": 0
        },
        "rule": "workflow_hardening/WH014",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@coderabbitai

coderabbitai Bot commented Nov 1, 2026

Copy link
Copy Markdown
Contributor

Add Carrot credits or activate Agent usage billing to use Autofix

@hyperpolymath
hyperpolymath merged commit 5f4b353 into main Nov 2, 2026
18 of 19 checks passed
@hyperpolymath
hyperpolymath deleted the dependabot/github_actions/actions-5c801928ed branch November 2, 2026 06:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants