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

Allowing adding testRunner = true to a lean_lib in lakefile.toml. #4142

Closed
kim-em opened this issue May 12, 2024 · 5 comments · Fixed by #4261
Closed

Allowing adding testRunner = true to a lean_lib in lakefile.toml. #4142

kim-em opened this issue May 12, 2024 · 5 comments · Fixed by #4261
Labels
feature missing feature Lake Lake related issue

Comments

@kim-em
Copy link
Collaborator

kim-em commented May 12, 2024

Aesop uses a library AesopTest as its test suite. It would be nice to have a way to tell lake test about this!

(This is better, I think, than the "pile of lean files + custom exe test runner" approach.)

See zulip discussion.
@kim-em kim-em added feature missing feature Lake Lake related issue labels May 12, 2024
@kim-em kim-em mentioned this issue May 13, 2024
Merged
@JLimperg
Copy link
Contributor

Advantages of this approach:

  • Perfectly incremental tests.
  • Tests which need to import other test files (e.g. anything involving initialize) are supported without any effort.

Disadvantages:

  • AesopTest library is 'accidentally' available publicly.
  • No support for intentionally failing files or golden tests (but guard_msgs suffices for all my use cases).

@kim-em
Copy link
Collaborator Author

kim-em commented May 15, 2024

Noting that ProofWidgets.Demos is effectively another "library as test suite" in the wild.

@kim-em
Copy link
Collaborator Author

kim-em commented May 15, 2024

  • Tests which need to import other test files (e.g. anything involving initialize) are supported without any effort.

Note that Batteries has Batteries/Test/Internal/DummyLabelAttr.lean specifically to jump through this hoop that a test file can't import another test file.

@kim-em kim-em mentioned this issue May 15, 2024
Open
@kim-em
Copy link
Collaborator Author

kim-em commented May 15, 2024

  • AesopTest library is 'accidentally' available publicly.

I've created an issue for this at #4168.

@nomeata
Copy link
Collaborator

nomeata commented May 15, 2024

It’s also the natural idiom I have been using for all my little libraries.

@tydeu tydeu mentioned this issue May 23, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue May 24, 2024
@tydeu
feat: lake test improvements & lake lint (#4261)
0448e3f 
Extends the functionality of `lake test` and adds a parallel command in
`lake lint`.

* Rename `@[test_runner]` / `testRunner` to `@[test_driver]` /
`testDriver`. The old names are kept as deprecated aliases.
* Extend help page for `lake test` and adds one for `lake check-test`. 
* Add `lake lint` and its parallel tag `@[lint_driver]` , setting
`lintDriver`, and checker `lake check-lint`.
* Add support for specifying test / lint drivers from dependencies. 
* Add `testDriverArgs` / `lintDriverArgs` for fixing additional
arguments to the invocation of a driver script or executable.
* Add support for library test drivers (but not library lint drivers). 
* `lake check-test` / `lake check-lint` only load the package (without
dependencies), not the whole workspace.

Closes #4116. Closes #4121. Closes #4142.
@abdoo8080 abdoo8080 mentioned this issue Aug 6, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
feature missing feature Lake Lake related issue
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

feat: lake test improvements & lake lint tydeu/lean4
3 participants
@nomeata @kim-em @JLimperg