New syntax for weak options

Stream: mathlib4

[Damiano Testa]

I am trying to use the new syntax for setting options in the lakefile, but there is something that I do not understand: what is wrong with this?

I set to false the default value of the Mathlib.Linter.linter.hashCommand option. Then, in the lakefile:

package mathlib where
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`autoImplicit, false⟩,
    ⟨`relaxedAutoImplicit, false⟩,

    ⟨`weak.Mathlib.Linter.linter.hashCommand, true⟩
  ]

However, the test file for the hashCommandLinter now fails, since the linter never fires.

[Notification Bot]

A message was moved here from #mathlib4 > Improper firing of linter.hashcommand by Damiano Testa.

[Eric Wieser]

The test files aren't affected by these options, I believe

[Damiano Testa]

I tried also in a Mathlib file importing the linter, but it still does not work...

[Damiano Testa]

And another thing that is suspicious about my setup is this

$ lake build -Dweak.linter.hashCommand
error: unknown short option '-D'

[Damiano Testa]

(I have the updated to the current master before all these attempts, in case you are wondering.)

[Sebastian Ullrich]

lake build does not take Lean options, that is correct. I assume the name of the option is linter.hashCommand and not Mathlib.Linter.linter.hashCommand?

[Damiano Testa]

I tried with both linter.hashCommand (the one that set_option accepts) and Mathlib.Linter.linter.hashCommand (the actual fully qualified name of the option). I was not able to get either to work.

[Eric Wieser]

I think something changed around option qualified names recently; I was caught by this in a lean bump

[Eric Wieser]

It is quite confusing how register_option linter.hashCommand creates docs#Mathlib.Linter.linter.hashCommand (inside the active namespace), but the way to use it is set_option linter.hashCommand (without the namespacing)

[Eric Wieser]

register_option _root_.foo is even more bizarre, which creates a foo declaration, but (I think) registers an option called _root_.foo

[Damiano Testa]

In case you are wondering, this is my attempt: #15609.

[Damiano Testa]

Oh, in CI the linter works, but locally it does not.

[Sebastian Ullrich]

Oh. weak may not work in the server yet. Try setting the option without weak in serverArgs, which I believe ignores unknown options

[Damiano Testa]

I realize that I do not understand much, but trying

package mathlib where
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`autoImplicit, false⟩,
    ⟨`relaxedAutoImplicit, false⟩,

    ⟨`Mathlib.Linter.linter.hashCommand, true⟩,
    ⟨`linter.hashCommand, true⟩
  ]

does not actually work: as soon as I try to build a file, lean complains that the hashCommands do not exist. I tried both of them together and also each one of them separately, but nothing worked.

[Damiano Testa]

I could also find no serverArgs, so I probably am not doing the right attempt, though.

[Sebastian Ullrich]

It's moreServerOptions. @Mac Malone I think the documentation is wrong here, moreServerOptions is not passed to lean --server.

[Damiano Testa]

This works!!!

[Damiano Testa]

Using

package mathlib where
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`autoImplicit, false⟩,
    ⟨`relaxedAutoImplicit, false⟩
  ]
  -- These are additional settings which do not affect the lake hash,
  -- so they can be enabled in CI and disabled locally or vice versa.
  -- Warning: Do not put any options here that actually change the olean files,
  -- or inconsistent behavior may result
  -- weakLeanArgs := #[]
  moreServerOptions := #[
    ⟨`linter.hashCommand, true⟩
  ]

with the linter default value set to false, the test file still gets flagged by the linter!

[Damiano Testa]

And just to be completely explicity, it is the name that gets used by set_option the one that is relevant here. In the case above, it is linter.hashCommand, not the fully qualified name of the option (as in, just putting the fully qualified name does not make the linter active).

[Damiano Testa]

If an option is set in moreServerOptions but not in leanOptions, then the option is not active in CI: a file that is noisy locally passes CI in #15609.