linting for unclosed sections?

Stream: mathlib4

[Kim Morrison]

Does anyone have an idea about linting for unclosed sections? They are quite common in Mathlib, and they are tedious to encounter when doing minimizations.

[Damiano Testa]

Oh, that's a challenge!

[Damiano Testa]

Should they be closed at the end of file?

[Johan Commelin]

They should be closed before the scope that contains them is closed. This containing scope could be a file/namespace/section.

[Damiano Testa]

Ok, I meant to say "they should be closed at the latest point where it is legal to do so"?

[Damiano Testa]

An alternative being "the earliest place where the file still builds".

[Johan Commelin]

Well, I think you are going one step beyond, and thinking already about a refactor tool.
As a first step it would of course already be useful to have the warning.

[Damiano Testa]

Ok, I'll think about this. I've been indeed also thinking of producing the refactor tool with every linter, but not actively writing one for every linter.

[Damiano Testa]

I'll have to see how/if sections leave traces in Scope (or elsewhere).

[Damiano Testa]

"Anonymous" sections (as in section) leave very little trace, while "named" sections (as in section Easy_lemmas) do modify the "header". What do you think of linting against anonymous sections and then catching missing end section?

[Johan Commelin]

How many anonymous sections are there in mathlib?
Just to be sure: you are proposing that they all become named, right?

[Damiano Testa]

I have not checked how many unnamed sections there are and yes, the linter would ask to name them.

[Damiano Testa]

Technically, this is not needed, as I can simply begin linting for the named ones and then think about the unnamed ones.

[Damiano Testa]

However, unnamed sections are a little weird anyway...

[Kim Morrison]

Please let's not do anything disruptive like forbidding anonymous sections!

[Kim Morrison]

I just want to warn on unclosed sections (named or not) at EOF.

[Kim Morrison]

The problem is that when minimising, we copy one file into another and unclosed sections need to be repaired.

[Damiano Testa]

Ok, grepping suggests that there are close to 2k unnamed sections. I will think of how to handle them without flagging them.

[Michael Rothgang]

You can probably write a simple-minded text-based linter for this, right? As in, ignore multi-line comments and keep a stack of all open sections and namespace, which you update as you encounter them. (No time until end of this week, but I could also try writing the latter.)

[Damiano Testa]

Yes, I am trying exactly this at the moment.

[Damiano Testa]

Oh, actually it seems that the only way to have open namespaces/sections is if they accumulate at the end of a file. So the only thing to do is check that the last command of each file closes everything!

[Eric Wieser]

Kim Morrison said:

I just want to warn on unclosed sections (named or not) at EOF.

Could this warning be built into lean core?

[Eric Wieser]

It seems like the existing section elaborator would know if there are unclosed sections (it surely did in lean 3), and so it could emit the lint warning itself rather than in a dedicated linter

[Eric Wieser]

Kim Morrison said:

The problem is that when minimising, we copy one file into another and unclosed sections need to be repaired.

An alternative solution would be to allow

section outer

section unclosed

end outer

which means you can assemble your mwe by adding section my_file around the entire file contents. This feels like something you might already want to do today to insulate variables and set_options

[Kim Morrison]

I'd prefer not to touch any core behaviour here. This would add work for me rather than save it. I know Mario has expressed a desire for the opposite convention in Batteries (leave out all unnecessary end at EOF).

[Damiano Testa]

#14352 -- let's see if it works!

[Damiano Testa]

It looks like there might be ~1k files with missing end: should I add the ending ends?

[Kim Morrison]

Ouch. I would like this, but maybe we should get some +1s before proceeding.

[Kevin Buzzard]

I thought "you don't have to end sections now" was a feature not a bug, and IIRC this was the sort of change from Lean 3 that the devs were loving. Are we saying that this is no longer considered good style in mathlib?

[Kim Morrison]

My understanding is that Mathlib has for the most part been closing sections, but that it has not been consistent.

[Kim Morrison]

I think Damiano's number says that roughly 80% of files close their sections.

[Mario Carneiro]

keep in mind that 80% of files are from lean 3 which required sections to be closed

[Mario Carneiro]

noncomputable section is not a section that should need to be closed

[Damiano Testa]

It was easy enough to add the first layer of end: 936 files.

[Kim Morrison]

Admittedly copilot usually manages to write the end statements for me when I am minimizing and this causes an error.

[Mario Carneiro]

surely copilot doesn't have enough context length to get end right?

[Kim Morrison]

It reads the error message

[Kim Morrison]

(I think???)

[Mario Carneiro]

ok we should clearly make autocomplete better there

[Damiano Testa]

(also, my script is actually closing noncomputable sections, I think.)

[Mario Carneiro]

and we could definitely have a code action at global scope to close the last section/namespace

[Damiano Testa]

(Btw, I am not particularly invested in this: I went for a quick hack to get missing ends and I do not have a strong opinion on whether I am happy or not with the change!)

[Damiano Testa]

In case anyone is curious, the linter is happy with #14352

[Kim Morrison]

@Damiano Testa how does this linter handle noncomputable section? Mario asked that that be allowed with a corresponding end, and this seems quite reasonable to me.

[Damiano Testa]

The linter treats noncomputable section like any other section and asks to close it.

[Damiano Testa]

What should it do with

section
noncomputable section
end
end

?

Are both final ends optional? Or should only an "outermost" noncomputable section be allowed to not end?

[Damiano Testa]

I adapted the linter. The behaviour now should be that the linter asks to close all dangling sections/namespaces, with the exception of the "outermost" noncomputable section, regardless of whether or not it is named.

[Damiano Testa]

I imagine that it is never the case that there is a noncomputable section nested inside a noncomputable section, but I am not sure and the linter does not check this.

[Damiano Testa]

I am trying out the "new" linter that allows dangling noncomputable section to be left open in #14378.

There are only 200 files in Mathlib/* that need an end to please the "noncomputable-admitting linter", as opposed to the ~900 files that the stricter linter flagged.

[Damiano Testa]

TIL: did you know that

section A.B

end B

end A

is valid?

[Damiano Testa]

#14378 added ends to 212 files and passed CI. No outmost open noncomputable section has been closed.

[Yaël Dillies]

I did! I think I used this behaviour exactly once so far, though :sweat_smile:

[Kim Morrison]

Damiano Testa said:

TIL: did you know that

section A.B

end B

end A

is valid?

It works the other way around as well, I think. You can probably even section a.b; section c.d.e; end a.b.c; end d.e if you are feeling antisocial!

[Mario Carneiro]

an even more amusing variant of this:

section
section Foo
end «».Foo

[Damiano Testa]

Btw, the linter is no longer going to allow this feature:

section

end section

[Damiano Testa]

(Mathlib has this twice.)

[Kevin Buzzard]

Given that this is silly and should be removed, I think it's great that we can lint for it!

[Damiano Testa]

Is the consensus that the "strict" linter that also wants to close noncomputable sections is not desired?

If this is the case, I will close that PR (#14352) and leave just the one with the "permissive" linter (#14378) and the discussion can continue about that one.

[Johan Commelin]

I for one wouldn't mind requiring noncomputable section to be closed. But I don't have a strong opinion about it.

[Damiano Testa]

The way the linter is set up, to not allow dangling noncomputable sections it suffices to remove this line (and then deal with adding ends wherever the linter tells you to).

As allowing dangling noncomputables is probably less controversial than not allowing them, I have closed the other PR anyway. I can always re-open it later, or simply remove the line, re-run the linter and the autocorrection and prepare a fresh one!

[Damiano Testa]

Are there any more thoughts on #14378?

It is a bit insidious to maintain, since splitting a file need not trigger a merge conflict, but might make the linter unhappy with merging master.

[Johan Commelin]

@Michael Rothgang @Jon Eugster could one of you maybe review this please?

[Michael Rothgang]

Sure - I'll try to review this by Wednesday. (Might happen sooner, but no promises: I'm decompressing from having my thesis submitted, so am taking things slightly slower.)

[Jon Eugster]

I'm on vacation until the 18th, sorry. I'd take a look if it still remains open by then

[David Renshaw]

How do I disable this linter? I tried putting ⟨linter.endOf, false⟩ in leanOptions` in my lakefile.lean, but that yielded

invalid -D parameter, unknown configuration option 'linter.endOf'

[Michael Rothgang]

David Renshaw said:

How do I disable this linter? I tried putting ⟨linter.endOf, false⟩ in leanOptions` in my lakefile.lean, but that yielded

invalid -D parameter, unknown configuration option 'linter.endOf'

You're in a project depending on mathlib, right? Short answer, as far as I know is "lobby the lint author to restrict the lint to mathlib".

[David Renshaw]

yes, for a project that depends on mathlib

[Michael Rothgang]

Longer answer: AFAIK, only built-in linters can be disabled in the lakefile (that's lean4#3403, feel free to upvote if you care about this). The endOf linter is defined in mathlib, hence is not built in.

[Michael Rothgang]

#14696 deactivates the linter outside of mathlib - for discussion.
That said: is simply complying by the linter onerous for you? #14378 has a shell script to automatically fix all errors.

[David Renshaw]

I ran that script and it added a bunch of spurious sorries

[David Renshaw]

in any file that had a sorry, it added its own sorry, causing an error

[David Renshaw]

This is in Compfiles, where every file has a single namespace (so unclosed namespaces pose no danger to refactoring), and I want to avoid extra clutter

[Damiano Testa]

The script was written assuming that the build would only report warnings from the linter. I can adapt it to be more robust, if that is desirable, or, if you prefer to use refactor, a better solution would be using that.

[Damiano Testa]

(The issue is that refactor is still a PR.)

[Damiano Testa]

The script below should be more robust:

eval "$(
  lake build |
  sed -z 's=\n\nend=\\n\\nend=g; s='"'"'\n=\\n&=g' |
  awk -F: '/^warning.*unclosed sections or namespaces; expected:/ {
    line=$0
    gsub(/^.*unclosed sections or namespaces; expected: /, "", line)
    printf("printf %s >> %s\n", line, $2)
  }'
)"

[David Renshaw]

Thanks. That works, though I would still prefer to be able to disable the linter.

[Damiano Testa]

I agree that it would be useful to set global options in projects: the issue about this is lean4#3403.

[Michael Rothgang]

Thinking about this again, I'm still not very happy with the name endOf: what do you think about renaming it to unclosedScope? (Yes, the word "scope" is jargon, but I find the new name less cryptic that endOf.)

[Damiano Testa]

I'm happy to change name, other options: missingEnd or openSection (even though a namespace might also be open)?

[Michael Rothgang]

Namespaces can also be open. openSectionOrNamespace feel a bit clunky for me.

[Kim Morrison]

I like missingEnd.

[Michael Rothgang]

Filed #14758 doing the rename.