display automatic translations to informal math

leanpkg.toml

@@ -1,8 +1,8 @@
 [package]
 name = "."
 version = "0.1"
-lean_version = "leanprover-community/lean:3.35.1"
+lean_version = "leanprover-community/lean:3.45.0"
 path = "src"
 
 [dependencies]
-mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "77ba0c4160793de8a824461128c57ca394792143"}
+mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "54c4c2220ab3b6a655e8d76c5c167a7d3d08dc9c"}

nav.js

@@ -246,3 +246,52 @@ for (const elem of document.getElementsByClassName('gh_link')) {
     }
   }
 }
+
+// Informal Statement feedback form handler
+// -------
+
+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 name = event.submitter.getAttribute('name')
+        const value = event.submitter.getAttribute('value')
+        url.searchParams.set(name, value)
+        if (value === 'no') {
+          feedbackForm.textContent = "Please correct the text below:"
+          editForm.removeAttribute('style')
+          const edit = await new Promise((resolve, reject) => {
+            editForm.addEventListener('submit', event => {
+              event.preventDefault()
+              resolve(ta.value)
+            })
+          });
+          url.searchParams.set('edit', edit)
+          editForm.remove()
+        }
+        feedbackForm.textContent = "Sending..."
+
+        const response = await fetch(url, { method: 'POST' })
+        if (response.ok) {
+          feedbackForm.textContent = "Thanks for your feedback!"
+        } else {
+          const txt = await response.text()
+          throw new Error(`Bad response: ${txt}`)
+        }
+      } catch (err) {
+        feedbackForm.textContent = `Error: ${err.message}`
+      }
+    })
+  }
+})

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,23 @@ 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']
+      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 +351,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

@@ -697,3 +697,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/decl.j2

@@ -32,6 +32,35 @@
 
 {{ decl.doc_string | convert_markdown }}
 
+{% if decl.informal_statement %}
+
+<details open>
+    <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>