Ecosyste.ms: Issues
An open API service for providing issue and pull request metadata for open source projects.
GitHub / leanprover/lean-action issues and pull requests
#100 - chore: update functional test Lean version to 4.11.0
Pull Request -
State: closed - Opened by austinletson 3 months ago
#100 - chore: update functional test Lean version to 4.11.0
Pull Request -
State: closed - Opened by austinletson 3 months ago
#99 - feat: add Windows runner support
Pull Request -
State: closed - Opened by austinletson 3 months ago
#99 - feat: add Windows runner support
Pull Request -
State: closed - Opened by austinletson 3 months ago
#98 - doc: fix misspelling in README.md
Pull Request -
State: closed - Opened by david-christiansen 3 months ago
- 2 comments
#98 - doc: fix misspelling in README.md
Pull Request -
State: closed - Opened by david-christiansen 3 months ago
- 2 comments
#97 - fix: replace `actions/cache` with `actions/cache/restore`
Pull Request -
State: closed - Opened by austinletson 3 months ago
#97 - fix: replace `actions/cache` with `actions/cache/restore`
Pull Request -
State: closed - Opened by austinletson 3 months ago
#96 - Failed to save: Unable to reserve cache with key
Issue -
State: closed - Opened by zhassan-aws 3 months ago
- 1 comment
#96 - Failed to save: Unable to reserve cache with key
Issue -
State: closed - Opened by zhassan-aws 3 months ago
- 1 comment
#95 - doc: v1.0.2 CHANGELOG
Pull Request -
State: closed - Opened by austinletson 3 months ago
#95 - doc: v1.0.2 CHANGELOG
Pull Request -
State: closed - Opened by austinletson 3 months ago
#94 - fix: only end log group if lake command succeeds
Pull Request -
State: closed - Opened by austinletson 3 months ago
#93 - v1.0.2 release
Issue -
State: closed - Opened by austinletson 3 months ago
- 2 comments
Labels: release
#93 - v1.0.2 release
Issue -
State: closed - Opened by austinletson 3 months ago
- 2 comments
Labels: release
#92 - fix: remove set-output-parameters step to fix log group expansion
Pull Request -
State: closed - Opened by austinletson 3 months ago
#92 - fix: remove set-output-parameters step to fix log group expansion
Pull Request -
State: closed - Opened by austinletson 3 months ago
#91 - fix: correct typo in configuration step
Pull Request -
State: closed - Opened by austinletson 3 months ago
#91 - fix: correct typo in configuration step
Pull Request -
State: closed - Opened by austinletson 3 months ago
#90 - lake check-test failed -> will not run lake lint
Issue -
State: closed - Opened by kim-em 3 months ago
#90 - lake check-test failed -> will not run lake lint
Issue -
State: closed - Opened by kim-em 3 months ago
#89 - doc: update CHANGELOG.md for v1.0.1
Pull Request -
State: closed - Opened by austinletson 3 months ago
#89 - doc: update CHANGELOG.md for v1.0.1
Pull Request -
State: closed - Opened by austinletson 3 months ago
#88 - feat: use lake manifest to determine mathlib dependency
Pull Request -
State: closed - Opened by austinletson 3 months ago
#88 - feat: use lake manifest to determine mathlib dependency
Pull Request -
State: closed - Opened by austinletson 3 months ago
#87 - chore: fix release template typo
Pull Request -
State: closed - Opened by austinletson 3 months ago
#87 - chore: fix release template typo
Pull Request -
State: closed - Opened by austinletson 3 months ago
#86 - v1.0.1 release
Issue -
State: closed - Opened by austinletson 3 months ago
- 1 comment
Labels: release
#86 - v1.0.1 release
Issue -
State: closed - Opened by austinletson 3 months ago
- 1 comment
Labels: release
#85 - bug: `detect_mathlib` doesn't find mathlib dependency
Issue -
State: closed - Opened by Seasawher 3 months ago
- 4 comments
#85 - bug: `detect_mathlib` doesn't find mathlib dependency
Issue -
State: closed - Opened by Seasawher 3 months ago
- 4 comments
#84 - feat: switch elan installation method from tar -> `elan-init.sh`
Pull Request -
State: closed - Opened by austinletson 3 months ago
#84 - feat: switch elan installation method from tar -> `elan-init.sh`
Pull Request -
State: closed - Opened by austinletson 3 months ago
#83 - MacOS 14 build failure
Issue -
State: closed - Opened by bollu 3 months ago
- 1 comment
#83 - MacOS 14 build failure
Issue -
State: closed - Opened by bollu 3 months ago
- 1 comment
#82 - Use the Lake manifest to determine Mathlib dependency
Issue -
State: closed - Opened by austinletson 4 months ago
#82 - Use the Lake manifest to determine Mathlib dependency
Issue -
State: closed - Opened by austinletson 4 months ago
#81 - feat: bump functional_tests.yml default version to 4.10.0
Pull Request -
State: closed - Opened by austinletson 4 months ago
#81 - feat: bump functional_tests.yml default version to 4.10.0
Pull Request -
State: closed - Opened by austinletson 4 months ago
#80 - doc: update CHANGELOG.md and README.md for v1.0.0
Pull Request -
State: closed - Opened by austinletson 4 months ago
#80 - doc: update CHANGELOG.md and README.md for v1.0.0
Pull Request -
State: closed - Opened by austinletson 4 months ago
#79 - v1.0.0 release
Issue -
State: closed - Opened by austinletson 4 months ago
- 1 comment
Labels: release
#79 - v1.0.0 release
Issue -
State: closed - Opened by austinletson 4 months ago
- 1 comment
Labels: release
#78 - doc: update RELEASE.md and create release issue template
Pull Request -
State: closed - Opened by austinletson 4 months ago
#78 - doc: update RELEASE.md and create release issue template
Pull Request -
State: closed - Opened by austinletson 4 months ago
#77 - fix: use input instead of hardcoded toolchain in auto-config tests
Pull Request -
State: closed - Opened by austinletson 4 months ago
#77 - fix: use input instead of hardcoded toolchain in auto-config tests
Pull Request -
State: closed - Opened by austinletson 4 months ago
#76 - chore(deps): bump raven-actions/actionlint from 1 to 2
Pull Request -
State: closed - Opened by dependabot[bot] 4 months ago
Labels: dependencies
#76 - chore(deps): bump raven-actions/actionlint from 1 to 2
Pull Request -
State: closed - Opened by dependabot[bot] 4 months ago
Labels: dependencies
#75 - install elan on windows
Issue -
State: closed - Opened by Seasawher 4 months ago
- 4 comments
Labels: enhancement
#75 - install elan on windows
Issue -
State: closed - Opened by Seasawher 4 months ago
- 4 comments
Labels: enhancement
#74 - (DRAFT RFC) Add support for building leanblueprint to lean-action
Issue -
State: open - Opened by austinletson 4 months ago
Labels: enhancement
#74 - (DRAFT RFC) Add support for building leanblueprint to lean-action
Issue -
State: open - Opened by austinletson 4 months ago
Labels: enhancement
#73 - feat: add `lint` input to control the `lake lint` step
Pull Request -
State: closed - Opened by austinletson 4 months ago
- 1 comment
#73 - feat: add `lint` input to control the `lake lint` step
Pull Request -
State: closed - Opened by austinletson 4 months ago
- 1 comment
#72 - chore: bump functional tests default Lean version to 4.9.0
Pull Request -
State: closed - Opened by austinletson 4 months ago
#72 - chore: bump functional tests default Lean version to 4.9.0
Pull Request -
State: closed - Opened by austinletson 4 months ago
#71 - fix: improve GitHub cache keys
Pull Request -
State: closed - Opened by austinletson 5 months ago
#71 - fix: improve GitHub cache keys
Pull Request -
State: closed - Opened by austinletson 5 months ago
#70 - Fix GitHub cache keys to reduce problems with the cache when updating Lean version
Issue -
State: closed - Opened by austinletson 5 months ago
Labels: bug
#70 - Fix GitHub cache keys to reduce problems with the cache when updating Lean version
Issue -
State: closed - Opened by austinletson 5 months ago
Labels: bug
#69 - test: parameterize functional tests by Lean toolchain
Pull Request -
State: closed - Opened by austinletson 5 months ago
- 1 comment
#69 - test: parameterize functional tests by Lean toolchain
Pull Request -
State: closed - Opened by austinletson 5 months ago
- 1 comment
#68 - Update `RELEASING.md` based on improvements to release process
Issue -
State: closed - Opened by austinletson 5 months ago
Labels: documentation
#68 - Update `RELEASING.md` based on improvements to release process
Issue -
State: closed - Opened by austinletson 5 months ago
Labels: documentation
#67 - doc: update CHANGELOG.md for v1.0.0-beta.1 release
Pull Request -
State: closed - Opened by austinletson 5 months ago
#67 - doc: update CHANGELOG.md for v1.0.0-beta.1 release
Pull Request -
State: closed - Opened by austinletson 5 months ago
#66 - v1-beta.1 release
Issue -
State: closed - Opened by austinletson 5 months ago
- 2 comments
Labels: release
#66 - v1-beta.1 release
Issue -
State: closed - Opened by austinletson 5 months ago
- 2 comments
Labels: release
#65 - Save cache even if a build fails
Issue -
State: open - Opened by austinletson 5 months ago
Labels: enhancement
#65 - Save cache even if a build fails
Issue -
State: open - Opened by austinletson 5 months ago
Labels: enhancement
#64 - Problem about caching strategy for Lean
Issue -
State: closed - Opened by SnO2WMaN 5 months ago
- 5 comments
#64 - Problem about caching strategy for Lean
Issue -
State: closed - Opened by SnO2WMaN 5 months ago
- 5 comments
#63 - Parameterize functional tests by lean version.
Issue -
State: closed - Opened by austinletson 5 months ago
Labels: testing, v1-release
#63 - Parameterize functional tests by lean version.
Issue -
State: closed - Opened by austinletson 5 months ago
Labels: testing, v1-release
#62 - bug: run `lake update` and `lean-action` gets an error
Issue -
State: closed - Opened by Seasawher 5 months ago
- 18 comments
Labels: bug
#62 - bug: run `lake update` and `lean-action` gets an error
Issue -
State: closed - Opened by Seasawher 5 months ago
- 18 comments
Labels: bug
#61 - feat: add `auto-config` and `build` inputs.
Pull Request -
State: closed - Opened by austinletson 5 months ago
- 2 comments
#61 - feat: add `auto-config` and `build` inputs.
Pull Request -
State: closed - Opened by austinletson 5 months ago
- 2 comments
#60 - Create `auto-config` input
Issue -
State: closed - Opened by austinletson 5 months ago
- 1 comment
Labels: enhancement, v1-release
#60 - Create `auto-config` input
Issue -
State: closed - Opened by austinletson 5 months ago
- 1 comment
Labels: enhancement, v1-release
#59 - test: verify expected steps ran during functional test
Pull Request -
State: closed - Opened by austinletson 5 months ago
#59 - test: verify expected steps ran during functional test
Pull Request -
State: closed - Opened by austinletson 5 months ago
#58 - build args default should be 'quiet'
Issue -
State: closed - Opened by Seasawher 5 months ago
- 2 comments
#58 - build args default should be 'quiet'
Issue -
State: closed - Opened by Seasawher 5 months ago
- 2 comments
#57 - Leverage Lake's API to determine if a package is downstream of Mathlib
Issue -
State: closed - Opened by austinletson 5 months ago
- 1 comment
Labels: wontfix
#57 - Leverage Lake's API to determine if a package is downstream of Mathlib
Issue -
State: closed - Opened by austinletson 5 months ago
- 1 comment
Labels: wontfix
#56 - Leverage output parameters for `lake build` and `lake test` steps to to verify the expected steps ran during a test
Issue -
State: closed - Opened by austinletson 6 months ago
Labels: enhancement
#56 - Leverage output parameters for `lake build` and `lake test` steps to to verify the expected steps ran during a test
Issue -
State: closed - Opened by austinletson 6 months ago
Labels: enhancement
#55 - feat: don't raise an error if test_runner is not provided
Pull Request -
State: closed - Opened by Seasawher 6 months ago
- 6 comments
#55 - feat: don't raise an error if test_runner is not provided
Pull Request -
State: closed - Opened by Seasawher 6 months ago
- 6 comments
#54 - fix: remove `elan-init` file
Pull Request -
State: closed - Opened by Seasawher 6 months ago
- 3 comments
#54 - fix: remove `elan-init` file
Pull Request -
State: closed - Opened by Seasawher 6 months ago
- 3 comments
#53 - Automatically check if test runner is available
Issue -
State: closed - Opened by Seasawher 6 months ago
- 18 comments
Labels: enhancement
#53 - Automatically check if test runner is available
Issue -
State: closed - Opened by Seasawher 6 months ago
- 18 comments
Labels: enhancement
#52 - test: add functional test for `lake init tomltest .toml`
Pull Request -
State: closed - Opened by austinletson 6 months ago
#52 - test: add functional test for `lake init tomltest .toml`
Pull Request -
State: closed - Opened by austinletson 6 months ago
#51 - refactor: break out functional tests into actions
Pull Request -
State: closed - Opened by austinletson 6 months ago
#51 - refactor: break out functional tests into actions
Pull Request -
State: closed - Opened by austinletson 6 months ago
#50 - Revert "refactor: move functional tests to a dedicated directory"
Pull Request -
State: closed - Opened by austinletson 6 months ago