module (?)

Stream: new members

[George McNinch]

Hi--
Returning after a month or so, I'm having an issue maybe related to module?

I have a project my-project with lean-toolchain given by

leanprover/lean4:v4.26.0-rc2

If I copy my-project/.lake/packages/mathlib/Mathlib/Algebra/Polynomial/Module/Basic.lean
to the source-file part of my project directory and try to open it in VSCode
I see an error

`module` keyword is experimental and not enabled here

in the infoview. (And basically can't interact with the file via Lean).

On the other hand, if I just visit
my-project/.lake/packages/mathlib/Mathlib/Algebra/Polynomial/Module/Basic.lean
in VSCode I don't get any errors.

So presumably I need a better configuration somewhere (maybe something in lakefile.toml?)

Well, perhaps you are going to tell me that copying the file is a silly thing to do. But it appears that any file ~/my-project/my-project/foo.lean which begins with module throws this error for me.

[Eric Paul]

You have to set the option experimental.module to be true in your lakefile.toml (the reference talks about this here).

[George McNinch]

Perfect; thank you!