Add giscus-based comments and reactions

site/src/css/giscus-custom.css

@@ -0,0 +1,42 @@
+/* hides not used reactions */
+.gsc-reactions .gsc-emoji-button:nth-child(3),
+.gsc-reactions .gsc-emoji-button:nth-child(4),
+.gsc-reactions .gsc-emoji-button:nth-child(5),
+.gsc-reactions .gsc-emoji-button:nth-child(7),
+.gsc-reactions .gsc-emoji-button:nth-child(8) { display: none; }
+
+/* paints over giscus reaction name (+1/-1/Love) with a same-colored rectangle */
+.gsc-reactions .gsc-reactions-popover p.overflow-hidden {
+  position: relative;          /* establishes a positioning context */
+}
+.gsc-reactions .gsc-reactions-popover p.overflow-hidden::after {
+  content: "Pick your reaction";
+  position: absolute;
+  inset: 0;                    /* stretches to cover the entire <p> */
+  background: var(--color-canvas-overlay, #fff);  /* same color as popup background */
+  color: var(--color-fg-muted, #656d76);
+  white-space: nowrap; overflow: hidden; text-overflow: ellipsis;
+}
+/* overwrites the reaction name in the reaction box using ::after */
+.gsc-reactions .gsc-reactions-popover:has(.gsc-emoji-button:nth-child(1):hover) p.overflow-hidden::after,
+.gsc-reactions .gsc-reactions-popover:has(.gsc-emoji-button:nth-child(1):focus) p.overflow-hidden::after { content: "True"; }
+.gsc-reactions .gsc-reactions-popover:has(.gsc-emoji-button:nth-child(2):hover) p.overflow-hidden::after,
+.gsc-reactions .gsc-reactions-popover:has(.gsc-emoji-button:nth-child(2):focus) p.overflow-hidden::after { content: "False"; }
+.gsc-reactions .gsc-reactions-popover:has(.gsc-emoji-button:nth-child(6):hover) p.overflow-hidden::after,
+.gsc-reactions .gsc-reactions-popover:has(.gsc-emoji-button:nth-child(6):focus) p.overflow-hidden::after { content: "Like"; }
+
+
+/* Rename the reactions box as "Cast your vote" + emoji meaning */
+.gsc-reactions .gsc-reactions-count { font-size: 0; }
+.gsc-reactions .gsc-reactions-count::before {
+  content: "Cast Your Vote";
+  display: block;
+  font-size: 1rem;
+}
+.gsc-reactions .gsc-reactions-count::after {
+  content: "👍 = True\2002👎 = False\2002❤️ = I like this conjecture";
+  display: block;
+  font-size: 0.8rem;
+  font-weight: normal;
+  padding-left: 2rem;
+}

site/src/css/style.css

@@ -91,6 +91,7 @@
 html {
   font-size: 18px;
   scroll-behavior: smooth;
+  scroll-padding-top: var(--nav-height);
 }
 
 body {
@@ -111,7 +112,7 @@ img { max-width: 100%; }
 ul, ol { list-style: none; }
 
 /* ---- Utility ---- */
-.container { max-width: var(--max-width); margin: 0 auto; padding: 0 1.5rem; }
+.container { width: 100%; max-width: var(--max-width); margin: 0 auto; padding: 0 1.5rem; }
 .visually-hidden { position: absolute; width: 1px; height: 1px; overflow: hidden; clip: rect(0,0,0,0); }
 
 /* ============================================================

site/src/js/giscus_voting.js

@@ -0,0 +1,81 @@
+/**
+ * giscus_voting.js — giscus-backed voting system.
+ *
+ * Votes are stored as reactions (emojis) on the theorem page.
+ */
+
+'use strict';
+
+(function () {
+
+  // ---------------------------------------------------------------------------
+  // Apply giscus theme (filter emojis + reaction labels)
+  // ---------------------------------------------------------------------------
+  function applyGiscusTheme() {
+    // Reaction key order from giscus's Reactions object (matches GitHub API order)
+    var REACTION_ORDER = ['THUMBS_UP', 'THUMBS_DOWN', 'LAUGH', 'HOORAY', 'CONFUSED', 'HEART', 'ROCKET', 'EYES'];
+    var REACTION_LABELS = { THUMBS_UP: 'True', THUMBS_DOWN: 'False', HEART: 'Likes' };
+
+    var base = document.documentElement.dataset.base || '';
+    fetch(base + '/assets/css/giscus-custom.css')
+      .then(function(r) { if (!r.ok) return Promise.reject(); return r.text(); })
+      .then(function(baseCss) {
+        var currentIframe = null;
+        var lastReactions = {};  // { THUMBS_UP: {count, viewerHasReacted}, ... }
+
+        function buildCss() {
+          var labelCss = '';
+          var pos = 0;
+          for (var i = 0; i < REACTION_ORDER.length; i++) {
+            var key = REACTION_ORDER[i];
+            var group = lastReactions[key];
+            if (group && group.count > 0) {
+              pos++;
+              var label = REACTION_LABELS[key];
+              if (label) {
+                labelCss += '.gsc-reactions .gsc-direct-reaction-button:nth-child(' + pos + ') .gsc-social-reaction-summary-item-count::before{content:"' + label + ' ";}';
+              } else {
+                labelCss += '.gsc-reactions .gsc-direct-reaction-button:nth-child(' + pos + '){display:none;}';
+              }
+            }
+          }
+          return baseCss + labelCss;
+        }
+
+        function sendTheme() {
+          if (!currentIframe) return;
+          var giscusOrigin = new URL(currentIframe.src).origin;
+          var css = '@import url("' + giscusOrigin + '/themes/light.css");' + buildCss();
+          currentIframe.contentWindow.postMessage(
+            { giscus: { setConfig: { theme: 'data:text/css,' + encodeURIComponent(css) } } },
+            '*'
+          );
+        }
+
+        // Re-apply with correct labels whenever reaction counts change
+        window.addEventListener('message', function(event) {
+          if (typeof event.data !== 'object' || !event.data.giscus) return;
+          var discussion = event.data.giscus.discussion;
+          if (!discussion || !discussion.reactions) return;
+          lastReactions = discussion.reactions;
+          sendTheme();
+        });
+
+        function waitAndApply() {
+          window.addEventListener('message', function onReady(event) {
+            if (typeof event.data !== 'object' || !event.data.giscus || !event.data.giscus.resizeHeight) return;
+            window.removeEventListener('message', onReady);
+            currentIframe = document.querySelector('iframe.giscus-frame');
+            if (!currentIframe) return;
+            sendTheme();
+            // Re-apply if the iframe reloads (e.g. after sign-out)
+            currentIframe.addEventListener('load', waitAndApply, { once: true });
+          });
+        }
+
+        waitAndApply();
+      });
+  }
+
+  applyGiscusTheme();
+})();

site/src/js/theorem.js

@@ -38,6 +38,8 @@ async function init() {
   }
 
   document.title = `${theorem.displayTheorem} — Formal Conjectures`;
+  const ogTitle = document.querySelector('meta[property="og:title"]');
+  if (ogTitle) ogTitle.content = theorem.theorem;
   const siblings = data.conjectures.filter(c => c.module === theorem.module);
   const verso = data.versoFragments || { moduleDocs: {}, constLinks: {} };
   const contributors = data.contributors?.[theorem.githubPath] || [];
@@ -542,6 +544,7 @@ function renderDetail(theorem, siblings, verso, contributors) {
       <a href="${FC.escapeHTML(theorem.githubUrl)}" class="btn btn-outline" target="_blank" rel="noopener">
         View on GitHub ↗
       </a>
+      <a href="${_base}/about/#comments" class="btn btn-outline">About comments and votes</a>
     </nav>
   `;
 

site/src/templates/about.html

@@ -112,6 +112,23 @@ <h2>A note on accuracy</h2>
         and plans to leverage automated tools to help identify potential misformalisations.
       </p>
 
+      <h2 id="comments">Comments and votes</h2>
+      <p>
+        Each theorem page includes a comment section backed by
+        <a href="https://giscus.app" target="_blank" rel="noopener">Giscus</a>
+        and GitHub Discussions.
+      </p>
+      <p>
+        <b>Comments and votes are public.</b>
+        Any reaction (👍 True, 👎 False, ❤️ Like) or comment you leave is
+        stored in a publicly visible GitHub Discussion and is
+        associated with your GitHub username. Anyone can see who reacted
+        and what they wrote.
+      </p>
+      <p>
+        Comments and votes require a GitHub account.
+      </p>
+
       <h2>Licensing</h2>
       <p>
         All software is licensed under

site/src/templates/theorem.html

@@ -4,7 +4,12 @@
   <meta charset="UTF-8">
   <meta name="viewport" content="width=device-width, initial-scale=1.0">
   <title>Theorem — Formal Conjectures</title>
-  <meta name="description" content="Theorem detail page for the Formal Conjectures repository.">
+  <meta name="description" content="The emoji reactions on this post carry special meaning:
+ * 👍: I believe the corresponding conjecture is True
+ * 👎: I believe the corresponding conjecture is False
+ * ❤️: I like the conjecture">
+  <meta property="og:title" content="">
+  <meta name="giscus:backlink" content="#">
   <link rel="preload" href="/assets/fonts/LibertinusSans-Regular.woff2" as="font" type="font/woff2" crossorigin>
   <link rel="stylesheet" href="/assets/css/style.css">
   <link rel="icon" href="/assets/img/formal_conjectures_logo.svg" type="image/svg+xml">
@@ -40,6 +45,40 @@
   </div>
 </main>
 
+<div class="container">
+<script>
+  /* Set og:title and description first line using the page URL, before loading giscus. */
+  (function() {
+    var name = new URLSearchParams(location.search).get('name') || '';
+    var ogTitle = document.querySelector('meta[property="og:title"]');
+    if (ogTitle && name) ogTitle.content = name;
+
+    var url = new URL(location.href);
+    url.searchParams.delete('giscus');
+    url.hash = '';
+    var cleanHref = url.toString();
+
+    var desc = document.querySelector('meta[name="description"]');
+    if (desc) desc.content = 'Discussion page for ' + cleanHref + '.\n' + desc.content;
+  })();
+</script>
+<script src="https://giscus.app/client.js"
+        data-repo="google-deepmind/formal-conjectures"
+        data-repo-id="R_kgDOOogmBw"
+        data-category="Problems"
+        data-category-id="DIC_kwDOOogmB84C_EMz"
+        data-mapping="og:title"
+        data-strict="0"
+        data-reactions-enabled="1"
+        data-emit-metadata="1"
+        data-input-position="bottom"
+        data-theme="light"
+        data-lang="en"
+        crossorigin="anonymous"
+        async>
+</script>
+</div>
+
 <footer class="site-footer">
   <div class="container site-footer__inner">
     <span>Formal Conjectures &mdash; Apache 2.0 / CC-BY 4.0</span>
@@ -52,7 +91,7 @@
 </footer>
 
 <script src="/assets/js/main.js"></script>
-<!-- <script src="/assets/js/voting.js"></script> -->
+<script src="/assets/js/giscus_voting.js"></script>
 <script src="/assets/js/theorem.js"></script>
 </body>
 </html>