Initiating someone else's lean 3 project

Stream: general

[Quinn Culver]

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]

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]

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

[Quinn Culver]

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

[Quinn Culver]

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

[Floris van Doorn]

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]

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]

Thank you!

[Quinn Culver]

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]

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]

Okay thanks.

[Quinn Culver]

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

[Kevin Buzzard]

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