display automatic translations to informal math

nav.js

@@ -246,3 +246,91 @@ for (const elem of document.getElementsByClassName('gh_link')) {
     }
   }
 }
+
+// Informal Statement feedback form handler
+// -------
+
+/** Same as `fetch` but throws an error if it's a bad response. */
+async function fetchGood(...args) {
+  const response = await fetch(...args);
+  if (!response.ok)  {
+    const txt = await response.text()
+    throw new Error(`Bad response: ${txt}`)
+  }
+}
+
+/** Handler for clicking feedback buttons in informal statements. */
+window.addEventListener('load', _ => {
+  for (const translationDiv of document.querySelectorAll('.translation_qs')) {
+    const declName = translationDiv.getAttribute('data-decl');
+    if (!declName) {
+      console.error('no data-decl on translation_qs');
+    }
+    const feedbackForm = translationDiv.querySelector('.informal_statement_feedback');
+    const editForm = translationDiv.querySelector('.informal_statement_edit');
+    const ta = editForm.querySelector('textarea');
+    const url = new URL(feedbackForm.getAttribute('action'));
+    url.searchParams.set('decl', declName);
+    url.searchParams.set('statement', ta.value);
+    feedbackForm.addEventListener('submit', async event => {
+      event.preventDefault();
+      try {
+        const value = event.submitter.getAttribute('value');
+        url.searchParams.set('rate', value);
+        feedbackForm.textContent = "Sending...";
+        await fetchGood(url, { method: 'POST' });
+        if (value === 'no') {
+          feedbackForm.textContent = "Thanks for your feedback! Optionally, please help us out by submitting a corrected statement: ";
+          editForm.removeAttribute('style');
+          const edit = await new Promise((resolve, reject) => {
+            editForm.addEventListener('submit', event => {
+              event.preventDefault();
+              resolve(ta.value);
+            });
+          });
+          url.searchParams.delete('rate'); // don't double-count the rating.
+          url.searchParams.set('edit', edit);
+          editForm.remove();
+          feedbackForm.textContent = "Sending...";
+          await fetchGood(url, { method: 'POST' });
+        }
+        feedbackForm.textContent = "Thanks for your feedback!"
+      } catch (err) {
+        feedbackForm.textContent = `Error: ${err.message}`;
+      }
+    })
+  }
+})
+
+const INFORMAL_OPEN_ID = 'informal_statement_open';
+
+function getInformalOpen() {
+  const item = localStorage.getItem(INFORMAL_OPEN_ID);
+  if (!item) {
+    return false; // default is closed
+  } else {
+    return JSON.parse(item);
+  }
+}
+
+function updateInformalOpen(state) {
+  if (state !== undefined) {
+    localStorage.setItem(INFORMAL_OPEN_ID, JSON.stringify(state));
+  } else {
+    state = getInformalOpen();
+  }
+  const details = document.querySelectorAll('.informal_statement_details');
+  for (const detail of details) {
+    detail.open = state;
+  }
+}
+
+window.addEventListener('load', _ => {
+  updateInformalOpen();
+  const checkbox = document.querySelector('#informal-open');
+  checkbox.checked = getInformalOpen();
+  checkbox.addEventListener('change', e => {
+    const value = checkbox.checked;
+    updateInformalOpen(value);
+  });
+});

print_docs.py

@@ -25,6 +25,7 @@
 from pathlib import Path
 from typing import NamedTuple, List, Optional
 import sys
+import hashlib
 
 import mistletoe
 from mistletoe_renderer import CustomHTMLRenderer, PlaintextSummaryRenderer
@@ -321,6 +322,25 @@ def trace_deps(file_map):
   print(f"trace_deps: Processed {n_ok} / {n} dependency links")
   return graph
 
+
+def add_informal_statements_to_decls(informal, file_map):
+  for file in file_map:
+    for decl in file_map[file]:
+      informal_statement = ""
+      if decl['kind'] == 'theorem':
+        informal_decl = informal.get(decl['name'], None)
+        if informal_decl is not None and decl['args'] == informal_decl['args'] and decl['type'] == informal_decl['type']:
+          informal_statement = informal_decl['informal_statement']
+      # a hack to avoid `$a<b$`` being interpreted as html
+      informal_statement = informal_statement.replace('<', '< ')
+      decl['informal_statement'] = informal_statement
+      # create a hash of the given informal statement string
+      # there is no need for it to be a cryptographic hash, better to use xxhash but requires dependency
+      # we can't use builtin `hash` because not stable across executions.
+      m = hashlib.md5()
+      m.update(informal_statement.encode())
+      decl['informal_statement_digest'] = m.hexdigest()
+
 def load_json():
   try:
     with open('export.json', 'r', encoding='utf-8') as f:
@@ -333,6 +353,9 @@ def load_json():
       print(raw)
     raise
   file_map, loc_map = separate_results(decls['decls'])
+  with gzip.open('tagged_nl2.json.gz') as tagged_nl:
+    translations = json.load(tagged_nl)
+  add_informal_statements_to_decls(translations, file_map)
   for entry in decls['tactic_docs']:
     if len(entry['tags']) == 0:
       entry['tags'] = ['untagged']

style.css

@@ -377,13 +377,18 @@ nav {
     font-size: inherit;
 }
 
-#color-theme-switcher {
+#settings form {
     display: flex;
     justify-content: space-between;
     padding: 0 2ex;
     flex-flow: row wrap;
 }
 
+#settings input[type="checkbox"] {
+    margin-left: 5px;
+    margin-top: 5px;
+}
+
 /* custom radio buttons for dark/light switch */
 #color-theme-switcher input {
     -webkit-appearance: none;
@@ -697,3 +702,39 @@ a:hover {
     margin-top: 2em;
     margin-bottom: 2em;
 }
+
+.informal_statement {
+    margin-top: 1em;
+}
+
+
+.informal_statement .statement, .informal_statement .translation_qs {
+    margin-left: 2ch;
+}
+
+.informal_statement .translation_qs {
+    color:gray;
+}
+
+.informal_statement_feedback {
+  display: inline;
+}
+
+.informal_statement_feedback button {
+    background: none!important;
+    border: none;
+    padding: 0!important;
+    font-family: inherit;
+    font-size: inherit;
+    color: var(--link-color);
+    cursor: pointer;
+}
+
+.informal_statement_feedback button:hover {
+  text-decoration: underline
+}
+
+.informal_statement_edit textarea {
+    font-size: 1rem;
+    width: 100%;
+}

templates/base.j2

@@ -71,6 +71,7 @@ MathJax = {
         ignoreHtmlClass: 'tex2jax_ignore',
         processHtmlClass: 'tex2jax_process',
     },
+    loader: {load: ['ui/lazy']}
 };
 
 siteRoot = "{{ site_root }}";

templates/decl.j2

@@ -32,6 +32,35 @@
 
 {{ decl.doc_string | convert_markdown }}
 
+{% if decl.informal_statement %}
+
+<details class="informal_statement_details">
+    <summary>Informal translation</summary>
+
+    <div class="informal_statement">
+        <div class="statement">
+            {{ decl.informal_statement | convert_markdown }}
+        </div>
+
+        <div class="translation_qs" data-decl="{{decl.name}}">
+            This translation to informal mathematics is automatically generated and should NOT be trusted!
+            The translation is a <a href="">beta feature powered by OpenAI's Codex API</a>.
+            <br>
+            <form class="informal_statement_feedback" action="https://lean-chat-server.deno.dev/doc-gen?digest={{decl.informal_statement_digest}}" method="post">
+              <span class="status" >Does this translation look correct?</span>
+              <button type="submit" name="rate" value="yes">Yes</button>
+              <button type="submit" name="rate" value="no">No</button>
+            </form>
+            <form class="informal_statement_edit" style="display: none;" action="#">
+                <textarea name="statement" rows="6">{{decl.informal_statement}}</textarea>
+                <button type="submit">Submit</button>
+            </form>
+        </div>
+    </div>
+</details>
+
+{% endif %}
+
 {% if decl.equations | length %}
     <details>
         <summary>Equations</summary>

templates/navbar.j2

@@ -36,7 +36,7 @@
 
 <div id="settings">
 
-<h3>Color scheme</h3>
+<h3>Settings</h3>
 <form id="color-theme-switcher">
     <label for="color-theme-dark">
         <input type="radio" name="color_theme" id="color-theme-dark" value="dark" autocomplete="off">dark</label>
@@ -46,4 +46,11 @@
         <input type="radio" name="color_theme" id="color-theme-light" value="light" autocomplete="off">light</label>
 </form>
 
+<form>
+  <label for="informal-open">
+    <input type="checkbox" id="informal-open">
+    expand informal translations
+  </label>
+</form>
+
 </div>