From b6115eecbe2e09315a78894d0faec449036ad6f5 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Wed, 4 Nov 2026 23:29:32 +0000 Subject: [PATCH] docs(roadmap): mark the 3d row's e172f8a / v4.13.0 as historical #57 marked 3d met at 168f09d, but the row still said TropicalAdapterPath lives at e172f8a on Lean v4.13.0, giving two current pins (CodeRabbit, outside-diff finding on #57). Those values are what was read on 2026-10-14; the current pin is the lakefile.toml require. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX --- ROADMAP.adoc | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/ROADMAP.adoc b/ROADMAP.adoc index ca756b1..d7aa668 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -62,8 +62,9 @@ are refused |3d. Import the estate's fully proved `TropicalAdapterPath.lean` behind the `Marches/Tropical.lean` seam. Do NOT paraphrase it. It lives in -hyperpolymath/tropical-types (lake package `tropical-resource-typing`) at -`e172f8a`, on Lean v4.13.0. Decided 2026-10-14: *depend, tracking latest*. +hyperpolymath/tropical-types (lake package `tropical-resource-typing`); read +on 2026-10-14 at `e172f8a`, then on Lean v4.13.0 (historical; the current +pin is in `lakefile.toml`). Decided 2026-10-14: *depend, tracking latest*. `lakefile` requires tropical-types at a pinned commit, and the weekly re-pin bot keeps that commit current. Prerequisite, upstream in tropical-types: build on marches' toolchain (hyperpolymath/tropical-types#65).