Lake

Stream: lean4

[Rudolf Meijer]

Do I understand correctly that lake new/init always fills Main.lean with "hello world?". Or is there a way to ask lake to create a "neutral" project, i.e. one with an empty Main?

[Mario Carneiro]

Yes, it always puts the hello world in. You can always just delete the content of the file if you are past the hello world stage

[Mario Carneiro]

an empty file is kind of hard to use as a starting point, because you could put anything in there, it's not even obviously lean code at that point

[James Gallicchio]

(also it's nice to know that your setup is working in the sense you can interact with the hello world definition)

[Rudolf Meijer]

Understood. Subsidiary question: the Std that I have pulled in one project's lakefile, is that also valid for other projects, or do I have to pull Std in each project?

[Mario Carneiro]

different projects are completely independent, you have to put the dependency in each project you want to use it in

[Mario Carneiro]

You can point multiple projects to the same lake-packages directory if you are worried about using too much space, although if you have different versions of dependencies in different projects then you might end up bouncing between the versions

[Rudolf Meijer]

Thx