attr := simp

Stream: mathlib4

[Johan Commelin]

@Floris van Doorn We have

attribute [to_additive (attr := simp)]
  toDual_smul ofDual_smul toDual_smul' ofDual_smul'
  toLex_smul ofLex_smul toLex_smul' ofLex_smul'

which gets the following error

The source declaration has attribute simp.
This attribute is not translated to the declarations generated by to_additive. Use something like
`@[to_additive (attr := simp)]` instead.

[Johan Commelin]

https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Algebra/Group/OrderSynonym.lean#L300L302

[Chris Hughes]

You have to remove simp from the original declaration.

[Chris Hughes]

Not the most readable style

[Johan Commelin]

How can we compile mathlib in such a way that it reports all these messages on stdout?

[Floris van Doorn]

I am currently working on changing these warnings into linting errors, and fixing them all.
I'm adding some new features of to_additive so that you can easily additivize an already additive declaration (which is what is happening here). Please don't touch them, I'll fix it.
I'll improve the error message at the same time.

[Floris van Doorn]

What I'm doing is also going to be a relatively big change throughout the library, almost certainly conflicting with !4#1816, so I prefer if we merge !4#1816 before I start changing many files. @Johan Commelin are you currently working on that PR?

[Gabriel Ebner]

Johan Commelin said:

How can we compile mathlib in such a way that it reports all these messages on stdout?

It's lake build -v. But that also shows the full Lean command-line. @Mario Carneiro You were the one who decided to hide stderr/stdout by default in Lake. At the time we had lots of noise because of the unused variable warnings. Are there other reasons as well? Should we show the output again?

[Mario Carneiro]

I wanted to hide the lean command-line, not stderr/stdout

[Mario Carneiro]

I think stdout should just be printed so that we can see noisy files

[Mario Carneiro]

stderr too, although it would be nice if lake could interpret the output to control when and how it is presented

[Mario Carneiro]

I think cargo does something like rustc --json to do this kind of thing

[Floris van Doorn]

In !4#1819 I change the log info messages to linter errors, and fixed all the current linter errors.

[Floris van Doorn]

It would be nice if compilation of files continues after a linter error (both in CI and locally).

[Mario Carneiro]

oh yes that is a major peeve for me

[Mario Carneiro]

especially imports in interactive mode should not be blocked by warnings

[Gabriel Ebner]

Filed as lean4#2061.