feat: improvements to test_extern command #3075
Merged
Conversation
This file contains 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
github-actions
bot
added
the
toolchain-available
|
digama0
reviewed
Dec 15, 2023
| test_extern.lean:7:0-7:17: error: test_extern: HAdd.hAdd does not have an @[extern] attribute | ||
| test_extern.lean:9:0-9:86: error: native implementation did not agree with reference implementation! | ||
| test_extern.lean:6:0-6:17: error: test_extern: HAdd.hAdd does not have an @[extern] attribute or @[implemented_by] attribute | ||
| test_extern.lean:8:0-8:86: error: native implementation did not agree with reference implementation! | ||
| Compare the outputs of: |
There was a problem hiding this comment.
Why does the error message say to compare the outputs instead of showing what the outputs are? I think it should actually print the outputs (when possible), because these issues can be OS dependent so it's important to know what value was actually produced in CI since they may not reproduce locally.
There was a problem hiding this comment.
That's a good suggestion, but I'd prefer not to take it on now. Happy to either open an issue, let you do that. Or, for that matter, to accept commits on this PR, or promise to review a new PR! :-)
|
Another improvement I found a need for in #3961 was to allow specifying the desired result which both versions of the function should evaluate to. |
2 tasks
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.
Two improvements suggested by @digama0 after the initial PR was merged.
implemented_byattributes as well.DecidableEqrather thanBEqfor stricter testing.