assert_not_imported

Stream: Is there code for X?

[Damiano Testa]

There is an assert_not_exists command that checks whether a specific declaration is not present in the environment.

Should there be an analogous assert_not_imported command that checks whether a module is imported or not?

[Johan Commelin]

Would make sense, I guess

[Johan Commelin]

But do you have particular examples in mind already?

[Michael Rothgang]

This came up in #15732, in Mathlib/Algebra/Field/Defs.lean

[Damiano Testa]

Yes, my only usecase is the one that Michael mentioned.

[Kim Morrison]

I've definitely encountered the problem of wanting to exclude a module, and then having to dig through it for a stable looking declaration to exclude instead, so +1 from me.

[Yury G. Kudryashov]

What if someone renames the module?

[Kim Morrison]

Damiano has already been setting up infrastructure to check at the end that everything asserted about eventually exists. I presume such a system would catch that case. A split would be more complicated, and I agree that it seems likely regressions could slip through.

[Damiano Testa]

Yes, files no longer existing could be caught by the same mechanism that catches declarations no longer existing. Maybe, once a missing file is detected, the error message could suggest to discuss on Zulip how to proceed.

[Damiano Testa]

Here is a possible implementation. Checking for existing files will not works in the online server, I think, since I do not really know how the filepaths work there.

import Mathlib.Tactic.Linter

open Lean in
elab "assert_not_imported " ids:ident* : command => do
  let mods := (← getEnv).allImportedModuleNames
  for id in ids do
    if mods.contains id.getId then logWarningAt id m!"'{id}' is imported"
    if let none ← (← searchPathRef.get).findModuleWithExt "olean" id.getId then
      logWarningAt id m!"'{id}' does not exist"

assert_not_imported
  Mathlib.Tactic.Common  -- ok
  Lean.Elab.Command  -- 'Lean.Elab.Command' is imported
  I_do_not_exist  -- 'I_do_not_exist.lean' does not exist

If someone using a system other than Linux could check that this works as intended there, it would be great!

[Kim Morrison]

Works on macos!

[Damiano Testa]

Ok, let me prepare a PR, then! Since the above works on my computer, it works on MacOs and also works on the online server, how could it possibly fail on any system? :smile:

[Damiano Testa]

#15769

[Michael Rothgang]

#15782 uses this for the file which inspired this thread. :-)

[Michael Rothgang]

branch#MR-use-ane observes three further stale comments, which look like they ought to use this command, but the referenced file Data.Nat.Order.Basic does not exist any more.

@Yaël Dillies That sounds like you might have performed this split: can you suggest how to update the comment best? I'm unsure whether to update the comment or use assert_not_imported instead, but the current state is surely suboptimal :-)

[Yaël Dillies]

Order.Nat.Basic should be the file

[Michael Rothgang]

Damiano Testa said:

#15769

In #15783, I'm proposing a small wording tweak (and changing on warning to an error).

[Michael Rothgang]

Fast reviews are great - but then we should embrace follow-up PRs for any small things we notice later :-)

[Michael Rothgang]

Yaël Dillies said:

Order.Nat.Basic should be the file

There only exists Order.Nat; do you mean that? (Update: doesn't look like it; that file is virtually empty)

[Damiano Testa]

Michael Rothgang said:

#15782 uses this for the file which inspired this thread. :-)

This looks great! I just have a small doubt, thinking ahead about the linter: should assert_not_exists and assert_not_imported appear in a specific order, or should they just float to the top of each file, preceded only by imports and doc-strings, but with no fixed relative order between them?

[Yaël Dillies]

Michael Rothgang said:

Yaël Dillies said:

Order.Nat.Basic should be the file

There only exists Order.Nat; do you mean that? (Update: doesn't look like it; that file is virtually empty)

Ah sorry, Algebra.Order.Nat is what I mean

[Michael Rothgang]

Yaël Dillies said:

Michael Rothgang said:

Yaël Dillies said:

Order.Nat.Basic should be the file

There only exists Order.Nat; do you mean that? (Update: doesn't look like it; that file is virtually empty)

Ah sorry, Algebra.Order.Nat is what I mean

Doesn't exist either...

[Yaël Dillies]

Algebra.Order.Group.Nat :grinning:

[Michael Rothgang]

Damiano Testa said:

Michael Rothgang said:

#15782 uses this for the file which inspired this thread. :-)

This looks great! I just have a small doubt, thinking ahead about the linter: should assert_not_exists and assert_not_imported appear in a specific order, or should they just float to the top of each file, preceded only by imports and doc-strings, but with no fixed relative order between them?

Good question! I don't feel strongly about ordering them - but also wouldn't mind enforcing some order. (If nothing else, alphabetical comes to mind.)

[Michael Rothgang]

Yaël Dillies said:

Algebra.Order.Group.Nat

Thanks, that solved it. (I needed to prefix with Mathlib, but that's fine.)

[Michael Rothgang]

Fun fact: assert_not_imported assert_not_imported Mathlib.Algebra.Order.Group.Nat leaves no error: is this supposed to happen?
(Sometimes copy-pasting is useful, I guess...)

[Damiano Testa]

Ah, assert_not_imported takes a sequence of identifiers as input, but does not guard that the sequence is non-empty!

[Damiano Testa]

Feel free to fix this, or I'll do it tomorrow, very likely.

[Damiano Testa]

Michael Rothgang said:

Fun fact: assert_not_imported assert_not_imported Mathlib.Algebra.Order.Group.Nat leaves no error: is this supposed to happen?
(Sometimes copy-pasting is useful, I guess...)

#15795

[Damiano Testa]

Michael Rothgang said:

Damiano Testa said:

Michael Rothgang said:

#15782 uses this for the file which inspired this thread. :-)

This looks great! I just have a small doubt, thinking ahead about the linter: should assert_not_exists and assert_not_imported appear in a specific order, or should they just float to the top of each file, preceded only by imports and doc-strings, but with no fixed relative order between them?

Good question! I don't feel strongly about ordering them - but also wouldn't mind enforcing some order. (If nothing else, alphabetical comes to mind.)

I probably prefer "imports first, declarations later" (so, reverse alphabetical, I guess!). This is also what you did in your PR, I think.

[Michael Rothgang]

Damiano Testa said:

Michael Rothgang said:

Damiano Testa said:

Michael Rothgang said:

#15782 uses this for the file which inspired this thread. :-)

This looks great! I just have a small doubt, thinking ahead about the linter: should assert_not_exists and assert_not_imported appear in a specific order, or should they just float to the top of each file, preceded only by imports and doc-strings, but with no fixed relative order between them?

Good question! I don't feel strongly about ordering them - but also wouldn't mind enforcing some order. (If nothing else, alphabetical comes to mind.)

I probably prefer "imports first, declarations later" (so, reverse alphabetical, I guess!). This is also what you did in your PR, I think.

That's a good argument!

[Damiano Testa]

The implementation of assert_not_imported x has the issue that it looks for the .oleans of file x and hence reports as non-existing files that simply have not yet been built.

[Damiano Testa]

This is an issue in CI, when lake build is being run the first time.

[Damiano Testa]

Of course, searching for the .lean files is an alternative that does not require a build, but does require knowing where to look for them!

[Damiano Testa]

For something such as assert_not_exists Mathlib.Data.Nat.Basic, this is completely straightforward. However for assert_not_exists Lean.Elab.Command I was not able to tease out of Lean the filepath to the .lean file, rather than the .olean file that may not yet exist.

[Damiano Testa]

Does anyone know how to go from Lean.Elab.Command to the location where the file Lean/Elab/Command.lean should be?

[Kim Morrison]

Haha, I dimly remember having thought about this before, but when I went looking only found:

-- TODO allow finding Lean 4 sources from the toolchain.
def findLean (mod : Name) : IO FilePath := do
  return FilePath.mk ((← findOLean mod).toString.replace ".lake/build/lib/" "") |>.withExtension "lean"

[Eric Wieser]

I have a version of this somewhere that uses LEAN_SRC_PATH.

[Yaël Dillies]

@Damiano Testa said:

The implementation of assert_not_imported x has the issue that it looks for the .oleans of file x and hence reports as non-existing files that simply have not yet been built.

Is this why #11582 is failing CI?

[Yaël Dillies]

Maybe let's revert assert_not_imported until it's more stable?

[Matthew Ballard]

I think its fine to leave in for now. It is currently unused. I think it'll get fixed pretty soon (no pressure :wink: ).

[Damiano Testa]

I am definitely feeling the "no pressure"! :smile:

[Damiano Testa]

I really think that this should be easy. After all, if I write import X in a file in the project, Lean knows where to look for X:

• if it finds oleans, great (and I know how to replicate this);
• if it does not find oleans, it still knows how to locate the potential candidate source -- this is what I would like to access!

[Damiano Testa]

Here is a partial explanation of why I did not pick up on this.

• If you have a "working" version of Mathlib, then the oleans are there, maybe outdated, but are present.
• If you write a test file, it gets processed by CI, after it built mathlib, and in particular, the appropriate oleans are already there.
• During the regular built, it may be that the oleans for the non-imported files have already been built anyway, and the command finds them!

[Damiano Testa]

So, it is really only some (likely most, but certainly not all) CI runs that fail.

[Matthew Ballard]

Why not throw an error on linting if the declaration or module doesn’t exist in the environment at that time? I recognize immediate feedback is better but this at least improves the status quo. Or did some one suggest that and I’m just not paying attention…

[Michael Rothgang]

Isn't that what the linter currently doesdid before the revert, and this failed CI?

[Michael Rothgang]

(Or rather: it fails CI at (seemingly) unpredictable moments, on unrelated PRs.)

[Matthew Ballard]

I’ve only ever seen assert_not_exists silently fail when the name is mistyped. Did that get fixed?

[Damiano Testa]

The command that is causing problems now is just a straightforward "search for the olean and fail otherwise", it is not a linter.

[Damiano Testa]

Also, there are two commands: assert_not_exists that checks declaration names and assert_not_imported that checks modules.

[Damiano Testa]

The assert_not_exists (for declarations) only checks that a declaration with that name does not exist but does not attempt to check if "later on" it will exist.

[Damiano Testa]

There is a script to check for that, but the issues are now caused by the new import check.

[Damiano Testa]

I think that the unpredictability of the failure is due to the fact that Lean could have created the oleans for the file (maybe they are now obsolete, but they are still there) or may not have when you issue the command.

[Damiano Testa]

I think that an easy solution for now is to just not allow assert_not_imported to check for non-mathlib imports and just say that those never exist.

[Damiano Testa]

In the case of Mathlib files, it is easy enough to search for the .lean files and fail if you find nothing.

[Damiano Testa]

If you were looking for Lean.Elab.Command the command will tell you that the file does not exist (even though it can check whether or not it is imported).

[Damiano Testa]

Maybe, for the time being, this is a good compromise: assert_not_imported (in Mathlib).

[Damiano Testa]

That will not cause CI issues, it will just flag as incorrectly non-existing files that are in mathlib dependencies.

[Damiano Testa]

Ok, TL;DR: I am going to modify assert_not_imported x as follows:

• for any x, it complains if x is imported by the current module;
• if x starts with Mathlib., then also check that the file does indeed exist in Mathlib.

The gap that this leaves with the "ideal" implementation is that it does not report when you are trying to ban a file in a dependency that does not exist.

[Matthew Ballard]

Maybe I am not clear. (Or maybe I am and saying something silly.) I am saying: add an environmental linter which captures the assert_not_exists/imported commands and runs when everything is built.

[Damiano Testa]

Ah, yes, this was indeed a second step!

[Damiano Testa]

I wasam just trying to "salvage" quickly the assert_not_imported command, before adding functionality.

[Matthew Ballard]

Oh. I think using IO opens you up to too many edges cases for not enough gain, especially if there is going to be a second step that validates the overall existence of the name.

[Matthew Ballard]

But I don't feel strongly so take it or leave it. And thanks!

[Damiano Testa]

So, you are suggesting to not even check if Mathlib... files exist?

[Matthew Ballard]

Yes

[Damiano Testa]

I think that this should be easy and at least you get immediate feedback if there is an issue with the command.

[Damiano Testa]

Though maybe you are right.

[Matthew Ballard]

Please just treat as a mild thought

[Damiano Testa]

Ok, I'll PR a first "fix" that just discriminates on whether the file is imported or not.

[Damiano Testa]

When I get around to writing the linter, the logic for the Mathlib.XXX.lean files may be added to the command (or not) and will improve it, if possible.

[Damiano Testa]

#15839 changes to a minimal implementation: check whether or not the given name is an imported module, with no check of whether the module could be imported, just that it isn't imported.

[Damiano Testa]

#16002 adds the eventual check of existence of imports and declarations.