lake test

Stream: general

[Kim Morrison]

@Mac Malone, some libraries, e.g. Aesop, have a lean_lib for their test suite.

I'm pretty sure there's currently no way to annotate a lean_lib with testRunner, is that right? Would this be difficult to add?

[Mac Malone]

I don't know what running a library would mean.

[Kim Morrison]

building it

[Kim Morrison]

currently ./test in Aesop is just lake build AesopTest

[Mac Malone]

how does that work?

[Kim Morrison]

I'm confused by your question:

% cat test
#!/usr/bin/env bash

env LEAN_ABORT_ON_PANIC=1 lake build AesopTest

[Mac Malone]

so that menas, that once a test passes it can't be run again?

[Kim Morrison]

I mean, you can lake clean? And if dependencies change it will automatically run again. Seems like the desired behaviour, in fact?

[Mac Malone]

I mean, I guess? That seems like kind of an abuse of the concept of building a library.

[Kim Morrison]

So, what do we tell Aesop, then? "No, you can't have lake test replace ./test unless you ..."?

[Mac Malone]

I would generally default to the Batteries-style test runner for this. However, I will consider this style of testing library some more -- maybe it is worth supporting in the future? It is an interesting idea.

[Kim Morrison]

The batteries style test runner is insufficient here.

[Kim Morrison]

AesopTest has files that import other files in AesopTest

[Kim Morrison]

which we can't do in the "pile of lean files" test suite that Batteries and Mathlib currently use

[Kim Morrison]

To be honest, I think we should just switch all test suites to lean_libs.

[Eric Wieser]

Note that there is precedent in other systems for tests that are nothing other than "does this target build", such as in bazel

[Kim Morrison]

This would also mean we could ditch the ad-hoc test runner I wrote for Batteries, and instead just rely on lake's much more reliable build system!

[Kim Morrison]

I created lean#4142 to track this.

[Kim Morrison]

I'd love to sort out these lake test issues sooner rather than later. The lean-action repository is going to assume that lake test is the entry point for testing, and I would like to allow people to start using that everywhere if possible.

If either or both of lean#4142 (lean_lib as test runner) and lean#4121 (allow using upstream executable as testRunner) were available in time I would love to backport these to v4.8.0-rc2 so we can get started using lake test without just copying and pasting the Batteries test runner everywhere.

[Mario Carneiro]

Also it's not that weird for testing a lean project to entail building some files, since files can use #eval and #guard_msgs etc to move testing to compile time

[Kim Morrison]

Yes. #guard_msgs is basically our preferring testing mechanism at this point. Obviously it doesn't cover everything, but perhaps 99%!

[Mario Carneiro]

any project which is primarily about metaprogramming (e.g. a tactic library) will probably have all its tests at build time

[Mario Carneiro]

and TBH that's the majority of lean projects (with tests) right now

[Mario Carneiro]

Agreed that the Batteries test battery is a hack and should be replaced by lean_lib

[Mario Carneiro]

although it would be nice to have lean_libs that can't be imported for this purpose

[Utensil Song]

If all tests will be using lean_lib, is there a way to flexibly include/exclude tests, or mark tests as skip/broken (test libs in other languages could)? For a lean_lib the former can be achieved by glob, I don't know about the rest. For now it seems the only solution is to move the to-skip/broken tests to separate directories, but that would confuse git when merging these moves with modifications to the tests.

[Kim Morrison]

@Utensil Song, I think these questions apply equally well to the test runner in batteries#787.

[Kim Morrison]

This is stuff that we can ask for in later, full-featured test runners, but I don't think should block anything we're doing right now.

I'm not really a fan of supporting broken tests in a test runner, anyway. You comment it out, and create an issue, no?

[Utensil Song]

Yes. I don't mean them to be blocking issues of using lean_lib which seems to a nice improvement.

[Utensil Song]

Kim Morrison said:

I'm not really a fan of supporting broken tests in a test runner, anyway. You comment it out, and create an issue, no?

I used to have them marking test cases that fail for certain combination of inputs in other languages, e.g.733BCA30-2FCF-4410-8972-61C6E077C403.jpg which is very flexible in a situation where fixing the test for some inputs will break for other inputs, this makes it clear that which tests should pass but are broken for now. A issue can only describe the general situation, and these executable marks will keep tracking what's going on specifically and more maintainable than comments.

[Utensil Song]

Just noticed that lake test is not documented in https://github.com/leanprover/lean4/blob/master/src/lake/README.md , or is there another reference?

[Kim Morrison]

No, I don't think is documented yet. Issue (asking for documentation) or PR (adding some!) very welcome.

[Ruben Van de Velde]

It can be valuable to keep running tests that fail so that ci tells you when they start passing again, as well

[Kim Morrison]

I think in the lean_lib scenario this will be okay: successive failures of lake build AesopTest show the failure error each time.

[Utensil Song]

Kim Morrison said:

No, I don't think is documented yet. Issue (asking for documentation) or PR (adding some!) very welcome.

In light of lean4#4116, I'll settle for lake test --help for now. The doc is subject to changes anyway.

[Kim Morrison]

Mario Carneiro said:

although it would be nice to have lean_libs that can't be imported for this purpose

There's now an issue tracking this at lean#4168.

[Bernardo Borges]

Hello. In leanprover/lean4:v4.8.0-rc2 adding @[test_runner] triggers the error:

unexpected token '@['; expected 'abbrev', 'axiom', 'binder_predicate', 'builtin_initialize', 'class', 'def', 'elab', 'elab_rules', 'example', 'extern_lib', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'lean_exe', 'lean_lib', 'library_facet', 'macro', 'macro_rules', 'module_facet', 'notation', 'opaque', 'package', 'package_facet', 'post_update', 'postfix', 'prefix', 'script', 'structure', 'syntax', 'target' or 'theorem'

[Bernardo Borges]

Are there examples of usage?

[Kim Morrison]

Use @[test_driver] instead. (Although I thought there was a deprecation warning for this, not an error, so something else might be wrong with your setup.)

[Kim Morrison]

If @[test_driver] doesn't solve the problem, can you please post your lakefile.lean?

[Mac Malone]

@Kim Morrisonm @Bernardo Borges error is on v4.8.0-rc2 before the new test improvements. It seems like they may be putting the attribute on something that does not support attribues. @Bernardo Borges, could you post your lakefile.lean and show were you are adding the attribute?

[Bernardo Borges]

To be frank I could get rid of the error, it's just that I couldn't find documentation that explains how to make the script trigger the /test folder:

import Lake
open Lake DSL

package «lean-cutting-planes» where

require mathlib from git
  "https://github.com/leanprover-community/mathlib4"

lean_lib «LeanCuttingPlanes» where

@[test_runner]
script tests do
  return 0


@[default_target]
lean_exe «lean-cutting-planes» where
  root := `Main

[Kim Morrison]

Ah, at this point @[test_driver] / @[test_runner] can only be put on a lean_exe.

[Kim Morrison]

On v4.9.0-rc1, hopefully coming out soon, you can also put it on a lean_lib (having the effect of just building that lib).

[Kim Morrison]

I think a script is still not supported. Could you open an issue if you think there's a workflow supported by a script that wouldn't be possible otherwise?

[Bernardo Borges]

I'm setting this up just now so I don't have a workflow yet. What I would like to do is similar to the lean_lib you mentioned, where my ci will try to build the test folder

[Mac Malone]

Kim Morrison said:

I think a script is still not supported. Could you open an issue if you think there's a workflow supported by a script that wouldn't be possible otherwise?

A script is supported (in fact, it is the most preferrd in the ordering).

[Bernardo Borges]

Interesting! Is there a script that attempts to build all lean files in a directory?

[Kim Morrison]

My preference is that people avoid the use of scripts for now, as they are only supported in lakefile.lean, while I hope as many projects as possible will use lakefile.toml instead.

[Bernardo Borges]

Why is a .toml preferred now?

[Kim Morrison]

Simplicity. It's always better to use a non-interpreted configuration file if you can, instead of having your configuration file being an arbitrary piece of interpreted code.

[Bernardo Borges]

Interesting, will this be the standard option when lake new is run?

[Kim Morrison]

This is proposed in lean#4106, but a final decision hasn't been made.