fix: restore authored PDF dates and titles

.github/workflows/gh-pages.yml

@@ -110,9 +110,9 @@ jobs:
         with:
           version: "0.4.27"
           # enable-cache: true
-      - name: Install xsltproc
+      - name: Install xsltproc and PDF text tools
         run: |
-          sudo apt install xsltproc
+          sudo apt install xsltproc poppler-utils
       # - name: Install Homebrew
       #   run: |
       #     bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"

assets/article.xsl

@@ -110,7 +110,14 @@
 
   <!-- AGENT-NOTE: Untyped note trees still carry Lean metadata and need a PDF-visible marker row. -->
   <xsl:template name="section-title">
-    <xsl:apply-templates />
+    <xsl:choose>
+      <xsl:when test="html:span[@class='translation-section-title']">
+        <xsl:apply-templates select="html:span[@class='translation-section-title']/node()" />
+      </xsl:when>
+      <xsl:otherwise>
+        <xsl:apply-templates />
+      </xsl:otherwise>
+    </xsl:choose>
     <xsl:call-template name="lean-marker-metadata">
       <xsl:with-param name="frontmatter" select=".." />
       <xsl:with-param name="continuation" select="true()" />

assets/latex.xsl

@@ -21,6 +21,49 @@
       </xsl:if>
     </xsl:for-each>
     <xsl:text>}</xsl:text>
+    <xsl:if test="f:date">
+      <xsl:text>\date{</xsl:text>
+      <xsl:call-template name="publication-date">
+        <xsl:with-param name="date" select="f:date" />
+      </xsl:call-template>
+      <xsl:text>}</xsl:text>
+    </xsl:if>
+  </xsl:template>
+
+  <!-- Keep the source-authored date visible while lize.sh freezes PDF metadata. -->
+  <xsl:template name="publication-date">
+    <xsl:param name="date" />
+    <xsl:choose>
+      <xsl:when test="$date/f:month">
+        <xsl:choose>
+          <xsl:when test="$date/f:month = 1">January</xsl:when>
+          <xsl:when test="$date/f:month = 2">February</xsl:when>
+          <xsl:when test="$date/f:month = 3">March</xsl:when>
+          <xsl:when test="$date/f:month = 4">April</xsl:when>
+          <xsl:when test="$date/f:month = 5">May</xsl:when>
+          <xsl:when test="$date/f:month = 6">June</xsl:when>
+          <xsl:when test="$date/f:month = 7">July</xsl:when>
+          <xsl:when test="$date/f:month = 8">August</xsl:when>
+          <xsl:when test="$date/f:month = 9">September</xsl:when>
+          <xsl:when test="$date/f:month = 10">October</xsl:when>
+          <xsl:when test="$date/f:month = 11">November</xsl:when>
+          <xsl:when test="$date/f:month = 12">December</xsl:when>
+        </xsl:choose>
+        <xsl:if test="$date/f:day">
+          <xsl:text> </xsl:text>
+          <xsl:value-of select="$date/f:day" />
+          <xsl:if test="$date/f:year">
+            <xsl:text>, </xsl:text>
+          </xsl:if>
+        </xsl:if>
+      </xsl:when>
+    </xsl:choose>
+    <xsl:value-of select="$date/f:year" />
+  </xsl:template>
+
+  <!-- Forester 5 expands anonymous translation subsections with a parent link. -->
+  <xsl:template match="f:title[html:span[@class='translation-section-title']]">
+    <xsl:apply-templates select="html:span[@class='translation-section-title']/node()" />
   </xsl:template>
 
   <xsl:template match="f:tree[not(f:frontmatter/f:taxon)]">

assets/uts-overrides.xsl

@@ -8,6 +8,11 @@
     xmlns:html="http://www.w3.org/1999/xhtml"
 >
 
+    <!-- Forester 5 adds root context to nested translation section titles. -->
+    <xsl:template match="fr:title[html:span[@class='translation-section-title']]">
+        <xsl:apply-templates select="html:span[@class='translation-section-title']/node()" />
+    </xsl:template>
+
     <!-- <xsl:template name="numbered-taxon">
         <span class="taxon">
             <xsl:apply-templates select="fr:taxon" />

justfile

@@ -134,10 +134,11 @@ verify-render:
 verify-pdf-fixtures:
     #!/usr/bin/env bash
     set -euo pipefail
-    for tree_id in spin-0001 hopf-0001 ca-0001 fgap-0001 fcap-0001 tt-0001 uts-000C; do
+    for tree_id in spin-0001 hopf-0001 ca-0001 fgap-0001 fgap-001F fgap-001G fcap-0001 connes-0001 tt-0001 uts-000C; do
         ./lize.sh "$tree_id" > "build/forester-pdf-$tree_id.log" 2>&1
         ./verify-forester-output.sh output/forest "$tree_id"
     done
+    bash ./verify-pdf-dates.sh spin-0001 hopf-0001 ca-0001 fgap-0001 fgap-001F fgap-001G fcap-0001 connes-0001 tt-0001 uts-000C
 
 pre-push:
     just chk

trees/ca-0003.tree

@@ -6,7 +6,7 @@
 % convention corollary axiom example exercise proof
 % discussion remark
 % \taxon{}
-\card{Definition}{Bilinear form}{
+\card{Definition}{bilinear form}{
     \label{BilinForm}
     \leanok
     \lean{BilinForm}
@@ -29,4 +29,3 @@ An \newvocab{bilinear form} #{B} over #{M} is a map #{B : M \to M \to R}, satisf
 
 for all #{a \in R, x, y, z \in M}.
 }}
-

trees/ca-000F.tree

@@ -2,8 +2,6 @@
 % clifford hopf spin draft
 \tag{clifford}
 
-\parent{ca-0001}
-
 % definition theorem lemma construction observation
 % convention corollary axiom example exercise proof
 % discussion remark
@@ -28,4 +26,4 @@
 
 \transclude{ca-000D}
 
-\transclude{ca-000E}
+\transclude{ca-000E}

trees/ca-000G.tree

@@ -2,7 +2,6 @@
 % clifford hopf spin draft
 \tag{clifford}
 
-\parent{ca-0001}
 \title{Operations}
 
 \transclude{ca-000H}

trees/ca-000I.tree

@@ -9,7 +9,7 @@
 % \refnote{}{}{
 % }
 
-\refdef{Grade involution}{wieser2022formalizing}{
+\refdef{grade involution}{wieser2022formalizing}{
 \p{
     \label{involute}
     \lean{CliffordAlgebra.involute}
@@ -44,4 +44,3 @@
 \p{    It's denoted #{\hat{m}} in \cite{lounesto2001clifford}, #{\alpha(m)} in \cite{jadczyk2019notes}, #{m^*} in \cite{chisolm2012geometric}.}
 
 }
-

trees/ca-000J.tree

@@ -9,7 +9,7 @@
 % \refnote{}{}{
 % }
 
-\refdef{Grade reversion}{wieser2022formalizing}{
+\refdef{grade reversion}{wieser2022formalizing}{
 \p{
     \label{reverse}
     \lean{CliffordAlgebra.reverse}
@@ -41,4 +41,3 @@
 
 \p{    It's denoted #{\tilde{m}} in \cite{lounesto2001clifford}, #{m^\tau} in \cite{jadczyk2019notes} (with variants like #{m^t} or #{m^\top} in other literatures), #{m^\dagger} in \cite{chisolm2012geometric}.
 }}
-

trees/macros.tree

@@ -476,7 +476,7 @@ so the text size almost matches the size output by native forester code. This do
   \put?\translation/dst{🇺🇸}
   \let\src{\get\translation/src}
   \let\dst{\get\translation/dst}
-  \block{\dst-content \langblock{\src}{\src-content}}{\body}
+  \block{\<html:span>[class]{translation-section-title}{\dst-content \langblock{\src}{\src-content}}}{\body}
 }
 
 \p{\code{translation/ttitle[dst-content][src-content]}: A translation title.}

trees/tt-000E.tree

@@ -5,7 +5,7 @@
 % definition theorem lemma construction observation
 % convention corollary axiom example exercise proof
 % discussion remark notation
-\refcardt{Lemma}{Iso}{2.4}{kostecki2011introduction}{
+\refcardt{Lemma}{iso}{2.4}{kostecki2011introduction}{
 
 \p{An iso arrow is always monic and epic. However, not every arrow which is monic and epic is also iso.}
 
@@ -32,4 +32,4 @@
     }
   }
 }
-}
+}

trees/tt-000J.tree

@@ -7,12 +7,12 @@
 % discussion remark notation
 \taxon{Convention}
 
-\title{Uniqueness: dashed arrow}
+\title{uniqueness: dashed arrow}
 
 \p{Uniqueness of an arrow is denoted #{\exists ! f} or simply #{!f}, and visualized as a \vocab{dashed arrow} in diagrams, and #{!} is often omitted.}
 
 \tikzfig{\begin{tikzcd}
     {} && {}
     \arrow["!f", dashed, from=1-1, to=1-3]
 \end{tikzcd}
-}
+}

trees/tt-000S.tree

@@ -7,6 +7,6 @@
 % discussion remark notation
 \taxon{Convention}
 
-\title{Grey arrow}
+\title{grey arrow}
 
 \p{We use \newvocab{grey arrow}s to represent the composition arrow in a \vocab{fork}. This convention is not from literatures and is subject to change.}

trees/tt-001D.tree

@@ -7,7 +7,7 @@
 % discussion remark notation
 \taxon{Convention}
 
-\title{Functors}
+\title{functors}
 
 \p{For simplicity, when there is no confusion, we use #{\bullet} to represent corresponding objects, and omit the arrow names in the codomain of a functor, e.g.
 

trees/tt-0024.tree

@@ -5,10 +5,10 @@
 % definition theorem lemma construction observation
 % convention corollary axiom example exercise proof
 % discussion remark notation
-\refcardt{Remark}{Limits}{ch. 5}{leinster2016basic}{
+\refcardt{Remark}{limits}{ch. 5}{leinster2016basic}{
 
 \p{[Adjointness](tt-001T) is about the relationships \em{between} categories. [Representability](tt-002K) is a property of [\em{set-valued}](tt-001L) functors. \vocab{Limit}s are about what goes on \em{inside} a category.}
 
 \p{Whenever you meet a method for taking some objects and arrows in a category and constructing a new object out of them, there is a good chance that you are looking at either a \vocab{limit} or a \vocab{colimit}.}
 
-}
+}

trees/tt-004B.tree

@@ -10,7 +10,7 @@
 
 % kostecki2011introduction leinster2016basic nakahira2023diagrammatic
 
-\taxon{Notation}\title{Presheaf}
+\taxon{Notation}\title{presheaf}
 
 \p{We'll use #{\fF} to denote a \vocabk{presheaf}{tt-002Q} since sheaf in French is \newvocab{faisceau}.
 }

verify-pdf-dates.sh

@@ -0,0 +1,47 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+if [ "$#" -eq 0 ]; then
+    echo "Usage: $0 TREE_ID [...]" >&2
+    exit 2
+fi
+
+for tree_id in "$@"; do
+    source_file="trees/$tree_id.tree"
+    pdf_file="output/forest/$tree_id.pdf"
+    source_date=$(sed -nE 's/^[[:space:]]*\\date\{([0-9]{4})-([0-9]{2})-([0-9]{2})\}[[:space:]]*$/\1-\2-\3/p' "$source_file")
+
+    if [ -z "$source_date" ]; then
+        echo "Missing ISO publication date in $source_file" >&2
+        exit 1
+    fi
+
+    IFS=- read -r year month day <<< "$source_date"
+    case "$month" in
+        01) month_name=January ;;
+        02) month_name=February ;;
+        03) month_name=March ;;
+        04) month_name=April ;;
+        05) month_name=May ;;
+        06) month_name=June ;;
+        07) month_name=July ;;
+        08) month_name=August ;;
+        09) month_name=September ;;
+        10) month_name=October ;;
+        11) month_name=November ;;
+        12) month_name=December ;;
+        *)
+            echo "Invalid month in $source_file: $source_date" >&2
+            exit 1
+            ;;
+    esac
+    expected_date="$month_name $((10#$day)), $year"
+
+    pdf_text=$(pdftotext "$pdf_file" -)
+    if ! grep -Fqx "$expected_date" <<< "$pdf_text"; then
+        echo "PDF publication date mismatch for $tree_id: expected $expected_date" >&2
+        exit 1
+    fi
+done
+
+echo "PDF publication dates verified for $# fixture(s)"