Add Lean action in CI #10
Merged
Conversation
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
|
This is an example run in my fork: https://github.com/zhassan-aws/rust-lean-models/actions/runs/10584292641/job/29328218478 |
|
Does the action have some issues? It seems it is trying to save the cache twice (and the second one fails). |
tautschnig
approved these changes
Aug 27, 2024
|
Good catch. I'm seeing this error in other repos that use the action though, e.g: Not sure what the error means. |
Yes, this doesn't seem to be an issue with how you use it. It just makes me wonder about the quality of the action itself. Might just need some engaging with the action to help them improve it. |
|
Created leanprover/lean-action#96 to ask about the error. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Add Lean action in CI to make sure the package doesn't break.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.