Some options cannot be set at the command line

[fgdorais]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Options that are not defined in Lean itself (or in a plugin?) cannot be set using -D at the command line.

Context

In the discussion of std4#625, I proposed using an option to control how the lemma command works instead of an ad-hoc switch mechanism. This would allow users to turn on the lemma command using set_option but it would also allow Mathlib to enable lemma globally by setting it in the lakefile. Using set_option works fine but, since it is declared in Std and not in Lean, the option cannot be set globally from the lakefile.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[joneugster]

Being able to set options globally for a package would be desired for a few other projects, too:

• Aesop has various check options that enable internal consistency checks. These are off by default for performance reasons, but it would be nice to be able to build Mathlib with these checks just by editing the lakefile.
• Aesop has a benchmarking option that would be nice to enable for the entirety of Mathlib.
• Lean4Game wants to show help for the creator in Vscode but silence these logInfo when building. It now abuses the built-in -Dtrace.debug instead of using it's own option.
• I18n would want to set the language of a project in order to provide translations of strings.

Here is an example lakefile, how I would hope one could set it's own options:

Example lakefile

import Lake
open Lake DSL

-- Sample dependency. Contains: 
--   register_option lean4game.verbose : Bool := {
--     defValue := false
--     descr := "display more info messages to help developing the game."
--   }
require GameServer from git "https://github.com/leanprover-community/lean4game.git" @ "v4.5.0" / "server"

-- set the option for the entire project:
package «OptionMWE» where
  moreLeanArgs := #[
    "-Dtactic.hygienic=false",
    "-Dlean4game.verbose=false"]
  moreServerOptions := #[
    ⟨`tactic.hygienic, false⟩,
    ⟨`lean4game.verbose, true⟩]

lean_lib «OptionMWE» where