flag all structure instances with a given pattern

Stream: lean4

[Matthew Ballard]

What I want to do: I want a list of all structure instances (in mathlib) for which there are declared fields of the form

add :=  (. + .)

Here add is an example. Generally, I want to know if the user has explicitly filled a field with what is effectively a call toinferInstance. What are people's thoughts on the best way to do this?

[Mario Carneiro]

a linter sounds like the easiest way to do this

[Mario Carneiro]

you won't get a list exactly but you can run it in CI and get a bunch of warnings

[Matthew Ballard]

I am guessing we will want a linter for this anyway. The context being the following: such a pattern, most of the time, creates a expanded term for the structure instance which is less efficient for unification than just deleting the line and for no benefit.

[Eric Wieser]

Note that in Lean3 the opposite was often true; writing add := (+) would ensure that you could unfold one step and get to the has_add instance

[Eric Wieser]

I've had timeouts (in Lean 3) that were solved by adding lines exactly of the form you mention above.

[Matthew Ballard]

And we defaulted to Lean 3 muscle memory for the port.

[Matthew Ballard]

What is the closest thing we have to this behavior (figuring out if we are using inferInstance or something close to it) at the moment?

[Mario Carneiro]

I was thinking of something pretty syntactic: look for a structure instance syntax, and if the field is foo := e then both foo and e will have Exprs in the info tree, see if e is an application of foo (modulo some lambdas)

[Matthew Ballard]

Are we talking Lean.Linter since you mention the info tree? Are those in runLinter?

[Matthew Ballard]

What is the current infrastructure to run a docs#Lean.Elab.Command.Linter like the std linters inrunLinter? I want to run over a whole library and report back the results in a single place.

[Mario Carneiro]

there is no such thing currently

[Mario Carneiro]

you can run a linter on a specific Syntax, but in order to get that syntax you would have to elaborate the file, at which point you are already running the linter

[Mario Carneiro]

and moreover that only works for one file; if you wanted the results from multiple files you would need multiple processes because lean doesn't handle multiple files in one process right now

[Mario Carneiro]

so you could do it, but it would involve compiling the whole project

[Mario Carneiro]

and then a bunch of IPC via json or something to get the results in one place

[Scott Morrison]

@Matthew Ballard, I have some infrastructure for running something at every declaration in mathlib. Look at https://github.com/semorrison/lean-training-data, particularly tactic-benchmark.

[Scott Morrison]

If you give me exactly what you want to run at each declaration I can hook it up to that on Monday.