[create-pull-request] automated change

Author: github-merge-queue[bot]

Blase/lake-manifest.json

@@ -22,10 +22,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2100ee662d0d4b3233534f70716a04f15f74c300",
+   "rev": "47232c86ec8a757736df7a7e225fff8044ec0913",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing-2025-12-01",
+   "inputRev": "nightly-testing-2025-12-03",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
@@ -72,7 +72,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eda0afd936954acb4006b3786b61fe9f621cc00d",
+   "rev": "8e37a9bed06d16a2c4253ee62938e216d3fc9a3a",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -82,7 +82,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1fd34ec2de724344b0ba4b84c5f93627c941a272",
+   "rev": "2fa5d6eaad021d45b7262e79cbf6f68a2d65adfd",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -92,7 +92,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9eab46cb0b18faa48a241f2e03f7304d4e19ebe0",
+   "rev": "9a0ab3e8886a335b378baae6b58ce7df96440dba",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",

Blase/lakefile.toml

@@ -13,7 +13,7 @@ name = "Blase"
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4-nightly-testing"
-rev = "nightly-testing-2025-12-01"
+rev = "nightly-testing-2025-12-03"
 
 [[lean_lib]]
 name = "BlaseTest"

LeanMLIR/lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2100ee662d0d4b3233534f70716a04f15f74c300",
+   "rev": "47232c86ec8a757736df7a7e225fff8044ec0913",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing-2025-12-01",
+   "inputRev": "nightly-testing-2025-12-03",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eda0afd936954acb4006b3786b61fe9f621cc00d",
+   "rev": "8e37a9bed06d16a2c4253ee62938e216d3fc9a3a",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1fd34ec2de724344b0ba4b84c5f93627c941a272",
+   "rev": "2fa5d6eaad021d45b7262e79cbf6f68a2d65adfd",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9eab46cb0b18faa48a241f2e03f7304d4e19ebe0",
+   "rev": "9a0ab3e8886a335b378baae6b58ce7df96440dba",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",

LeanMLIR/lakefile.toml

@@ -8,4 +8,4 @@ name = "LeanMLIR"
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4-nightly-testing"
-rev = "nightly-testing-2025-12-01"
+rev = "nightly-testing-2025-12-03"

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "99b86fee3af9ab6a04345e58cb933be23c9d573e",
+   "rev": "1878b52c91ffd4c21bc09c8a1edd39907b34a357",
    "name": "SailRV64",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9d2639b76d29e1d0493e9597640726406a951b3b",
+   "rev": "4bb7fb1802b2fc580ebe845936dc2b255d68a695",
    "name": "leanwuzla",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -63,30 +63,40 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c02420a8a248c95883a676a40de12cf773aa1fc4",
+   "rev": "1c5153dd9f1410d1316fd23a2f0680d47e15fc80",
    "name": "Lean_RV64D",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/rems-project/lean-sail",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "aed25177482c50db6a7d8da8144388cc69da10f2",
+   "name": "Sail",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v2",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/opencompl/valaig",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7bcb9df848cc53100152ebfb7f94458a056a553a",
+   "rev": "97fc5d8872fdd4ccb4655a7ad97df5852670c1e7",
    "name": "valaig",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "7bcb9df848cc53100152ebfb7f94458a056a553a",
+   "inputRev": "97fc5d8872fdd4ccb4655a7ad97df5852670c1e7",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4-nightly-testing",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2100ee662d0d4b3233534f70716a04f15f74c300",
+   "rev": "47232c86ec8a757736df7a7e225fff8044ec0913",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing-2025-12-01",
+   "inputRev": "nightly-testing-2025-12-03",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
@@ -133,7 +143,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eda0afd936954acb4006b3786b61fe9f621cc00d",
+   "rev": "8e37a9bed06d16a2c4253ee62938e216d3fc9a3a",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -143,7 +153,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1fd34ec2de724344b0ba4b84c5f93627c941a272",
+   "rev": "2fa5d6eaad021d45b7262e79cbf6f68a2d65adfd",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -153,7 +163,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9eab46cb0b18faa48a241f2e03f7304d4e19ebe0",
+   "rev": "9a0ab3e8886a335b378baae6b58ce7df96440dba",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-12-01
+leanprover/lean4:nightly-2026-01-22