From 8dda2299df7e0ca1e123d28979823e93f29e59d5 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Fri, 20 Jun 2025 07:07:21 +0900 Subject: [PATCH 1/2] add `Book` --- .../VersoManual/Bibliography.lean | 27 ++++++++++++++++--- 1 file changed, 24 insertions(+), 3 deletions(-) diff --git a/src/verso-manual/VersoManual/Bibliography.lean b/src/verso-manual/VersoManual/Bibliography.lean index ae61ce02..474a6ed7 100644 --- a/src/verso-manual/VersoManual/Bibliography.lean +++ b/src/verso-manual/VersoManual/Bibliography.lean @@ -53,6 +53,19 @@ structure Thesis where url : Option String := none deriving ToJson, FromJson, BEq, Hashable, Ord +structure Book where + title : Doc.Inline Manual + authors : Array (Doc.Inline Manual) + year : Int + url : Option String := none + isbn : Option String := none -- TODO: make concrete type `ISBN10` or `ISBN13` + publisher : Option (Doc.Inline Manual) := none + edition : Option (Doc.Inline Manual) := none + series : Option (Doc.Inline Manual) := none + number: Option Int := none + +deriving ToJson, FromJson, BEq, Hashable, Ord + structure ArXiv where title : Doc.Inline Manual authors : Array (Doc.Inline Manual) @@ -77,6 +90,7 @@ inductive Citable where | thesis : Thesis → Citable | arXiv : ArXiv → Citable | article : Article → Citable + | book : Book → Citable deriving ToJson, FromJson, BEq, Hashable, Ord instance : Coe InProceedings Citable where @@ -91,21 +105,25 @@ instance : Coe ArXiv Citable where instance : Coe Article Citable where coe := .article +instance : Coe Book Citable where + coe := .book + def Citable.authors : Citable → Array (Doc.Inline Manual) - | .inProceedings p | .arXiv p | .article p => p.authors + | .inProceedings p | .arXiv p | .article p | .book p => p.authors | .thesis p => #[p.author] def Citable.title : Citable → Doc.Inline Manual - | .inProceedings p | .arXiv p | .thesis p | .article p => p.title + | .inProceedings p | .arXiv p | .thesis p | .article p | .book p => p.title def Citable.year : Citable → Int - | .inProceedings p | .arXiv p | .thesis p | .article p => p.year + | .inProceedings p | .arXiv p | .thesis p | .article p | .book p => p.year def Citable.url : Citable → Option String | .inProceedings p => p.url | .thesis p => p.url | .arXiv p => some s!"https://arxiv.org/abs/{p.id}" | .article p => p.url + | .book p => p.url private def slugString : Doc.Inline Manual → String @@ -167,6 +185,9 @@ def Citable.bibHtml (go : Doc.Inline Genre.Manual → HtmlT Manual (ReaderT Exte | .arXiv p => let authors ← andList <$> p.authors.mapM go return {{ {{authors}} s!", {p.year}. " {{ link {{"“" {{← go p.title}} "”"}} }} ". arXiv:" {{p.id}} }} + | .book p => + let authors ← andList <$> p.authors.mapM go + return {{ {{authors}} s!", {p.year}. " {{ link {{"“" {{← go p.title}} "”"}} }} }} where wrap (content : Html) : Html := {{{{content}}}} link (title : Html) : Html := From 1d78d280605e68402a38c7666614a2f782130ac8 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Fri, 20 Jun 2025 08:19:54 +0900 Subject: [PATCH 2/2] wip for bib --- examples/textbook/DemoTextbook.lean | 3 ++- examples/textbook/DemoTextbook/Papers.lean | 14 +++++++++++--- src/verso-manual/VersoManual/Bibliography.lean | 17 +++++++++++------ 3 files changed, 24 insertions(+), 10 deletions(-) diff --git a/examples/textbook/DemoTextbook.lean b/examples/textbook/DemoTextbook.lean index 8bd8b9ab..3464476b 100644 --- a/examples/textbook/DemoTextbook.lean +++ b/examples/textbook/DemoTextbook.lean @@ -98,11 +98,12 @@ Cite works using {lean}`citet`, {lean}`citep`, or {lean}`citehere`. They take a name of a citable reference value as a parameter. References should be defined as values, typically in one module that is imported (similar to the role of a `.bib` file in LaTeX). -Textual citations, as with {citet someThesis}[], look like this. +Textual citations, as with {citet someBook}[], look like this. Parenthetical {citep someArXiv}[] looks like this. Use {lean}`citehere` to literally include the cite rather than making a margin note, e.g. {citehere somePaper}[]. Literally-included cites are mostly useful when performing citation inside a margin note. + # Section References %%% tag := "sec-ref" diff --git a/examples/textbook/DemoTextbook/Papers.lean b/examples/textbook/DemoTextbook/Papers.lean index d5ce6179..d20e2924 100644 --- a/examples/textbook/DemoTextbook/Papers.lean +++ b/examples/textbook/DemoTextbook/Papers.lean @@ -8,21 +8,29 @@ open Verso.Genre.Manual -- Here, `inlines!` is a macro that parses a string constant into Verso inline elements -def someThesis : Thesis where +def someThesis : Bibliography.Thesis where title := inlines!"A Great Thesis" author := inlines!"A. Great Student" year := 2025 university := inlines!"A University" degree := inlines!"Something" -def somePaper : InProceedings where +def somePaper : Bibliography.InProceedings where title := inlines!"Grommulation of Flying Lambdas" authors := #[inlines!"A. Great Student"] year := 2025 booktitle := inlines!"Proceedings of the Best Conference Ever" -def someArXiv : ArXiv where +def someArXiv : Bibliography.ArXiv where title := inlines!"Grommulation of Flying Lambdas" authors := #[inlines!"A. Great Student"] year := 2025 id := "...insert arXiv id here..." + +def someBook : Bibliography.Book where + title := inlines!"A Good Book" + authors := #[inlines!"A. Great Student"] + year := 2025 + publisher := inlines!"Oxford University Press" + series := some (inlines!"Series Books", 42) + isbn := some "978-0-19-853779-3" diff --git a/src/verso-manual/VersoManual/Bibliography.lean b/src/verso-manual/VersoManual/Bibliography.lean index 474a6ed7..911e377e 100644 --- a/src/verso-manual/VersoManual/Bibliography.lean +++ b/src/verso-manual/VersoManual/Bibliography.lean @@ -59,11 +59,9 @@ structure Book where year : Int url : Option String := none isbn : Option String := none -- TODO: make concrete type `ISBN10` or `ISBN13` - publisher : Option (Doc.Inline Manual) := none + publisher : Doc.Inline Manual edition : Option (Doc.Inline Manual) := none - series : Option (Doc.Inline Manual) := none - number: Option Int := none - + series : Option ((Doc.Inline Manual) × Int) := none deriving ToJson, FromJson, BEq, Hashable, Ord structure ArXiv where @@ -176,7 +174,10 @@ def Citable.bibHtml (go : Doc.Inline Genre.Manual → HtmlT Manual (ReaderT Exte match c with | .inProceedings p => let authors ← andList <$> p.authors.mapM go - return {{ {{authors}} s!", {p.year}. " {{ link {{"“" {{← go p.title}} "”"}} }} ". In " {{← go p.booktitle}}"."{{(← p.series.mapM go).map ({{" (" {{·}} ")" }}) |>.getD .empty}} }} + return {{ + {{authors}} s!", {p.year}. " {{ link {{"“" {{← go p.title}} "”"}} }} + ". In " {{← go p.booktitle}}"."{{(← p.series.mapM go).map ({{" (" {{·}} ")" }}) |>.getD .empty}} + }} | .article p => let authors ← andList <$> p.authors.mapM go return {{ {{authors}} " (" {{(← p.month.mapM go).map (· ++ {{" "}}) |>.getD .empty}}s!"{p.year}" "). " {{ link {{"“" {{← go p.title}} "”"}} }} ". " {{← go p.journal}}"." {{← go p.volume}}" "{{← go p.number}} {{p.pages.map (fun (x, y) => s!"pp. {x}–{y}") |>.getD .empty }} "."}} @@ -187,7 +188,11 @@ def Citable.bibHtml (go : Doc.Inline Genre.Manual → HtmlT Manual (ReaderT Exte return {{ {{authors}} s!", {p.year}. " {{ link {{"“" {{← go p.title}} "”"}} }} ". arXiv:" {{p.id}} }} | .book p => let authors ← andList <$> p.authors.mapM go - return {{ {{authors}} s!", {p.year}. " {{ link {{"“" {{← go p.title}} "”"}} }} }} + return {{ + {{authors}} s!", {p.year}. " {{ link {{"“" {{← go p.title}} "”"}} }} ". " + {{ p.series.map (λ (s, v) => {{ "Volume " s!"{v}" " of " /- TODO: insert series -/ ", "}}) |>.getD .empty }} + {{← go (p.publisher)}}". " + }} where wrap (content : Html) : Html := {{{{content}}}} link (title : Html) : Html :=