register_option or EnvExtension?

Stream: lean4

[Jon Eugster]

This is more of a conceptional question. I'm reasonably far writing a i18n package (somewhat inspired by this snippet by @Kyle Miller ). One missing part is how to save the input- and output-language and especially how the user sets them. I imagine roughly the following:

• user require the I18n package in their lakefile
• They set their preferred input-language and output-language once. (where?) In all files in that directory the commands t!"..." and String.translate should have access to these options in order to provide the translation.
• ideally, a user could also overwrite the output-language for a single file.

What's the best option to provide such "global" options?

I see a few options:

• register_option: as far as I can tell this requires to add set_option i18n.lang "en" in each single file. There is no option to set a custom option globally (e.g. in the lakefile), is there?
• PersistentEnvExtension: This has the limitation that the user's project needs somewhat a "root file" which is imported everywhere and which sets the language (say with a SetLanguage en command).
• The user could also provide these options with lake build -R -Klang=fr. That feels like the hackiest option...

Is there a better option I haven't thought of?

[Matthew Ballard]

I could have sworn you could globally set_option in a lakefile

[Jon Eugster]

I thought only the core ones but not custom ones. But maybe I misremember

[Matthew Ballard]

Oh maybe

[Jannis Limperg]

Could you make an issue about setting non-builtin options on the Lean command line? I recently hit this as well with two use cases:

• 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.
• Similarly, Aesop has a benchmarking option that I'd like to enable for the entirety of Mathlib.

[Jon Eugster]

That's probably a good idea if there is no issue already. In another project I just abused the option -Dtrace.debug for my own usage. I have no idea what implications that has, I just hoped that option wasn't really used in any meaningful way :sweat_smile:

[Jon Eugster]

Looks like there is at least already a relevant issue: https://github.com/leanprover/lean4/issues/3403

[Matthew Ballard]

I :+1: ’d it