Different defaults for a Lean.Option

Stream: mathlib4

[Damiano Testa]

Short version.
How can I have a different set_option default between local builds and CI? I just defined a new Lean.Option in Mathlib and would like it to be quiet locally and chatty in CI.

Longer version.
I am writing a linter for making sure that #-commands are not allowed in Mathlib files.

Currently, setting it to true logs a warning when a #-command is used. However, I would like the default behaviour to be to do nothing and only turning it on for CI. I tried modifying the lakefile.lean as follows:

  weakLeanArgs :=
    if get_config? CI |>.isSome then
      #["-DwarningAsError=true", "-Dlinter.hashCommand=true"] -- added here and below, to test locally
    else
      #["-Dlinter.hashCommand=true"]

However, when I run lake build Mathlib.mwe (Mathlib/mwe.lean is my current test file that imports the file with the linter and has an eval command) I get the error:

$ lake build Mathlib.mwe
[303/304] Building Mathlib.mwe
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/packages/importGraph/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=./.lake/build/lib /home/damiano/.elan/toolchains/leanprover--lean4---v4.6.0-rc1/bin/lean -Dlinter.hashCommand=true -Dpp.unicode.fun=true -Dpp.proofs.withType=false -DautoImplicit=false -DrelaxedAutoImplicit=false ./././Mathlib/mwe.lean -R ././. -o ./.lake/build/lib/Mathlib/mwe.olean -i ./.lake/build/lib/Mathlib/mwe.ilean -c ./.lake/build/ir/Mathlib/mwe.c
error: stderr:
invalid -D parameter, unknown configuration option 'linter.hashCommand'
error: external command `/home/damiano/.elan/toolchains/leanprover--lean4---v4.6.0-rc1/bin/lean` exited with code 1

Am I doing something wrong? It seems like lean does not know about linter.hashCommand, which is fair enough, since I just defined it. But I do not know how to make lean aware of its existence...

Ref: #11019

[Jannis Limperg]

This does not currently seem to be possible. See #lean4 > register_option or EnvExtension? and lean4#3403.

[Damiano Testa]

:man_facepalming: you are right: I knew of both those discussions, but somehow I was hoping that they would not apply to me... :smile: