leanproject build

Stream: new members

[Dima Pasechnik]

What are advantages of organising lean3 code into projects? I understand that leanproject build might come handy (certainly for scripring etc) - but does it provide e.g. speed advantages over the VSCode setup?

[Eric Wieser]

What do you mean by "the vscode setup"?

[Eric Wieser]

Are you asking about leanpkg vs leanproject?

[Dima Pasechnik]

Eric Wieser said:

What do you mean by "the vscode setup"?

I mean, loading individual Lean files without creating a project. (That's what my students like to do, and I'm not sure whether it's a good idea).

[Kevin Buzzard]

You can't import anything if you just open a file, and for mathematicians this is a catastrophe

[Dima Pasechnik]

Kevin Buzzard said:

You can't import anything if you just open a file, and for mathematicians this is a catastrophe

I don't know what they do, but they manage somehow...

[Dima Pasechnik]

them: I'd like to work on, but it's broken (git repo with collection of old lean files, no project or anything)
me: OK (frantically restructures the code, creating a project, etc), sends updated repo to the student
them: OK, thanks, but I managed without a project (sends a link to a repo with a single Lean file)
me: ....

[Dima Pasechnik]

maybe they just don't check in various config files created on the fly by the VSCode plugin?

[Eric Rodriguez]

a thing that can be done is if you have a local clone of mathlib, and make a file whilst that is open in VSCode, then it will run

[Eric Wieser]

But if you do that, there's no guarantee it will work next time when mathlib is newer. The project file ensures you record which version you were actually using

[Kevin Buzzard]

Aah I see, you can open some random version of mathlib and then just make a new file within it.

[Dima Pasechnik]

Kevin Buzzard said:

Aah I see, you can open some random version of mathlib and then just make a new file within it.

yes, IDEs are full of surprises. For teaching purposes, I'd much prefer being able to run leanproject build from terminal and see how it does.