Skip to content
This repository has been archived by the owner on Oct 25, 2023. It is now read-only.

lean_packages/manifest.jsonlake-manifest.json #111

Closed
arthurpaulino opened this issue Aug 5, 2022 · 14 comments
Closed

lean_packages/manifest.jsonlake-manifest.json #111

arthurpaulino opened this issue Aug 5, 2022 · 14 comments
Labels
chore Maintenance tasks or refactors
Milestone

Comments

@arthurpaulino
Copy link
Contributor

Dependency version pinning usually happens at the root project directory for many languages.

It also clears the .gitignore and repo structure because there wouldn't be the need to keep a directory with just a json file.

@tydeu
Copy link
Member

tydeu commented Aug 5, 2022

@gebner, @Kha what do you think?

tydeu added a commit that referenced this issue Aug 5, 2022
@Kha
Copy link
Member

Kha commented Aug 5, 2022

It was my very first thought when I saw the current file path to be honest, but I didn't want to start a discussion if it's just me (and also I'm not exactly a regular Lake user). But if we're renaming anyway, I really think we should just name it lakefile.lock like the cool kids, which looks quite nice in directory listings. Somehow my first thought when hearing "manifest" is "Java".

@gebner
Copy link
Member

gebner commented Aug 6, 2022

I'd also prefer lakefile.lock. But please let's not make this configurable. I'm willing to put up with any convention as long as it is consistent.

@tydeu
Copy link
Member

tydeu commented Aug 7, 2022

But please let's not make this configurable. I'm willing to put up with any convention as long as it is consistent.

I should note that literally everything else about the package layout is configurable, so having this be the one thing that wasn't was honestly more inconsistent. I doubt it being configurable matters. I imagine virtually everyone will stick with the defaults unless there is some real issue preventing them from doing so.

@tydeu
Copy link
Member

tydeu commented Aug 7, 2022

I really think we should just name it lakefile.lock like the cool kids, which looks quite nice in directory listings.

Here is my two cents on this: I absolutely hate this naming convention.

For one, it is not a real lock file. Before this become a common convention for package managers, a .lock file was a mutex (i.e., an actual lock) to prevent simultaneous edits by a program to a directory (e.g., Git's .git/index.lock). Instead, the file is really a manifest. I am especially disappointed that Cargo of all things did not use this term, since one definition of a manifest is a "certified list of a ship's cargo", fitting perfectly with the theme.

Second, it does not have the proper file extension (e.g., json) indicating its data format, which is very bad (e.g., for opening the file with a proper editor, for open file dialogs for things that care about file types,, and for syntax highlighting), Furthermore, different package managers use different data formats (e.g., TOML for Rust, JSON for NPM/Yarn), so there isn't even a standard data format of a .lock file to associate the extension with.

@arthurpaulino
Copy link
Contributor Author

I, on the other hand, don't care much about the name, really. But I do believe that placing a file in a folder that will hold a single file on every git repository is not the best default option

@tydeu
Copy link
Member

tydeu commented Aug 8, 2022

@arthurpaulino Yeah, I think your suggested change is reasonable. I am otherwise occupied for the next 2 weeks, but afterwards I plan to do a v4 maintenance release of Lake that should include this change.

@Kha
Copy link
Member

Kha commented Aug 8, 2022

I am especially disappointed that Cargo of all things did not use this term

Ah, but it does - Cargo.toml(!) is described as the manifest file in the documentation. So while manifest seems to be a pretty muddled term, I really can't think of a clearer term than lockfile in the context of a package manager. As you said, it's become a common convention.

Second, it does not have the proper file extension (e.g., json) indicating its data format

I'm pretty sure that's exactly as intended to signify that the file is generated and not meant for human consumption.

@arthurpaulino
Copy link
Contributor Author

Regarding the file name, here's an alternative idea: use YAML and call it lake_dependencies.yml. And then have a comment at the very top saying

This file is automatically generated and managed by Lake

@Kha
Copy link
Member

Kha commented Aug 8, 2022

Please don't use YAML for generated data. Actually any kind of data, but I can accept other opinions there.

@gebner
Copy link
Member

gebner commented Aug 8, 2022

A bit off-topic, but I think YAML is even worse for user-provided data than for generated data. At least the generator won't fall into the true/YES/yeah trap. (For the uninitiated, all three are valid YAML syntax. But the first two parse to the same boolean value, while the third is of course a string.)

(This commonly appears when listing countries. [NL, US] is a list of country codes and parses as a list of strings so everything looks great. But then you add Norway to the list...)

@RaitoBezarius
Copy link

If I can also add my 2 cents (and a "feature request"), it would be great if the chosen target file can be easily readable by Nix, e.g. commonly used file formats and enough data to download everything (hashes, etc.) without external assistance.

@tydeu
Copy link
Member

tydeu commented Aug 8, 2022

@RaitoBezarius The current manifest format should already fit this (it uses JSON and has hashes etc.)

@tydeu
Copy link
Member

tydeu commented Aug 8, 2022

Ah, but it does - Cargo.toml(!) is described as the manifest file in the documentation. So while manifest seems to be a pretty muddled term,

But it is not a manifest file? To keep with the analogy of cargo, it is an order, not an invoice. That is, the user is ordering what packages they want downloaded, it is not a "certified list" of which ones were downloaded (that is what the .lock file is). Thus,, I do not feel we should adopt their misuse of the English language.

As you said, it's become a common convention.

In my view, bad conventions should be broken. Especially if the convention is jargon and not helpful to new user's understanding.

I'm pretty sure that's exactly as intended to signify that the file is generated and not meant for human consumption.

But Lake's manifest is. As mentioned in #70, manually altering the manifest may be necessary to fix conflicts.

@tydeu tydeu closed this as completed in b7d5085 Aug 8, 2022
tydeu added a commit that referenced this issue Aug 8, 2022
@tydeu tydeu added the chore Maintenance tasks or refactors label Aug 8, 2022
@tydeu tydeu added this to the v4.1.0 milestone Aug 16, 2022
tydeu added a commit that referenced this issue Oct 1, 2022
tydeu added a commit that referenced this issue Nov 11, 2022
Kha pushed a commit to Kha/lean4 that referenced this issue Jul 17, 2023
Kha pushed a commit to Kha/lean4 that referenced this issue Jul 17, 2023
Kha pushed a commit to Kha/lean4 that referenced this issue Jul 17, 2023
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
chore Maintenance tasks or refactors
Projects
None yet
Development

No branches or pull requests

5 participants