Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: test_extern command #2970

Merged
merged 12 commits into from
Dec 13, 2023
Merged

feat: test_extern command #2970

merged 12 commits into from
Dec 13, 2023

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Nov 28, 2023 •
edited
Loading

This adds a test_extern command.

Usage:

import Lean.Util.TestExtern

test_extern Nat.add 17 37

This:

  • Checks that the head symbol has an @[extern] attribute.
  • Writes down t == t', where t is the term provided, and t' is the reference implementation (specifically, t with the head symbol unfolded).
  • Tries to reduce this to true, and complains if this fails.

Note that the type of the term must have a BEq instance for this to work: there's a self-explanatory error message if it isn't available.

@kim-em kim-em added the awaiting-review Waiting for someone to review the PR label Nov 28, 2023
@kim-em kim-em marked this pull request as ready for review November 28, 2023 01:50
nomeata
nomeata approved these changes Nov 28, 2023
View reviewed changes
Copy link
Collaborator

@nomeata nomeata left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very neat

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 1, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 1, 2023
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#2970
d412aa0
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Dec 1, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Dec 1, 2023 •
edited
Loading

@leodemoura leodemoura removed the awaiting-review Waiting for someone to review the PR label Dec 1, 2023
@leodemoura leodemoura enabled auto-merge December 1, 2023 14:42
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 2, 2023
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#2970
e0020c6
@leodemoura leodemoura added this pull request to the merge queue Dec 2, 2023
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Dec 2, 2023
@kim-em kim-em added the full-ci label Dec 2, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 12, 2023
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#2970
b530cd9
@kim-em kim-em added this pull request to the merge queue Dec 12, 2023
Merged via the queue into master with commit d4dca3b Dec 13, 2023
17 checks passed
@digama0
Copy link
Collaborator

digama0 commented Dec 13, 2023 •
edited
Loading

Note that the type of the term must have a BEq instance for this to work: there's a self-explanatory error message if it isn't available.

I think this should be using a DecidableEq instance, not a BEq instance, because this is guarding against values that are different in any way. Even if the difference is ignored by BEq this is still bad.

Also this is equally useful for implemented_by.

@kim-em kim-em mentioned this pull request Dec 15, 2023
Merged
github-merge-queue bot pushed a commit that referenced this pull request Apr 24, 2024
@kim-em
feat: improvements to test_extern command (#3075)
41697dc 
Two improvements
[suggested](#2970 (comment))
by @digama0 after the initial PR was merged.

* Allow testing `implemented_by` attributes as well.
* Use `DecidableEq` rather than `BEq` for stricter testing.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@nomeata nomeata nomeata approved these changes

@leodemoura leodemoura leodemoura approved these changes

@Kha Kha Awaiting requested review from Kha

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@kim-em @leanprover-community-mathlib4-bot @digama0 @nomeata @leodemoura