Add "Proof" section to slug detail pages linking to proof source

html-generators/generate.java

@@ -404,6 +404,30 @@ String renderDocLinks(String tpl, JsonNode docs) {
     return String.join("\n", links);
 }
 
+String slugToPascalCase(String slug) {
+    return Arrays.stream(slug.split("-"))
+            .filter(w -> !w.isEmpty())
+            .map(w -> Character.toUpperCase(w.charAt(0)) + w.substring(1))
+            .collect(Collectors.joining());
+}
+
+String renderProofSection(Snippet s, Map<String, String> strings) {
+    var pascal = slugToPascalCase(s.slug());
+    var proofFile = Path.of("proof", s.category(), pascal + ".java");
+    if (!Files.exists(proofFile)) return "";
+    var proofUrl = "https://github.com/javaevolved/javaevolved.github.io/blob/main/proof/%s/%s.java"
+            .formatted(s.category(), pascal);
+    var label = strings.getOrDefault("sections.proof", "Proof");
+    var linkText = strings.getOrDefault("sections.proofLink", "View proof source");
+    return """
+    <section class="docs-section">
+      <div class="section-label">%s</div>
+      <div class="docs-links">
+        <a href="%s" target="_blank" rel="noopener" class="doc-link">%s ↗</a>
+      </div>
+    </section>""".formatted(label, proofUrl, linkText);
+}
+
 String renderRelatedSection(String tpl, Snippet snippet, Map<String, Snippet> all, String locale, Map<String, String> strings) {
     return snippet.related().stream().filter(all::containsKey)
             .map(p -> renderRelatedCard(tpl, all.get(p), locale, strings))
@@ -469,6 +493,7 @@ String generateHtml(Templates tpl, Snippet s, Map<String, Snippet> all, Map<Stri
             Map.entry("navArrows", renderNavArrows(s, locale)),
             Map.entry("whyCards", renderWhyCards(tpl.whyCard(), s.whyModernWins())),
             Map.entry("docLinks", renderDocLinks(tpl.docLink(), s.node().withArray("docs"))),
+            Map.entry("proofSection", renderProofSection(s, extraTokens)),
             Map.entry("relatedCards", renderRelatedSection(tpl.relatedCard(), s, all, locale, extraTokens)),
             Map.entry("socialShare", renderSocialShare(tpl.socialShare(), s.slug(), s.title(), extraTokens))));
     var localeName = LOCALES.getOrDefault(locale, locale);

html-generators/generate.py

@@ -341,6 +341,32 @@ def render_related_section(tpl, data, all_snippets, locale, strings):
     return "\n".join(cards)
 
 
+def slug_to_pascal_case(slug):
+    """Convert a hyphen-delimited slug to PascalCase. E.g. 'type-inference-with-var' -> 'TypeInferenceWithVar'."""
+    return "".join(w.capitalize() for w in slug.split("-") if w)
+
+
+def render_proof_section(data, strings):
+    """Render the proof section linking to the proof source file on GitHub, or empty string if no proof exists."""
+    slug = data["slug"]
+    category = data["category"]
+    pascal = slug_to_pascal_case(slug)
+    proof_file = os.path.join("proof", category, f"{pascal}.java")
+    if not os.path.isfile(proof_file):
+        return ""
+    proof_url = f"https://github.com/javaevolved/javaevolved.github.io/blob/main/proof/{category}/{pascal}.java"
+    label = strings.get("sections.proof", "Proof")
+    link_text = strings.get("sections.proofLink", "View proof source")
+    return (
+        '    <section class="docs-section">\n'
+        f'      <div class="section-label">{label}</div>\n'
+        '      <div class="docs-links">\n'
+        f'        <a href="{proof_url}" target="_blank" rel="noopener" class="doc-link">{link_text} ↗</a>\n'
+        '      </div>\n'
+        '    </section>'
+    )
+
+
 def render_social_share(tpl, slug, title, strings):
     """Render social share URLs."""
     encoded_url = url_encode(f"{BASE_URL}/{slug}.html")
@@ -520,6 +546,7 @@ def generate_html(templates, data, all_snippets, extra_tokens, locale):
         "navArrows": render_nav_arrows(data, locale),
         "whyCards": render_why_cards(templates["why_card"], data["whyModernWins"]),
         "docLinks": render_doc_links(templates["doc_link"], data.get("docs", [])),
+        "proofSection": render_proof_section(data, extra_tokens),
         "relatedCards": render_related_section(
             templates["related_card"], data, all_snippets, locale, extra_tokens
         ),

templates/slug-template.html

@@ -214,6 +214,8 @@ <h1>{{title}}</h1>
       </div>
     </section>
 
+{{proofSection}}
+
     <section class="related">
       <div class="section-label">{{sections.relatedPatterns}}</div>
       <div class="related-grid">

translations/strings/ar.yaml

@@ -25,6 +25,8 @@ sections:
   jdkSupport: دعم JDK
   howItWorks: كيف يعمل
   relatedDocs: توثيق ذو صلة
+  proof: إثبات
+  proofLink: عرض كود الإثبات
   relatedPatterns: أنماط ذات صلة
 filters:
   show: "عرض:"

translations/strings/de.yaml

@@ -27,6 +27,8 @@ sections:
   jdkSupport: JDK-Unterstützung
   howItWorks: Wie es funktioniert
   relatedDocs: Zugehörige Dokumentation
+  proof: Beweis
+  proofLink: Beweisquelle ansehen
   relatedPatterns: Verwandte Muster
 filters:
   show: 'Anzeigen:'

translations/strings/en.yaml

@@ -27,6 +27,8 @@ sections:
   jdkSupport: JDK Support
   howItWorks: How it works
   relatedDocs: Related Documentation
+  proof: Proof
+  proofLink: View proof source
   relatedPatterns: Related patterns
 filters:
   show: 'Show:'

translations/strings/es.yaml

@@ -27,6 +27,8 @@ sections:
   jdkSupport: Soporte JDK
   howItWorks: Cómo funciona
   relatedDocs: Documentación Relacionada
+  proof: Prueba
+  proofLink: Ver código de prueba
   relatedPatterns: Patrones relacionados
 filters:
   show: 'Mostrar:'

translations/strings/fr.yaml

@@ -27,6 +27,8 @@ sections:
   jdkSupport: Support JDK
   howItWorks: Comment ça fonctionne
   relatedDocs: Documentation Associée
+  proof: Preuve
+  proofLink: Voir la preuve source
   relatedPatterns: Patterns associés
 filters:
   show: 'Afficher :'

translations/strings/it.yaml

@@ -27,6 +27,8 @@ sections:
   jdkSupport: Supporto JDK
   howItWorks: Come funziona
   relatedDocs: Documentazione Correlata
+  proof: Prova
+  proofLink: Vedi sorgente di prova
   relatedPatterns: Pattern correlati
 filters:
   show: 'Mostra:'

translations/strings/ja.yaml

@@ -25,6 +25,8 @@ sections:
   jdkSupport: JDKサポート
   howItWorks: 仕組み
   relatedDocs: 関連ドキュメント
+  proof: 証明
+  proofLink: 証明ソースを見る
   relatedPatterns: 関連パターン
 filters:
   show: '表示:'

translations/strings/ko.yaml

@@ -25,6 +25,8 @@ sections:
   jdkSupport: JDK 지원
   howItWorks: 동작 원리
   relatedDocs: 관련 문서
+  proof: 증명
+  proofLink: 증명 소스 보기
   relatedPatterns: 관련 패턴
 filters:
   show: '표시:'

translations/strings/pl.yaml

@@ -26,6 +26,8 @@ sections:
   jdkSupport: Wsparcie JDK
   howItWorks: Jak to działa
   relatedDocs: Powiązana dokumentacja
+  proof: Dowód
+  proofLink: Zobacz źródło dowodu
   relatedPatterns: Powiązane wzorce
 filters:
   show: 'Pokaż:'

translations/strings/pt-BR.yaml

@@ -26,6 +26,8 @@ sections:
   jdkSupport: Suporte JDK
   howItWorks: Como funciona
   relatedDocs: Documentação Relacionada
+  proof: Prova
+  proofLink: Ver código de prova
   relatedPatterns: Padrões relacionados
 filters:
   show: 'Mostrar:'

translations/strings/tr.yaml

@@ -26,6 +26,8 @@ sections:
   jdkSupport: JDK Desteği
   howItWorks: Nasıl çalışır
   relatedDocs: İlgili Belgeler
+  proof: Kanıt
+  proofLink: Kanıt kaynağını görüntüle
   relatedPatterns: İlgili desenler
 filters:
   show: 'Göster:'

translations/strings/zh-CN.yaml

@@ -26,6 +26,8 @@ sections:
   jdkSupport: JDK 支持
   howItWorks: 工作原理
   relatedDocs: 相关文档
+  proof: 证明
+  proofLink: 查看证明源码
   relatedPatterns: 相关模式
 filters:
   show: '显示：'