Zulip Chat Archive

Stream: general

Topic: Initiating someone else's lean 3 project

Quinn Culver (Oct 16 2022 at 18:28):

Hi, I just got a lean 3 directory from someone that already has leanpkg.path & leanpkg.toml files as well as src and _target directories. Is there something I should do with that directory to make it a project? From within that directory I ran leanproject new , which did something, namely

configuring  his_project 0.1
Adding mathlib
mathlib: trying to update _target/deps/mathlib to revision lean-3.48.0

↑ those are first three lines of the output.

Floris van Doorn (Oct 16 2022 at 18:45):

I think if it already has those directories and leanpkg.toml, the leanproject new won't help you (and it seems like it updates mathlib, which might break the project).
You want to run leanproject build to build the project (it will be quick if all the oleans are already there).

Floris van Doorn (Oct 16 2022 at 18:46):

running leanproject get-mathlib-cache also doesn't hurt (before build), though it might be unnecessary if you already have a _target.

Quinn Culver (Oct 16 2022 at 18:48):

Okay thanks. So if leanproject new broke it, will leanproject build indicate as much?

Quinn Culver (Oct 16 2022 at 18:49):

And is simply re-getting (i.e. re-unzipping) the original directory the best solution?

Floris van Doorn (Oct 16 2022 at 18:51):

Probably re-unzipping is a good idea to not update mathlib.
The leanproject build will raise any compilation errors (that might be caused by updating mathlib).

Floris van Doorn (Oct 16 2022 at 18:51):

Also, if you navigate the code using VS Code, make sure to open the root folder (the one containing src/ and leanpkg.toml) as a project (e.g. code . &), not an individual lean file.

Quinn Culver (Oct 16 2022 at 18:53):

Thank you!

Quinn Culver (Oct 16 2022 at 19:30):

After re-unzipping and running leanproject build, I got the following (error?) message

6.W34.card2.DC7.DCs_sub_sdiff_dB_DC_len4'external command exited with status 137
Command '['leanpkg', 'build']' returned non-zero exit status 1.

Patrick Massot (Oct 16 2022 at 19:33):

This kind of issue in a setup that is known to be broken is extremely difficult to debug remotely. If there is no secret here then the easiest way out is probably to post a zip file of what you originally got.

Quinn Culver (Oct 16 2022 at 19:37):

Okay thanks.

Quinn Culver (Oct 16 2022 at 19:37):

I'll ask the author if that's okay.

Kevin Buzzard (Oct 16 2022 at 19:52):

You might want to tell the author that _target and leanpkg.path should not be part of a correctly formatted project.

Last updated: Aug 03 2023 at 10:10 UTC