Project configuration interface

Stream: lean4

[Patrick Massot]

@Marc Huisinga Now that we have the nice project creation menu, it would be nice to have a dialog showing the lake configuration options, as a series of check-boxes with sensible defaults checked (where sensible depends on whether this is a math project or not). There would be a friendly message saying: "if you don't know what those options mean then don't modify anything". Currently my workflow after creating any project is to go the Mathlib lakefile and copy-paste

def moreServerArgs := #[
  "-Dpp.unicode.fun=true", -- pretty-prints `fun a ↦ b`
  "-Dpp.proofs.withType=false"
]

-- These settings only apply during `lake build`, but not in VSCode editor.
def moreLeanArgs := moreServerArgs

-- 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
def weakLeanArgs : Array String :=
  if get_config? CI |>.isSome then
    #["-DwarningAsError=true"]
  else
    #[]

package MyProject where
  moreServerArgs := moreServerArgs

@[default_target]
lean_lib MyProject where
  moreLeanArgs := moreLeanArgs
  weakLeanArgs := weakLeanArgs

[Shreyas Srinivas]

Do they already exist in the settings page? It might be nice to have them there too

[Shreyas Srinivas]

If someone made a mistake, they could fix it.

[Mac Malone]

@Patrick Massot We could have this as the default for a lake new foo math. I would accept any PRs to that effect.

[Eric Wieser]

Have we suggested that pp.proofs.withType=false should just be the default? pp.proofs.withType=true is a really nice feature to have as an option, but its a terrible default for verbosity!

[Eric Wieser]

(and in non-mathematical usage, I can't imagine it being useful either)

[Eric Wieser]

I assume pp.unicode.fun=true is destined to forever have a software/math split, and is not a hill worth fighting on.

[Patrick Massot]

Shreyas, what do you call "the settings page"?

[Eric Wieser]

I think Shreyas is suggesting integration between the vscode workspace settings and the lakefile settings

[Eric Wieser]

But I think this is a no-go because a single workspace can have multiple top-level folders, and the settings can't be per folder

[Patrick Massot]

@Mac Malone lean4#2770 as requested.

[Shreyas Srinivas]

Mac Malone said:

Patrick Massot We could have this as the default for a lake new foo math. I would accept any PRs to that effect.

Can it be an option? Patrick's suggestion could be the default. It might look like lake new <project_name> math --<without-some-nicer-settings>

[Scott Morrison]

Shreyas Srinivas said:

Mac Malone said:

Patrick Massot We could have this as the default for a lake new foo math. I would accept any PRs to that effect.

Can it be an option? Patrick's suggestion could be the default. It might look like lake new <project_name> math --<without-some-nicer-settings>

Too much configuration. Just edit the lakefile.

[Shreyas Srinivas]

I am not asking for new configuration. The current lakefile for mathlib project doesn't add any options. The new PR adds some options which are great for some projects but get added to all math projects whether the user wants it or not.

[Scott Morrison]

You are asking for an extra -- flag. That's lots of work for something people can easily achieve with an editor.

[Shreyas Srinivas]

What I ask is a way to maintain current behaviour for those who don't want these options without extra steps.

[Shreyas Srinivas]

For now it is not a big deal for me. In fact I like the two new options that Patrick has added. So I'll drop this here.

But in general if default behaviour is being changed it seems unfair to ask users happy with current behaviour to start editing config files to get it back.

[Patrick Massot]

I think those options are extremely uncontroversial. Note that I didn't include the much more controversial autoImplicit options.

[Patrick Massot]

And I don't understand why you care about math projects.

[Shreyas Srinivas]

Patrick I am in agreement with your proposal in the PR.

[Mario Carneiro]

I just noticed this PR, and IMO this makes the math config too long and complicated to be a default. I really want simple projects to have simple lakefiles, and this complexity is tolerable for mathlib itself but way too much for a hello world project for someone who just learned about the existence of lean/mathlib in the past hour.

[Mario Carneiro]

It also needs to be documented better - the existing documentation is appropriate for people poking around the mathlib lakefile but not for newbies trying to make simple modifications e.g. to change options

[Scott Morrison]

It would be great if the warningAsError-only-in-CI setting did not require any configuration!

[Eric Wieser]

Can't that live in the CI config? Can you set lean options on the lake command line?