feat: add lake-manifest.json, update .gitignore

leanprover-community / quote4

Intuitive, type-safe expression quotations for Lean 4.

Apache License 2.0

73 stars 11 forks source link

feat: add lake-manifest.json, update .gitignore #42

Closed Shreyas4991 closed 4 months ago

Shreyas4991 commented 4 months ago

As the title says, I have added lake-manifest.json by running lake update. I have also updated .gitignore to not ignore the manifest. If required, the .gitignore change can be undone.

For relevant discussion see the linked zulip thread

semorrison commented 4 months ago

We've previously avoided having "empty" lake-manifest, because they are just a useless file to gitignore. However the absence causes a warning downstream, and this confusion to users is a more important consideration.