[Merged by Bors] - fix(*): fix many indentation mistakes

[jcommelin]

---

[sgouezel]

Suggested change

	-- We construct an surjective linear map `(w → R) →ₗ[R] (ι → R)`,
	-- We construct a surjective linear map `(w → R) →ₗ[R] (ι → R)`,

[jcommelin]

This would destroy the "this PR only changes whitespace" property of this PR. Do we care?

[Vierkantor]

I would prefer to keep the changes whitespace-only, as there is enough to review in the linter itself :)

[Vierkantor]

Do I understand correctly that the indentation changes included in this PR are exactly those flagged by the linter, and there are no false positives you noticed? In that case, I'm happy to approve the overall design of the linter for now, and see how it responds to new code.

I suspect that doing the linter line-by-line is going to quickly make it hard to adapt if we need to keep tweaking it (already I don't really understand the order in which the different tokens in a line are handled): a better architecture would be to parse the file into tokens and advance the state token-by-token. That should make it easier to deal with situations like:

def blah := foo (some_complicated - expression) begin
  correctly_indented_tac,
  { subtac },
  { another_subtac }
end

[Vierkantor]

Do you have an example of a "normal" piece of Lean where the second if would apply that is not handled by the first if?

Suggested change

	if line.find("begin") > 0 and in_prf == 0:
	# complicate proof block syntax
	check_rest_of_block = False
	if lstr.find("begin") > 0:
	# complicate proof block syntax
	check_rest_of_block = False
	# Don't check complicated proof block syntax:
	# - a `begin` block in the middle of term mode
	if line.find("begin") > 0 and in_prf == 0:
	check_rest_of_block = False
	# - another case where `begin` appears somewhere else in the line
	if lstr.find("begin") > 0:
	check_rest_of_block = False

[jcommelin]

I think the first if can just be removed. I don't want to check the indentation of subproofs of the form

have foo : bla := begin
  stuff
end,

[jcommelin]

Oops, nope. I clarified how they both do useful things in the other PR.

[Vierkantor]

I'm concerned checks like if "keyword" in line are too likely to get false positives, e.g. the check for end will match all lines containing linear_independent, and cause the in_prf counter to turn negative. (It's good that you explicitly say in_prf > 0 above rather than in_prf, or we'd get some weird errors!)

More robust would be to use re.match("\bkeyword\b", line) (where \b is regex syntax for "word boundary").

[jcommelin]

Fixed in the other PR

[Vierkantor]

What is the motivation for checking [/] indent level before the "reset" logic and {/} indent level afterwards?

[jcommelin]

[/] is checking the nesting level, and if we're nested inside such a special block we don't want to do anything.
Moving these indent_lvl lines for {/} would break the indent checking code in the lines above.

[Vierkantor]

I would prefer to keep the changes whitespace-only, as there is enough to review in the linter itself :)

[PatrickMassot]

bors merge

[sgouezel]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests