What does this warning mean?

Stream: new members

[Ching-Tsun Chou]

What does the following warning mean?

'simp [h_k, Nat.segment', Nat.count_succ, -mem_range]' is a flexible tactic modifying '⊢'…
Note: This linter can be disabled with set_option linter.flexible false

[Yaël Dillies]

This means that you used simp on the goal before using a tactic like rw or exact

[Kevin Buzzard]

You can squeeze the simp with simp? if you really have to use it in a non-terminal way (ie not closing a goal)

[Kenny Lau]

should we have better docstring here?

[Ching-Tsun Chou]

What's wrong with using simp before rw or exact?

Anyway, following Kevin's suggestion, I used simp? to produce a simp only that removed the warning:
https://github.com/ctchou/cslib/commit/61661be3ddc4273232017fa27fdd2012d350582a
As you can see, it seems that not every offending simp is before rw or exact.

[Kevin Buzzard]

The warning means that you used a flexible tactic (e.g. simp) before a rigid tactic (e.g. lots of tactics, including rw and exact). The reason it's there is for maintainability issues -- people sometimes add or remove lemmas from the simp set in mathlib and proofs with a simp in the middle that break because of this are a pain to fix (because it's hard to tell what the simp call used to be doing without getting a second version of the repo up and running with the older version of mathlib when it worked).

[Ching-Tsun Chou]

But this checking doesn't seem to be turned on by default in a project using mathlib. In my own project using mathlib, I had never seen this warning. Now I'm working on something in cslib and I see its lakefile.toml contains:

[leanOptions]
weak.linter.mathlibStandardSet = true
weak.linter.flexible = true

Shouldn't this checking be turned on by default, if it is a good idea?

[Ruben Van de Velde]

I understand we're working on it, at least for mathlib

[Snir Broshi]

https://github.com/leanprover-community/mathlib4/pull/28962
https://github.com/leanprover-community/mathlib4/pull/30092