Correct way to add package

Stream: general

[Ioannis Konstantoulas]

Say I have created a non-math project with lake new project. Then I want to add Std as a dependency to project. What is the correct way to do it? import Std does not automatically install Std in the project directory, so I am assuming either

1. I have to invoke a lake command, or

2. to manually create a lake_packages folder, clone Std in there, and somehow pin the downloaded version to the project?

Of course, I would hope for (1).

[Rémy Degenne]

You need to edit the lakefile.lean file of your project to add

require std from git
  "https://github.com/leanprover/std4"

as explained here: https://github.com/leanprover/lake#adding-dependencies

[Damiano Testa]

Mathlib has several lines like

require std from git "https://github.com/leanprover/std4" @ "main"

in its lakefile.lean. Does adding the above works?

[Rémy Degenne]

I don't know if the @ "main" is required, but if mathlib uses it you probably should as well?

[Damiano Testa]

I think that someone recently said that the default branch with git is master and lake does weird things if main is the "main" branch, like in Std. But I am not really sure...

[Damiano Testa]

Here is the link to the comment: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Updating.20using.20lake.20again/near/393881597

[Ioannis Konstantoulas]

The above fails with

`/home/admin/.elan/toolchains/leanprover--lean4---nightly/bin/lake print-paths Init` failed:

stderr:
error: missing manifest; use `lake update` to generate one
Invalid Lake configuration.  Please restart the server after fixing the Lake configuration file.

Performing lake update gave me the warning:

warning: mwe_bare: package 'std' was required as 'std4'

I wonder what happens if Std is updated in github; do I keep getting the new versions?

[Rémy Degenne]

It looks like the correct name is std, not std4 as I incorrectly wrote in the code above (which I just edited to fix that)

[Rémy Degenne]

You don't get new versions automatically. To update your dependencies you need to run lake update.

[Rémy Degenne]

But be warned that if you run lake update and the lean version used by std got ahead of the lean version you have in your lean-toolchain file, it will break everything

[Mario Carneiro]

I recommend you always use the @ branch part in a require. The current lake behavior is subtly wrong and you don't want to have to think about that

[Kevin Buzzard]

This makes the updating process much harder though because then my students have to manually edit the lake file yet again to update the dependency

[Mario Carneiro]

what do you mean?

[Ioannis Konstantoulas]

Rémy Degenne said:

But be warned that if you run lake update and the lean version used by std got ahead of the lean version you have in your lean-toolchain file, it will break everything

Can we roll back updates?

[Mario Carneiro]

git...

[Kevin Buzzard]

If my students have a specific commit mentioned in a config file then they have to manually update the commit. If they just have "master" then they don't

[Rémy Degenne]

I put all my projects on github and if I manage to break really everything, I just delete the folder and clone again

[Mario Carneiro]

the only permanent thing that lake update changes is lake-manifest.json. If you restore that and run lake build again you should be back to square one

[Mario Carneiro]

Kevin Buzzard said:

If my students have a specific commit mentioned in a config file then they have to manually update the commit. If they just have "master" then they don't

I don't mean you should put a specific commit there, but you should put a branch name

[Mario Carneiro]

don't just leave it default

[Mario Carneiro]

because the default is master which does not match what github thinks the default is