leanblueprint with lakefile.toml

Stream: general

[Michael George]

I'm trying to set up a new blueprint for my project, but leanblueprint doesn't seem to support lakefile.toml yet. I've created a PR to solve this: https://github.com/PatrickMassot/leanblueprint/pull/23

[Utensil Song]

leanblueprint has an issue that would add duplicated entries to lakefile.lean (if the lakefile already contains entries about mathlib and doc-gen4 etc.). Skimming the code, it seems that the PR also didn't consider this scenario for TOML?

[Utensil Song]

Another question is whether it's preferred to entries to lakefile.lean(as in the PR) if "both lakefile.lean and lakefile.toml exist".

[Michael George]

Yes, I just preserved the existing behavior. It would be easy to deduplicate for TOML I think if that’s desired. Re defaulting to lakefile.lean, I chose that because it’s what lake does

[Utensil Song]

You might need to ping Patrick Massot on Zulip for reviewing the PR. Github PRs are easy to miss when one's busy.

[Patrick Massot]

Utensil Song said:

leanblueprint has an issue that would add duplicated entries to lakefile.lean (if the lakefile already contains entries about mathlib and doc-gen4 etc.). Skimming the code, it seems that the PR also didn't consider this scenario for TOML?

leanblueprint does not add an entry about mathlib of course, only doc-gen and a lib that is relevant only to blueprints, and it asks before doing it. I could try to detect the presence of those libs in the lakefile.lean but I think the risk is extremely low. And indeed using lakefile.toml is a much better solution for this kind of projects. The ability for external tools to edit the project configuration was the main motivation for supporting toml lake files.

[Patrick Massot]

And I saw the PR, I simply need to find time to review it.

[Utensil Song]

Actually I ran into the duplication issue a few days ago when setting up blueprint for someone who has already added doc-gen4, that's why I noticed it. But it was trivial to fix so I forgot it really quick.

Seeing the TOML PR makes me wonder if it would be easier to handle this, as maybe TOML library might already support an insert-or-replace-ish semantics.

Also for lakefile.lean, it also doesn't need a full parser for lakefile at all, just detect the repo URL which is most likely always there no matter how one writes the rest of the statement.

I agree that it's not a priority to fix it.