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
#50 - Revert "refactor: move functional tests to a dedicated directory"
Pull Request -
State: closed - Opened by austinletson 6 months ago
#49 - refactor: move functional tests to a dedicated directory
Pull Request -
State: closed - Opened by austinletson 6 months ago
#49 - refactor: move functional tests to a dedicated directory
Pull Request -
State: closed - Opened by austinletson 6 months ago
#48 - chore: upgrade elan to `v3.1.1`
Pull Request -
State: closed - Opened by austinletson 6 months ago
#48 - chore: upgrade elan to `v3.1.1`
Pull Request -
State: closed - Opened by austinletson 6 months ago
#47 - feat: add `lake-package-directory` input
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 1 comment
#47 - feat: add `lake-package-directory` input
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 1 comment
#46 - Update the lint step to use the more flexible `lake lint`
Issue -
State: closed - Opened by austinletson 6 months ago
Labels: enhancement, v1-release
#46 - Update the lint step to use the more flexible `lake lint`
Issue -
State: closed - Opened by austinletson 6 months ago
Labels: enhancement, v1-release
#45 - docs: improve README.md inputs usage section
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 2 comments
#45 - docs: improve README.md inputs usage section
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 2 comments
#44 - feat: add `use-github-cache` input
Pull Request -
State: closed - Opened by austinletson 6 months ago
#44 - feat: add `use-github-cache` input
Pull Request -
State: closed - Opened by austinletson 6 months ago
#43 - fix: rename misleading functional tests job
Pull Request -
State: closed - Opened by austinletson 6 months ago
#43 - fix: rename misleading functional tests job
Pull Request -
State: closed - Opened by austinletson 6 months ago
#42 - fix: remove misleading .toml error message in mathlib detection
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 1 comment
#42 - fix: remove misleading .toml error message in mathlib detection
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 1 comment
#41 - feat: add white space after each step
Pull Request -
State: closed - Opened by austinletson 6 months ago
#41 - feat: add white space after each step
Pull Request -
State: closed - Opened by austinletson 6 months ago
#40 - Mathlib detection prints unnecessary error when lakefile.toml not present
Issue -
State: closed - Opened by kim-em 6 months ago
Labels: bug
#40 - Mathlib detection prints unnecessary error when lakefile.toml not present
Issue -
State: closed - Opened by kim-em 6 months ago
Labels: bug
#39 - docs: release notes for v1-beta
Pull Request -
State: closed - Opened by austinletson 6 months ago
#39 - docs: release notes for v1-beta
Pull Request -
State: closed - Opened by austinletson 6 months ago
#38 - Add an option to disable GitHub caching
Issue -
State: closed - Opened by austinletson 6 months ago
Labels: enhancement
#38 - Add an option to disable GitHub caching
Issue -
State: closed - Opened by austinletson 6 months ago
Labels: enhancement
#37 - v1-beta release
Issue -
State: closed - Opened by austinletson 6 months ago
- 1 comment
Labels: release
#37 - v1-beta release
Issue -
State: closed - Opened by austinletson 6 months ago
- 1 comment
Labels: release
#36 - format: fix yaml formatting in README.md
Pull Request -
State: closed - Opened by austinletson 6 months ago
#36 - format: fix yaml formatting in README.md
Pull Request -
State: closed - Opened by austinletson 6 months ago
#35 - test: add workflow to run basic functional tests
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 1 comment
#35 - test: add workflow to run basic functional tests
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 1 comment
#34 - Support repositories with subdirectory Lean packages
Issue -
State: closed - Opened by austinletson 6 months ago
Labels: enhancement
#34 - Support repositories with subdirectory Lean packages
Issue -
State: closed - Opened by austinletson 6 months ago
Labels: enhancement
#33 - doc: add examples of projects which use `lean-action`
Pull Request -
State: closed - Opened by austinletson 6 months ago
#33 - doc: add examples of projects which use `lean-action`
Pull Request -
State: closed - Opened by austinletson 6 months ago
#32 - doc: add example of environment usage in later steps
Pull Request -
State: closed - Opened by austinletson 6 months ago
#32 - doc: add example of environment usage in later steps
Pull Request -
State: closed - Opened by austinletson 6 months ago
#31 - feat: add `lake check-test` check before running `lake test`
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 2 comments
#31 - feat: add `lake check-test` check before running `lake test`
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 2 comments
#30 - Add option to disable `lake build`
Issue -
State: closed - Opened by Seasawher 6 months ago
- 8 comments
Labels: enhancement
#30 - Add option to disable `lake build`
Issue -
State: closed - Opened by Seasawher 6 months ago
- 8 comments
Labels: enhancement
#29 - fix: rename `mathlib-cache` -> `get-mathlib-cache` and improve interface
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 2 comments
#29 - fix: rename `mathlib-cache` -> `get-mathlib-cache` and improve interface
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 2 comments
#28 - feat: convenience workflow for update major release tag
Pull Request -
State: open - Opened by oliver-butterley 6 months ago
- 1 comment
#28 - feat: convenience workflow for update major release tag
Pull Request -
State: open - Opened by oliver-butterley 6 months ago
- 1 comment
#27 - feat: add `build-args` input
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 2 comments
#27 - feat: add `build-args` input
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 2 comments
#26 - Use `lake check-test` to detect absence of a test runner
Issue -
State: closed - Opened by kim-em 6 months ago
- 3 comments
Labels: enhancement
#26 - Use `lake check-test` to detect absence of a test runner
Issue -
State: closed - Opened by kim-em 6 months ago
- 3 comments
Labels: enhancement
#25 - Inconsistency with `mathlib-cache` input
Issue -
State: closed - Opened by oliver-butterley 6 months ago
- 6 comments
#25 - Inconsistency with `mathlib-cache` input
Issue -
State: closed - Opened by oliver-butterley 6 months ago
- 6 comments
#24 - feat: add a step that logs the version of lake and lean
Pull Request -
State: closed - Opened by oliver-butterley 6 months ago
- 6 comments
#24 - feat: add a step that logs the version of lake and lean
Pull Request -
State: closed - Opened by oliver-butterley 6 months ago
- 6 comments
#23 - doc: add RELEASING.md and CHANGELOG.md
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 1 comment
#23 - doc: add RELEASING.md and CHANGELOG.md
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 1 comment
#22 - doc: add CONTRIBUTING.md
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 2 comments
#22 - doc: add CONTRIBUTING.md
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 2 comments
#21 - add version info
Pull Request -
State: closed - Opened by Seasawher 6 months ago
- 4 comments
#21 - add version info
Pull Request -
State: closed - Opened by Seasawher 6 months ago
- 4 comments
#20 - feat: group log outputs by step (#19)
Pull Request -
State: closed - Opened by austinletson 6 months ago
#20 - feat: group log outputs by step (#19)
Pull Request -
State: closed - Opened by austinletson 6 months ago
#19 - Improve log readability by grouping log lines inside of steps
Issue -
State: closed - Opened by austinletson 6 months ago
Labels: enhancement
#19 - Improve log readability by grouping log lines inside of steps
Issue -
State: closed - Opened by austinletson 6 months ago
Labels: enhancement
#18 - :memo: Update README.md to recommend dependabot
Pull Request -
State: closed - Opened by oliver-butterley 6 months ago
#18 - :memo: Update README.md to recommend dependabot
Pull Request -
State: closed - Opened by oliver-butterley 6 months ago
#17 - :sparkles: Add dependabot to notify when actions are updated
Pull Request -
State: closed - Opened by oliver-butterley 6 months ago
- 1 comment
#17 - :sparkles: Add dependabot to notify when actions are updated
Pull Request -
State: closed - Opened by oliver-butterley 6 months ago
- 1 comment
#16 - ✨ relocate checkout
Pull Request -
State: closed - Opened by oliver-butterley 6 months ago
- 1 comment
#16 - ✨ relocate checkout
Pull Request -
State: closed - Opened by oliver-butterley 6 months ago
- 1 comment
#15 - Add input to support passing parameters to `lake build`
Issue -
State: closed - Opened by austinletson 6 months ago
- 5 comments
Labels: enhancement
#15 - Add input to support passing parameters to `lake build`
Issue -
State: closed - Opened by austinletson 6 months ago
- 5 comments
Labels: enhancement
#14 - Document use cases where additional Lean CI steps are taken after `lean-action`
Issue -
State: closed - Opened by austinletson 6 months ago
Labels: documentation
#14 - Document use cases where additional Lean CI steps are taken after `lean-action`
Issue -
State: closed - Opened by austinletson 6 months ago
Labels: documentation
#13 - Add existing usage examples to README.md
Issue -
State: closed - Opened by austinletson 6 months ago
Labels: documentation
#13 - Add existing usage examples to README.md
Issue -
State: closed - Opened by austinletson 6 months ago
Labels: documentation
#12 - Enhance version information logging
Issue -
State: closed - Opened by austinletson 6 months ago
Labels: enhancement
#11 - chore: rename Std to Batteries
Pull Request -
State: closed - Opened by kim-em 6 months ago
#10 - Std is renamed Batteries
Issue -
State: closed - Opened by Seasawher 6 months ago
#9 - fix: add lakefile.tom detection to detect_mathlib.sh
Pull Request -
State: closed - Opened by austinletson 6 months ago
#8 - chore: add shebangs to scripts
Pull Request -
State: closed - Opened by kim-em 6 months ago
#7 - chore: add ShellCheck action
Pull Request -
State: closed - Opened by kim-em 6 months ago
- 2 comments
#6 - detect_mathlib assumes a lakefile.lean; should also support lakefile.toml
Issue -
State: closed - Opened by kim-em 6 months ago
#5 - feat: add support for lean4checker
Pull Request -
State: closed - Opened by austinletson 6 months ago
- 2 comments
#4 - v1-alpha release
Issue -
State: closed - Opened by austinletson 7 months ago
- 4 comments
Labels: release
#3 - Redundant mathlib caching
Issue -
State: open - Opened by austinletson 7 months ago
- 2 comments
Labels: enhancement
#2 - Automatically detect module for `lake exe runLinter`
Issue -
State: closed - Opened by austinletson 7 months ago
- 16 comments
Labels: enhancement
#1 - Add support for `lean4checker`
Issue -
State: closed - Opened by austinletson 7 months ago