Making Mathlib tests into a library

Stream: mathlib4

[Kim Morrison]

I would like to convert Mathlib's tests to a lake library. This means:

• we don't need to depend on the ad-hoc test runner I implemented in Batteries
• it is possible for Mathlib tests to import other files from Mathlib tests (e.g. so it is possible to properly test linter.minImports)

I created #18304 to attempt this, but lake build MathlibTests then runs with all the Mathlib linters, despite me not asking for them in

lean_lib MathlibTest where
  globs := #[.submodules `MathlibTest]

@Mac Malone, or anyone else who knows lake well enough, ... Could I please have some assistance here?

[Mac Malone]

@Kim Morrison The mathlib linters are set globally (as weak options) on the package declaration.

[Kim Morrison]

Can I turn them off again?

[Mac Malone]

Lake does not provide a way to subtract options, so they would have to be individual set (or not set) on the each target.

[Damiano Testa]

Would having an extra linter.test option set that enables/disables all linters when you are in a test.something file help?

[Damiano Testa]

Each linter would then use the combination of its own option and this "global test" option to decide whether to run or not.

[Kim Morrison]

Okay, I will just move those options from the package to the lean_lib Mathlib, so they don't affect the tests.

[Kim Morrison]

Okay, that works fine.

[Kim Morrison]

@Moritz Firsching and @Damiano Testa, I don't understand the (now failing) test

/-- info: [termG, termG] -/
#guard_msgs in
open Lean in
run_meta
  let env ← getEnv
  let consts := env.constants.toList.find? (·.1.getRoot == `termG)
  let reps := (consts.map (·.1.components.take 2)).getD default
  logInfo m!"{reps}"
  guard (reps[0]! == reps[1]!)
end termG

in MathlibTest/Lint.lean, which was added in #17631.

Would one of you mind looking at it on the test_lib branch, and doing some combination of fixing it / documenting what it is actually testing / explaining to me?

[Damiano Testa]

I'll take a look now. The test was a little hack: I wanted to make sure that "auto-generated" names with a repeated namespace would get caught by the linter. So, I used a term... autogenerated name: since these added term automatically, I rigged the namespace to contain a termG repetition.

[Damiano Testa]

It looks like the heuristics for the auto-generated name depend on the path... Probably it is easiest to remove the test: I was not too convinced by it to begin with.

[Kim Morrison]

If we would like to merge this, I would appreciate a speedy review. This PR #18304 will rot quickly, and every time we need to merge it is a rebuild from scratch because we touch the lakefile.

[Damiano Testa]

I personally like the idea of having a separate test library!

[Kim Morrison]

I don't think there's any opposition. The PR just needs a review for me being dumb. :-)

[Damiano Testa]

Ah, ok, let me look at it again! I was surprised that not more linters required changes: I thought that some of them inspected whether the root of the module name was test or not.

[Damiano Testa]

Was the MathlibTest.lean file generated by mk_all?

[Kim Morrison]

Yes

[Damiano Testa]

For me, the main test will be to see the PR pass CI.

[Damiano Testa]

Damiano Testa said:

Ah, ok, let me look at it again! I was surprised that not more linters required changes: I thought that some of them inspected whether the root of the module name was test or not.

I think that HashCommandLinter looks at the path to decide whether to run or not. I can switch that to a separate option or just perpetrate the hack by renaming the root of the path.

[Damiano Testa]

There are also a few comments in Mathlib that refer to test/.... I found them with

git grep '`test\b[^ ]' Mathlib/*

[Damiano Testa]

(If you prefer, I can push those renames directly to the branch.)

[Damiano Testa]

Actually, I just tested the new setup and the linters appear to be automatically disabled in MathlibTest, and they have to be explicitly opted in to view their reports. This means that the HashCommandLinter hack can simply be removed and nothing should break.

[Damiano Testa]

The current test error seems to be an inductive C defined in both MathlibTest/DeriveFintype.lean and MathlibTest/DeriveToExpr.lean.

[Eric Wieser]

What's the benefit of having MathlibTest.lean?

[Kim Morrison]

Do you mean as opposed to using a glob? We need one or the other, and given we don't use globs for Mathlib, I assumed we wouldn't want to here either.

[Kim Morrison]

Just fixed another round of merge conflicts.

[Kim Morrison]

I've switched back to using globs, so that name collisions in the test files are allowed.