From fe8dc7045427c1c8712407ed625b5cc78ef21bf8 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 17:27:45 +0100 Subject: [PATCH] docs: describe Statlib in the overlap scan instructions `scan.md` named Statlib among the upstreams but still listed the sources, the link formats and the `upstream` values of Mathlib, Tau Ceti and LML only. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo --- scripts/overlap/scan.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/scripts/overlap/scan.md b/scripts/overlap/scan.md index 63f7b2a1..d3768704 100644 --- a/scripts/overlap/scan.md +++ b/scripts/overlap/scan.md @@ -20,7 +20,8 @@ The bundle directory (given to you with these instructions) contains: - `lmlexplore-all.txt`: every LMLExplore declaration. The full sources at the current pins are under `.lake/packages/mathlib/Mathlib`, -`.lake/packages/TauCeti/TauCeti` and `.lake/packages/LeanMachineLearning/LeanMachineLearning`. +`.lake/packages/TauCeti/TauCeti`, `.lake/packages/LeanMachineLearning/LeanMachineLearning` and +`.lake/packages/Statlib/Statlib`. LMLExplore itself is under `LMLExplore/`. ## What to look for @@ -64,7 +65,8 @@ a paragraph starting with `Preserve:` listing the LMLExplore material that must that nothing additional exists). Link to sources as `https://github.com/leanprover-community/mathlib4/blob//#L`, `https://github.com/TauCetiProject/TauCeti/blob//#L`, -`https://github.com/LeanMachineLearning/LML/blob//#L` and +`https://github.com/LeanMachineLearning/LML/blob//#L`, +`https://github.com/stat-lib/statlib/blob//#L` and `https://github.com/LeanMachineLearning/LMLExplore/blob//#L`, using the commits in `scan.json`. @@ -78,7 +80,7 @@ Write this JSON object to the result path in `scan.json`: "complete": true, "findings": [ { - "upstream": "mathlib | TauCeti | LeanMachineLearning", + "upstream": "mathlib | TauCeti | LeanMachineLearning | Statlib", "direction": "new-upstream | missed-existing", "upstream_declarations": ["fully qualified names"], "lmlexplore_declarations": ["fully qualified names"],