From 7371f70a58dadf686753c3f5174c0c1bbd28228e Mon Sep 17 00:00:00 2001 From: "Anne C.A. Baanen" Date: Thu, 9 Oct 2025 14:58:00 +0200 Subject: [PATCH 1/6] WIP: link to library notes in the doc-gen output Some implementation details are hardcoded for now. --- DocGen4/Output/DocString.lean | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index c73e621..6002716 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -241,6 +241,24 @@ partial def modifyElement (element : Element) (funName : String) : HtmlM Element else return ⟨ name, attrs, ← modifyContents contents funName modifyElement ⟩ +/-- Find all library note references in a markdown text. -/ +partial def findAllNotes (s : String) (i : String.Pos := 0) + (ret : Std.HashSet String := ∅) : Std.HashSet String := + let lps := s.posOfAux '[' s.endPos i + if lps < s.endPos then + let lpe := s.posOfAux ']' s.endPos lps + if lpe < s.endPos then + let expected := "note " + if (Substring.toString ⟨s, lps - expected.endPos, lps⟩).toLower == expected then + let citekey := Substring.toString ⟨s, ⟨lps.1 + 1⟩, lpe⟩ + findAllNotes s lpe (ret.insert citekey) + else + findAllNotes s lpe ret + else + ret + else + ret + /-- Find all references in a markdown text. -/ partial def findAllReferences (refsMap : Std.HashMap String BibItem) (s : String) (i : String.Pos := 0) (ret : Std.HashSet String := ∅) : Std.HashSet String := @@ -259,10 +277,13 @@ partial def findAllReferences (refsMap : Std.HashMap String BibItem) (s : String /-- Convert docstring to Html. -/ def docStringToHtml (docString : String) (funName : String) : HtmlM (Array Html) := do + let notesMarkdown := "\n\n" ++ (String.join <| + (findAllReferences (← read).refsMap docString).toList.map fun s => + s!"[{s}]: ##Mathlib.LibraryNote.{s}\n") let refsMarkdown := "\n\n" ++ (String.join <| (findAllReferences (← read).refsMap docString).toList.map fun s => s!"[{s}]: references.html#ref_{s}\n") - match MD4Lean.renderHtml (docString ++ refsMarkdown) with + match MD4Lean.renderHtml (docString ++ notesMarkdown ++ refsMarkdown) with | .some rendered => match manyDocument rendered.mkIterator with | .success _ res => From dd29fcaa06d480d90e32d037772d80ef9cfe6a77 Mon Sep 17 00:00:00 2001 From: "Anne C.A. Baanen" Date: Thu, 9 Oct 2025 16:33:01 +0200 Subject: [PATCH 2/6] Change the check, maybe this works better? --- DocGen4/Output/DocString.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 6002716..52abbce 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -249,7 +249,7 @@ partial def findAllNotes (s : String) (i : String.Pos := 0) let lpe := s.posOfAux ']' s.endPos lps if lpe < s.endPos then let expected := "note " - if (Substring.toString ⟨s, lps - expected.endPos, lps⟩).toLower == expected then + if (Substring.toString ⟨s, 0, lps⟩).toLower.endsWith expected then let citekey := Substring.toString ⟨s, ⟨lps.1 + 1⟩, lpe⟩ findAllNotes s lpe (ret.insert citekey) else From f7b6c5a85bd5ce6e48e63164ca01dc2cbdcd321b Mon Sep 17 00:00:00 2001 From: "Anne C.A. Baanen" Date: Thu, 9 Oct 2025 16:43:43 +0200 Subject: [PATCH 3/6] Debug --- DocGen4/Output/DocString.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 52abbce..6c66498 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -249,7 +249,8 @@ partial def findAllNotes (s : String) (i : String.Pos := 0) let lpe := s.posOfAux ']' s.endPos lps if lpe < s.endPos then let expected := "note " - if (Substring.toString ⟨s, 0, lps⟩).toLower.endsWith expected then + dbg_trace s!"last bit of the string: {(Substring.toString ⟨s, lps - expected.endPos, lps⟩)}"; + if (Substring.toString ⟨s, i, lps⟩).toLower.endsWith expected then let citekey := Substring.toString ⟨s, ⟨lps.1 + 1⟩, lpe⟩ findAllNotes s lpe (ret.insert citekey) else From b6eadd778a6d19d3eccd430062fca34953b62779 Mon Sep 17 00:00:00 2001 From: "Anne C.A. Baanen" Date: Thu, 9 Oct 2025 17:01:56 +0200 Subject: [PATCH 4/6] Don't forget to actually call your new function. aaa --- DocGen4/Output/DocString.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 6c66498..48ca3f2 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -249,8 +249,7 @@ partial def findAllNotes (s : String) (i : String.Pos := 0) let lpe := s.posOfAux ']' s.endPos lps if lpe < s.endPos then let expected := "note " - dbg_trace s!"last bit of the string: {(Substring.toString ⟨s, lps - expected.endPos, lps⟩)}"; - if (Substring.toString ⟨s, i, lps⟩).toLower.endsWith expected then + if (Substring.toString ⟨s, lps - expected.endPos, lps⟩).toLower == expected then let citekey := Substring.toString ⟨s, ⟨lps.1 + 1⟩, lpe⟩ findAllNotes s lpe (ret.insert citekey) else @@ -279,7 +278,7 @@ partial def findAllReferences (refsMap : Std.HashMap String BibItem) (s : String /-- Convert docstring to Html. -/ def docStringToHtml (docString : String) (funName : String) : HtmlM (Array Html) := do let notesMarkdown := "\n\n" ++ (String.join <| - (findAllReferences (← read).refsMap docString).toList.map fun s => + (findAllNotes docString).toList.map fun s => s!"[{s}]: ##Mathlib.LibraryNote.{s}\n") let refsMarkdown := "\n\n" ++ (String.join <| (findAllReferences (← read).refsMap docString).toList.map fun s => From e33e382f60b04fc03d7f003b2f70a30dbaef959c Mon Sep 17 00:00:00 2001 From: "Anne C.A. Baanen" Date: Thu, 9 Oct 2025 17:05:33 +0200 Subject: [PATCH 5/6] Quote the reference so it gets parsed. --- DocGen4/Output/DocString.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 48ca3f2..ce09dd8 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -279,7 +279,7 @@ partial def findAllReferences (refsMap : Std.HashMap String BibItem) (s : String def docStringToHtml (docString : String) (funName : String) : HtmlM (Array Html) := do let notesMarkdown := "\n\n" ++ (String.join <| (findAllNotes docString).toList.map fun s => - s!"[{s}]: ##Mathlib.LibraryNote.{s}\n") + s!"[{s}]: ##Mathlib.LibraryNote.«{s}»\n") let refsMarkdown := "\n\n" ++ (String.join <| (findAllReferences (← read).refsMap docString).toList.map fun s => s!"[{s}]: references.html#ref_{s}\n") From c7881def2a694eabd5817ed1296a292e59e2a8cb Mon Sep 17 00:00:00 2001 From: "Anne C.A. Baanen" Date: Thu, 9 Oct 2025 17:31:06 +0200 Subject: [PATCH 6/6] Format it clearly as link destination --- DocGen4/Output/DocString.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index ce09dd8..22ced01 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -279,7 +279,7 @@ partial def findAllReferences (refsMap : Std.HashMap String BibItem) (s : String def docStringToHtml (docString : String) (funName : String) : HtmlM (Array Html) := do let notesMarkdown := "\n\n" ++ (String.join <| (findAllNotes docString).toList.map fun s => - s!"[{s}]: ##Mathlib.LibraryNote.«{s}»\n") + s!"[{s}]: <##Mathlib.LibraryNote.«{s}»>\n") let refsMarkdown := "\n\n" ++ (String.join <| (findAllReferences (← read).refsMap docString).toList.map fun s => s!"[{s}]: references.html#ref_{s}\n")