diff --git a/.gitignore b/.gitignore index 9cf8557aec..84244fad11 100644 --- a/.gitignore +++ b/.gitignore @@ -5,8 +5,3 @@ /lakefile.olean # After v4.3.0-rc2 lake stores its files here: /.lake/ -# Note: because std has no dependencies, the lake-manifest contains no information -# that is not regenerated automatically by lake, so this avoids conflicts when -# lake decides to upgrade its manifest version. -# We may revisit this if lake decides to store more useful information in the manifest. -lake-manifest.json diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000000..00280abb6f --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,50 @@ +{"version": 7, + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/xubaiw/CMark.lean", + "type": "git", + "subDir": null, + "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77", + "name": "CMark", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "rev": "280d75fdfe7be8eb337be7f1bf8479b4aac09f71", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/mhuisi/lean4-cli", + "type": "git", + "subDir": null, + "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "nightly", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/hargonix/LeanInk", + "type": "git", + "subDir": null, + "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1", + "name": "leanInk", + "manifestFile": "lake-manifest.json", + "inputRev": "doc-gen", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/doc-gen4", + "type": "git", + "subDir": null, + "rev": "b7fad51b87a5f8fb3a238dc820ec40ebfa2a636e", + "name": "«doc-gen4»", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean"}], + "name": "std", + "lakeDir": ".lake"}