From 508f26589b64c5bbca10c9812a434db5665c6077 Mon Sep 17 00:00:00 2001
From: Jonathan Cubides <prieto.jona@gmail.com>
Date: Thu, 13 Aug 2026 18:23:52 -0500
Subject: [PATCH] build: pin newest first-party releases

---
 CHANGELOG.md       |  4 ++++
 lake-manifest.json | 28 ++++++++++++++--------------
 lakefile.lean      |  8 ++++----
 3 files changed, 22 insertions(+), 18 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 16d003e..ee2804a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,9 @@
 # Changelog
 
+## 4.0.9 — 2026-08-13
+
+- Pin every first-party dependency to its newest released tag.
+
 ## 4.0.8 — 2026-08-13
 
 - Centralize lexical typing-environment scopes for binders and event parameters.
diff --git a/lake-manifest.json b/lake-manifest.json
index 4fc816a..2ddc50a 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,60 +15,60 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "cb413a668e43df68610d27aeb557cf47d4ce331f",
+   "rev": "ace54bd626ccc2f2be2b2c92aba73621e939dbb9",
    "name": "«termcolor-diagnostics»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.1.10",
+   "inputRev": "v0.1.16",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/jonaprieto/lean-argus.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "22f0b8b4196f0716938720fa529a566be0009cf1",
+   "rev": "19b79fe7cad9538db00c707dee4af3c79c642fef",
    "name": "argus",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.5.0",
+   "inputRev": "v0.5.3",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/jonaprieto/lean-grip",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fd849c244dbf4da0592ca403f89fcd468e115403",
+   "rev": "e16b6d4a735d8f194a2a02550a551d0194bf9d80",
    "name": "grip",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.1.0",
+   "inputRev": "v0.3.4",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/jonaprieto/lean-termcolor-layout.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bc8aa8e7d0ccc01f1615b218e776183a61c37c91",
+   "rev": "9b9532044ebf6dc93b52d0459ce1968ad869ebc6",
    "name": "«termcolor-layout»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.1.8",
+   "inputRev": "v0.1.13",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/jonaprieto/lean-termcolor-terminal.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b66e3870e15bb3eb7030ae9831d99b52f5f52736",
+   "rev": "dd48122caeaa986b95cea5c766fb449228db204a",
    "name": "«termcolor-terminal»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.3.1",
+   "inputRev": "v0.3.6",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/jonaprieto/lean-termcolor.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5a08bdadb6dc95f36e6b25d48b6812bc6e6d8b01",
+   "rev": "151cacea0983bde7399c2eca3cf008098ef95086",
    "name": "termcolor",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v1.1.0",
+   "inputRev": "v1.1.5",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "ead2003ccac8780b58e380ba7de65860ad5e5f26",
+   "rev": "ebf6f17fcf83f6726dcbefa9b1a0afc9d2fa531d",
    "name": "«termcolor-widgets»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.1.9",
+   "inputRev": "v0.1.13",
    "inherited": true,
    "configFile": "lakefile.lean"}],
  "name": "eventb",
diff --git a/lakefile.lean b/lakefile.lean
index 97bfddc..195973d 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,20 +2,20 @@ import Lake
 open Lake DSL
 
 package «eventb» where
-  version := v!"4.0.8"
+  version := v!"4.0.9"
   leanOptions := #[⟨`autoImplicit, false⟩, ⟨`relaxedAutoImplicit, false⟩]
 
 -- Pinned release tags, not `main`: corpus gate numbers are only reproducible if the
 -- parser underneath them is too.
 require grip from git
-  "https://github.com/jonaprieto/lean-grip" @ "v0.1.0"
+  "https://github.com/jonaprieto/lean-grip" @ "v0.3.4"
 
 require argus from git
-  "https://github.com/jonaprieto/lean-argus.git" @ "v0.5.0"
+  "https://github.com/jonaprieto/lean-argus.git" @ "v0.5.3"
 
 require «termcolor-diagnostics» from git
   "https://github.com/jonaprieto/lean-termcolor-diagnostics.git"
-  @ "v0.1.10"
+  @ "v0.1.16"
 
 require "leanprover-community" / "proofwidgets" @ git "v0.0.108"