From 0563173d7c218e4c63ab05461adf9b871cafe216 Mon Sep 17 00:00:00 2001
From: maxwell3025 <amoinus@gmail.com>
Date: Sat, 6 Dec 2025 15:50:19 -0500
Subject: [PATCH 1/7] fix: add table variant for require.git field in
 lakefile.toml schema

---
 src/lake/schemas/lakefile-toml-schema.json | 27 +++++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

diff --git a/src/lake/schemas/lakefile-toml-schema.json b/src/lake/schemas/lakefile-toml-schema.json
index 09f40a55d5f9..d272d77f4a5c 100644
--- a/src/lake/schemas/lakefile-toml-schema.json
+++ b/src/lake/schemas/lakefile-toml-schema.json
@@ -343,6 +343,31 @@
                 ]
             }
         },
+        "gitSpecification": {
+            "type": [
+                "string",
+                "object"
+            ],
+            "anyOf": [
+                {
+                    "type": "string"
+                },
+                {
+                    "type": "object",
+                    "properties": {
+                        "url": {
+                            "type": "string"
+                        },
+                        "subDir": {
+                            "type": "string"
+                        }
+                    },
+                    "required": [
+                        "url"
+                    ]
+                }
+            ]
+        },
         "dependencyConfig": {
             "type": "object",
             "properties": {
@@ -355,7 +380,7 @@
                     "description": "A dependency on the local filesystem, specified by its path."
                 },
                 "git": {
-                    "type": "string",
+                    "$ref": "#/definitions/gitSpecification",
                     "description": "A dependency in a Git repository, specified by its URL."
                 },
                 "subDir": {

From 5d2f4d39432e7f56cb6b1187c9f9e790e5383035 Mon Sep 17 00:00:00 2001
From: maxwell3025 <amoinus@gmail.com>
Date: Sat, 6 Dec 2025 22:27:35 -0500
Subject: [PATCH 2/7] test: add test for `lakefile-toml-schema.json`

---
 tests/lake/tests/lakefileSchema/clean.sh         |  1 +
 .../invalid/require_git_empty.toml               | 15 +++++++++++++++
 .../invalid/require_git_extra_fields.toml        | 15 +++++++++++++++
 .../invalid/require_git_missing_url.toml         | 15 +++++++++++++++
 tests/lake/tests/lakefileSchema/test.sh          | 16 ++++++++++++++++
 .../lake/tests/lakefileSchema/valid/default.toml | 10 ++++++++++
 .../lakefileSchema/valid/require_git_string.toml | 15 +++++++++++++++
 .../valid/require_git_url_only.toml              | 15 +++++++++++++++
 .../valid/require_git_url_subdir.toml            | 15 +++++++++++++++
 9 files changed, 117 insertions(+)
 create mode 100644 tests/lake/tests/lakefileSchema/clean.sh
 create mode 100644 tests/lake/tests/lakefileSchema/invalid/require_git_empty.toml
 create mode 100644 tests/lake/tests/lakefileSchema/invalid/require_git_extra_fields.toml
 create mode 100644 tests/lake/tests/lakefileSchema/invalid/require_git_missing_url.toml
 create mode 100755 tests/lake/tests/lakefileSchema/test.sh
 create mode 100644 tests/lake/tests/lakefileSchema/valid/default.toml
 create mode 100644 tests/lake/tests/lakefileSchema/valid/require_git_string.toml
 create mode 100644 tests/lake/tests/lakefileSchema/valid/require_git_url_only.toml
 create mode 100644 tests/lake/tests/lakefileSchema/valid/require_git_url_subdir.toml

diff --git a/tests/lake/tests/lakefileSchema/clean.sh b/tests/lake/tests/lakefileSchema/clean.sh
new file mode 100644
index 000000000000..a4953f9eb20d
--- /dev/null
+++ b/tests/lake/tests/lakefileSchema/clean.sh
@@ -0,0 +1 @@
+rm ./taplo
\ No newline at end of file
diff --git a/tests/lake/tests/lakefileSchema/invalid/require_git_empty.toml b/tests/lake/tests/lakefileSchema/invalid/require_git_empty.toml
new file mode 100644
index 000000000000..69b385308da2
--- /dev/null
+++ b/tests/lake/tests/lakefileSchema/invalid/require_git_empty.toml
@@ -0,0 +1,15 @@
+name = "foo"
+version = "0.1.0"
+defaultTargets = ["foo"]
+
+[[require]]
+name = "dependency"
+git = {}
+rev = "main"
+
+[[lean_lib]]
+name = "Foo"
+
+[[lean_exe]]
+name = "foo"
+root = "Main"
diff --git a/tests/lake/tests/lakefileSchema/invalid/require_git_extra_fields.toml b/tests/lake/tests/lakefileSchema/invalid/require_git_extra_fields.toml
new file mode 100644
index 000000000000..8e3d2730fe44
--- /dev/null
+++ b/tests/lake/tests/lakefileSchema/invalid/require_git_extra_fields.toml
@@ -0,0 +1,15 @@
+name = "foo"
+version = "0.1.0"
+defaultTargets = ["foo"]
+
+[[require]]
+name = "dependency"
+git = { url = "https://github.com/User/package", subDir = "subdirectory", extra="this should not exist" }
+rev = "main"
+
+[[lean_lib]]
+name = "Foo"
+
+[[lean_exe]]
+name = "foo"
+root = "Main"
diff --git a/tests/lake/tests/lakefileSchema/invalid/require_git_missing_url.toml b/tests/lake/tests/lakefileSchema/invalid/require_git_missing_url.toml
new file mode 100644
index 000000000000..fa844d31508b
--- /dev/null
+++ b/tests/lake/tests/lakefileSchema/invalid/require_git_missing_url.toml
@@ -0,0 +1,15 @@
+name = "foo"
+version = "0.1.0"
+defaultTargets = ["foo"]
+
+[[require]]
+name = "dependency"
+git = { subDir = "subdirectory" }
+rev = "main"
+
+[[lean_lib]]
+name = "Foo"
+
+[[lean_exe]]
+name = "foo"
+root = "Main"
diff --git a/tests/lake/tests/lakefileSchema/test.sh b/tests/lake/tests/lakefileSchema/test.sh
new file mode 100755
index 000000000000..4d98deccf829
--- /dev/null
+++ b/tests/lake/tests/lakefileSchema/test.sh
@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+TAPLO_URL=https://github.com/tamasfe/taplo/releases/latest/download/taplo-linux-x86_64.gz
+PROJECT_ROOT=$(realpath $(pwd)/../../../..)
+
+curl -fsSL $TAPLO_URL | gzip -d - > taplo
+chmod +x taplo
+
+for file in ./valid/*.toml; do
+    echo Test: $file should be marked valid by Taplo
+    ./taplo lint --schema file://$PROJECT_ROOT/src/lake/schemas/lakefile-toml-schema.json $file
+done
+
+for file in ./invalid/*.toml; do
+    echo Test: $file should be marked invalid by Taplo
+    ! ./taplo lint --schema file://$PROJECT_ROOT/src/lake/schemas/lakefile-toml-schema.json $file
+done
\ No newline at end of file
diff --git a/tests/lake/tests/lakefileSchema/valid/default.toml b/tests/lake/tests/lakefileSchema/valid/default.toml
new file mode 100644
index 000000000000..224a19652558
--- /dev/null
+++ b/tests/lake/tests/lakefileSchema/valid/default.toml
@@ -0,0 +1,10 @@
+name = "foo"
+version = "0.1.0"
+defaultTargets = ["foo"]
+
+[[lean_lib]]
+name = "Foo"
+
+[[lean_exe]]
+name = "foo"
+root = "Main"
diff --git a/tests/lake/tests/lakefileSchema/valid/require_git_string.toml b/tests/lake/tests/lakefileSchema/valid/require_git_string.toml
new file mode 100644
index 000000000000..5c9e8e7b4790
--- /dev/null
+++ b/tests/lake/tests/lakefileSchema/valid/require_git_string.toml
@@ -0,0 +1,15 @@
+name = "foo"
+version = "0.1.0"
+defaultTargets = ["foo"]
+
+[[require]]
+name = "dependency"
+git = "https://github.com/User/package"
+rev = "main"
+
+[[lean_lib]]
+name = "Foo"
+
+[[lean_exe]]
+name = "foo"
+root = "Main"
diff --git a/tests/lake/tests/lakefileSchema/valid/require_git_url_only.toml b/tests/lake/tests/lakefileSchema/valid/require_git_url_only.toml
new file mode 100644
index 000000000000..9bd950e2068d
--- /dev/null
+++ b/tests/lake/tests/lakefileSchema/valid/require_git_url_only.toml
@@ -0,0 +1,15 @@
+name = "foo"
+version = "0.1.0"
+defaultTargets = ["foo"]
+
+[[require]]
+name = "dependency"
+git = { url = "https://github.com/User/package" }
+rev = "main"
+
+[[lean_lib]]
+name = "Foo"
+
+[[lean_exe]]
+name = "foo"
+root = "Main"
diff --git a/tests/lake/tests/lakefileSchema/valid/require_git_url_subdir.toml b/tests/lake/tests/lakefileSchema/valid/require_git_url_subdir.toml
new file mode 100644
index 000000000000..8659d33810dd
--- /dev/null
+++ b/tests/lake/tests/lakefileSchema/valid/require_git_url_subdir.toml
@@ -0,0 +1,15 @@
+name = "foo"
+version = "0.1.0"
+defaultTargets = ["foo"]
+
+[[require]]
+name = "dependency"
+git = { url = "https://github.com/User/package", subDir = "subdirectory" }
+rev = "main"
+
+[[lean_lib]]
+name = "Foo"
+
+[[lean_exe]]
+name = "foo"
+root = "Main"

From a2ae9557fcfba9532044fe2d541908daa0bf3c59 Mon Sep 17 00:00:00 2001
From: maxwell3025 <amoinus@gmail.com>
Date: Sun, 7 Dec 2025 09:21:51 -0500
Subject: [PATCH 3/7] refactor: remove redundant type spec

---
 src/lake/schemas/lakefile-toml-schema.json | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/src/lake/schemas/lakefile-toml-schema.json b/src/lake/schemas/lakefile-toml-schema.json
index d272d77f4a5c..771653ae900d 100644
--- a/src/lake/schemas/lakefile-toml-schema.json
+++ b/src/lake/schemas/lakefile-toml-schema.json
@@ -344,10 +344,6 @@
             }
         },
         "gitSpecification": {
-            "type": [
-                "string",
-                "object"
-            ],
             "anyOf": [
                 {
                     "type": "string"

From 7a69aac10c5f671fb985c97233870553f3f5298f Mon Sep 17 00:00:00 2001
From: maxwell3025 <amoinus@gmail.com>
Date: Sun, 7 Dec 2025 09:46:50 -0500
Subject: [PATCH 4/7] fix: place git specification description in correct place

---
 src/lake/schemas/lakefile-toml-schema.json | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/lake/schemas/lakefile-toml-schema.json b/src/lake/schemas/lakefile-toml-schema.json
index 771653ae900d..acb855b15ff4 100644
--- a/src/lake/schemas/lakefile-toml-schema.json
+++ b/src/lake/schemas/lakefile-toml-schema.json
@@ -362,7 +362,8 @@
                         "url"
                     ]
                 }
-            ]
+            ],
+            "description": "A dependency in a Git repository, specified by its URL."
         },
         "dependencyConfig": {
             "type": "object",
@@ -376,8 +377,7 @@
                     "description": "A dependency on the local filesystem, specified by its path."
                 },
                 "git": {
-                    "$ref": "#/definitions/gitSpecification",
-                    "description": "A dependency in a Git repository, specified by its URL."
+                    "$ref": "#/definitions/gitSpecification"
                 },
                 "subDir": {
                     "type": "string",

From 5a325184b474903ace1d4a4dae82166369d5da4f Mon Sep 17 00:00:00 2001
From: maxwell3025 <amoinus@gmail.com>
Date: Sun, 7 Dec 2025 10:48:40 -0500
Subject: [PATCH 5/7] fix: remove `anyOf` declaration in girSpecification to
 avoid LSP completion menu clutter

---
 src/lake/schemas/lakefile-toml-schema.json | 21 ++-------------------
 1 file changed, 2 insertions(+), 19 deletions(-)

diff --git a/src/lake/schemas/lakefile-toml-schema.json b/src/lake/schemas/lakefile-toml-schema.json
index acb855b15ff4..79d64e47c8b8 100644
--- a/src/lake/schemas/lakefile-toml-schema.json
+++ b/src/lake/schemas/lakefile-toml-schema.json
@@ -344,25 +344,8 @@
             }
         },
         "gitSpecification": {
-            "anyOf": [
-                {
-                    "type": "string"
-                },
-                {
-                    "type": "object",
-                    "properties": {
-                        "url": {
-                            "type": "string"
-                        },
-                        "subDir": {
-                            "type": "string"
-                        }
-                    },
-                    "required": [
-                        "url"
-                    ]
-                }
-            ],
+            "type": ["string", "object"],
+            "default": "",
             "description": "A dependency in a Git repository, specified by its URL."
         },
         "dependencyConfig": {

From cbbdb8c255e16913b6b415d1f86789982341c3eb Mon Sep 17 00:00:00 2001
From: maxwell3025 <amoinus@gmail.com>
Date: Sun, 7 Dec 2025 10:50:49 -0500
Subject: [PATCH 6/7] refactor: dereference `gitSpecification` schema
 definition

---
 src/lake/schemas/lakefile-toml-schema.json | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/src/lake/schemas/lakefile-toml-schema.json b/src/lake/schemas/lakefile-toml-schema.json
index 79d64e47c8b8..6b8ce374cf23 100644
--- a/src/lake/schemas/lakefile-toml-schema.json
+++ b/src/lake/schemas/lakefile-toml-schema.json
@@ -343,11 +343,6 @@
                 ]
             }
         },
-        "gitSpecification": {
-            "type": ["string", "object"],
-            "default": "",
-            "description": "A dependency in a Git repository, specified by its URL."
-        },
         "dependencyConfig": {
             "type": "object",
             "properties": {
@@ -360,7 +355,9 @@
                     "description": "A dependency on the local filesystem, specified by its path."
                 },
                 "git": {
-                    "$ref": "#/definitions/gitSpecification"
+                    "type": ["string", "object"],
+                    "default": "",
+                    "description": "A dependency in a Git repository, specified by its URL."
                 },
                 "subDir": {
                     "type": "string",

From e29638e321e5dac0b1ae947618edace6ef17d419 Mon Sep 17 00:00:00 2001
From: maxwell3025 <amoinus@gmail.com>
Date: Mon, 8 Dec 2025 15:38:16 -0500
Subject: [PATCH 7/7] test: remove outdated tests

See https://github.com/leanprover/vscode-lean4/pull/694
---
 tests/lake/tests/lakefileSchema/clean.sh         |  1 -
 .../invalid/require_git_empty.toml               | 15 ---------------
 .../invalid/require_git_extra_fields.toml        | 15 ---------------
 .../invalid/require_git_missing_url.toml         | 15 ---------------
 tests/lake/tests/lakefileSchema/test.sh          | 16 ----------------
 .../lake/tests/lakefileSchema/valid/default.toml | 10 ----------
 .../lakefileSchema/valid/require_git_string.toml | 15 ---------------
 .../valid/require_git_url_only.toml              | 15 ---------------
 .../valid/require_git_url_subdir.toml            | 15 ---------------
 9 files changed, 117 deletions(-)
 delete mode 100644 tests/lake/tests/lakefileSchema/clean.sh
 delete mode 100644 tests/lake/tests/lakefileSchema/invalid/require_git_empty.toml
 delete mode 100644 tests/lake/tests/lakefileSchema/invalid/require_git_extra_fields.toml
 delete mode 100644 tests/lake/tests/lakefileSchema/invalid/require_git_missing_url.toml
 delete mode 100755 tests/lake/tests/lakefileSchema/test.sh
 delete mode 100644 tests/lake/tests/lakefileSchema/valid/default.toml
 delete mode 100644 tests/lake/tests/lakefileSchema/valid/require_git_string.toml
 delete mode 100644 tests/lake/tests/lakefileSchema/valid/require_git_url_only.toml
 delete mode 100644 tests/lake/tests/lakefileSchema/valid/require_git_url_subdir.toml

diff --git a/tests/lake/tests/lakefileSchema/clean.sh b/tests/lake/tests/lakefileSchema/clean.sh
deleted file mode 100644
index a4953f9eb20d..000000000000
--- a/tests/lake/tests/lakefileSchema/clean.sh
+++ /dev/null
@@ -1 +0,0 @@
-rm ./taplo
\ No newline at end of file
diff --git a/tests/lake/tests/lakefileSchema/invalid/require_git_empty.toml b/tests/lake/tests/lakefileSchema/invalid/require_git_empty.toml
deleted file mode 100644
index 69b385308da2..000000000000
--- a/tests/lake/tests/lakefileSchema/invalid/require_git_empty.toml
+++ /dev/null
@@ -1,15 +0,0 @@
-name = "foo"
-version = "0.1.0"
-defaultTargets = ["foo"]
-
-[[require]]
-name = "dependency"
-git = {}
-rev = "main"
-
-[[lean_lib]]
-name = "Foo"
-
-[[lean_exe]]
-name = "foo"
-root = "Main"
diff --git a/tests/lake/tests/lakefileSchema/invalid/require_git_extra_fields.toml b/tests/lake/tests/lakefileSchema/invalid/require_git_extra_fields.toml
deleted file mode 100644
index 8e3d2730fe44..000000000000
--- a/tests/lake/tests/lakefileSchema/invalid/require_git_extra_fields.toml
+++ /dev/null
@@ -1,15 +0,0 @@
-name = "foo"
-version = "0.1.0"
-defaultTargets = ["foo"]
-
-[[require]]
-name = "dependency"
-git = { url = "https://github.com/User/package", subDir = "subdirectory", extra="this should not exist" }
-rev = "main"
-
-[[lean_lib]]
-name = "Foo"
-
-[[lean_exe]]
-name = "foo"
-root = "Main"
diff --git a/tests/lake/tests/lakefileSchema/invalid/require_git_missing_url.toml b/tests/lake/tests/lakefileSchema/invalid/require_git_missing_url.toml
deleted file mode 100644
index fa844d31508b..000000000000
--- a/tests/lake/tests/lakefileSchema/invalid/require_git_missing_url.toml
+++ /dev/null
@@ -1,15 +0,0 @@
-name = "foo"
-version = "0.1.0"
-defaultTargets = ["foo"]
-
-[[require]]
-name = "dependency"
-git = { subDir = "subdirectory" }
-rev = "main"
-
-[[lean_lib]]
-name = "Foo"
-
-[[lean_exe]]
-name = "foo"
-root = "Main"
diff --git a/tests/lake/tests/lakefileSchema/test.sh b/tests/lake/tests/lakefileSchema/test.sh
deleted file mode 100755
index 4d98deccf829..000000000000
--- a/tests/lake/tests/lakefileSchema/test.sh
+++ /dev/null
@@ -1,16 +0,0 @@
-#!/usr/bin/env bash
-TAPLO_URL=https://github.com/tamasfe/taplo/releases/latest/download/taplo-linux-x86_64.gz
-PROJECT_ROOT=$(realpath $(pwd)/../../../..)
-
-curl -fsSL $TAPLO_URL | gzip -d - > taplo
-chmod +x taplo
-
-for file in ./valid/*.toml; do
-    echo Test: $file should be marked valid by Taplo
-    ./taplo lint --schema file://$PROJECT_ROOT/src/lake/schemas/lakefile-toml-schema.json $file
-done
-
-for file in ./invalid/*.toml; do
-    echo Test: $file should be marked invalid by Taplo
-    ! ./taplo lint --schema file://$PROJECT_ROOT/src/lake/schemas/lakefile-toml-schema.json $file
-done
\ No newline at end of file
diff --git a/tests/lake/tests/lakefileSchema/valid/default.toml b/tests/lake/tests/lakefileSchema/valid/default.toml
deleted file mode 100644
index 224a19652558..000000000000
--- a/tests/lake/tests/lakefileSchema/valid/default.toml
+++ /dev/null
@@ -1,10 +0,0 @@
-name = "foo"
-version = "0.1.0"
-defaultTargets = ["foo"]
-
-[[lean_lib]]
-name = "Foo"
-
-[[lean_exe]]
-name = "foo"
-root = "Main"
diff --git a/tests/lake/tests/lakefileSchema/valid/require_git_string.toml b/tests/lake/tests/lakefileSchema/valid/require_git_string.toml
deleted file mode 100644
index 5c9e8e7b4790..000000000000
--- a/tests/lake/tests/lakefileSchema/valid/require_git_string.toml
+++ /dev/null
@@ -1,15 +0,0 @@
-name = "foo"
-version = "0.1.0"
-defaultTargets = ["foo"]
-
-[[require]]
-name = "dependency"
-git = "https://github.com/User/package"
-rev = "main"
-
-[[lean_lib]]
-name = "Foo"
-
-[[lean_exe]]
-name = "foo"
-root = "Main"
diff --git a/tests/lake/tests/lakefileSchema/valid/require_git_url_only.toml b/tests/lake/tests/lakefileSchema/valid/require_git_url_only.toml
deleted file mode 100644
index 9bd950e2068d..000000000000
--- a/tests/lake/tests/lakefileSchema/valid/require_git_url_only.toml
+++ /dev/null
@@ -1,15 +0,0 @@
-name = "foo"
-version = "0.1.0"
-defaultTargets = ["foo"]
-
-[[require]]
-name = "dependency"
-git = { url = "https://github.com/User/package" }
-rev = "main"
-
-[[lean_lib]]
-name = "Foo"
-
-[[lean_exe]]
-name = "foo"
-root = "Main"
diff --git a/tests/lake/tests/lakefileSchema/valid/require_git_url_subdir.toml b/tests/lake/tests/lakefileSchema/valid/require_git_url_subdir.toml
deleted file mode 100644
index 8659d33810dd..000000000000
--- a/tests/lake/tests/lakefileSchema/valid/require_git_url_subdir.toml
+++ /dev/null
@@ -1,15 +0,0 @@
-name = "foo"
-version = "0.1.0"
-defaultTargets = ["foo"]
-
-[[require]]
-name = "dependency"
-git = { url = "https://github.com/User/package", subDir = "subdirectory" }
-rev = "main"
-
-[[lean_lib]]
-name = "Foo"
-
-[[lean_exe]]
-name = "foo"
-root = "Main"