leanOption in lakefile doesn't work

[timechess]

I want to set the option autoImplicit to false in a project on my self host server. My mathlib-demo/lakefile.lean is as follows:

import Lake
open Lake DSL

package "MathlibLatest" where
  -- add package configuration options here
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`autoImplicit, false⟩,
    ⟨`relaxedAutoImplicit, false⟩]

@[default_target]
lean_lib «MathlibLatest» where
  -- add library configuration options here

require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.10.0"

In VSCode the setting works quite well. For example, the following code will fail since n is not defined:

example (p : ℕ → Prop) : p n := sorry

However, in web editor, it will compile since the option is default to be true.

I think the web editor should allow us to set the options ourselves. And I think autoImplicit should not be defaultly true. I don't know why the developers choose to do this.

[joneugster]

Thanks for the report! I've isolated the issue and might have a fix ready later.

(The file URI here of the opened file needs to be inside the current project folder or lean --server does not apply the options provided.)

[joneugster]

And I think autoImplicit should not be default to true. I don't know why the developers choose to do this.

This is mostly irrelevant here, all I could do in this repo is to set autoImplicit false in the default project mathlib-demo.

For what it's worth my understanding is that auto-implicits are a useful feature for experienced Lean users but they are an absolute tripping hazard for new users...

[timechess]

For what it's worth my understanding is that auto-implicits are a useful feature for experienced Lean users but they are an absolute tripping hazard for new users...

Thanks for the reply!

What I am complaining here is all because we are trying to use web editor for teaching, and autoImplicit will cause confusion for freshmen. As I know mathematics_in_lean also set this option to be false.

Anyway, it has nothing else to do with this bug. Looking forward to the fix.

[joneugster]

Possible fix:

• [x] hhu-adam/lean4monaco#3

I'll try to get some opinion (tomorrow) if there's a better way before merging.

[joneugster]

I've cycled back to this and implemented what I could: The leanOptions should be used in the development setup (i.e. using npm start). The requirement is that there exists a file Projects/[project]/[project].lean, for example Projects/MathlibDemo/MathlibDemo.lean.

However, it does not work in the production setup in the bubblewrap container due to

• [ ] leanprover/lean4#7814