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 = "b2af6ee923fac9d60bd4e2fdce27b11287cc614f"}

print_docs.py

@@ -321,6 +321,16 @@ 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
+
 def load_json():
   try:
     with open('export.json', 'r', encoding='utf-8') as f:
@@ -333,6 +343,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,17 @@ 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;
+}
+

templates/decl.j2

@@ -32,6 +32,29 @@
 
 {{ 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 }}
+        </div>
+
+        <div class="translation_qs">
+            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>
+            Does this translation look correct? <a href="">Yes</a> | <a href = "">No</a> 
+        </div>
+    </div>
+
+
+</details> 
+
+{% endif %}
+
 {% if decl.equations | length %}
     <details>
         <summary>Equations</summary>