Skip to content
This repository was archived by the owner on Aug 15, 2025. It is now read-only.

display automatic translations to informal math #168

Open
robertylewis wants to merge 22 commits into
base: master
Choose a base branch
from
Open

display automatic translations to informal math #168

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
7cec640
bump mathlib version
robertylewis Jul 20, 2022
7ff6709
display informal translations
robertylewis Jul 21, 2022
5328ddd
outdated css
robertylewis Jul 22, 2022
d46cddf
Update templates/decl.j2
robertylewis Jul 22, 2022
3252777
change feedback links to form
EdAyers Jul 30, 2022
411bfb0
fix: edit style
EdAyers Aug 2, 2022
03443f8
Add translation form handler.
EdAyers Aug 2, 2022
6624d54
Support feedback edit
EdAyers Aug 3, 2022
6c05dba
hack to escape < in mathjax
robertylewis Aug 3, 2022
42c2a9d
Send feedback as soon as user clicks No
EdAyers Aug 3, 2022
f9108f2
Fix double-counting ratings
EdAyers Aug 3, 2022
4b847fa
Add toggle for opening or closing all informal statement panels
EdAyers Aug 5, 2022
7470cdc
fix localstorage
EdAyers Aug 5, 2022
935ca19
Apply suggestions from code review
EdAyers Aug 8, 2022
bbc1dfb
Refactor localstorage code for informalopen
EdAyers Aug 8, 2022
93a69c5
Informal statement details are closed by default
EdAyers Aug 8, 2022
b31b053
semicolons everywhere
EdAyers Aug 8, 2022
376fba4
more semicolons
EdAyers Aug 8, 2022
46cc148
Merge branch 'master' into display-informal
robertylewis Aug 10, 2022
846af1b
fix merge
robertylewis Aug 10, 2022
f8c1b50
lazy loading of math
robertylewis Aug 10, 2022
bab70a7
change configuration options header
robertylewis Aug 10, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions leanpkg.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"}
13 changes: 13 additions & 0 deletions print_docs.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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']
Expand Down
36 changes: 36 additions & 0 deletions style.css
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -697,3 +697,39 @@ a:hover {
margin-top: 2em;
margin-bottom: 2em;
}

.informal_statement {
margin-top: 1em;
}

.informal_statement .explain {
color:var(--link-color);
}

.informal_statement .explain .tooltiptext {
visibility: hidden;
width: 120px;
background-color: black;
color: #fff;
text-align: center;
padding: 5px 0;
border-radius: 6px;

/* Position the tooltip text - see examples below! */
top: -5px;
left: 105%;

}
Comment thread
robertylewis marked this conversation as resolved.
Outdated
Comment thread
robertylewis marked this conversation as resolved.
Outdated

.informal_statement .statement, .informal_statement .translation_qs {
margin-left: 2ch;
}

.informal_statement .translation_qs {
color:gray;
}

/* Show the tooltip text when you mouse over the tooltip container */
.informal_statement .explain:hover .tooltiptext {
visibility: visible;
}
Comment thread
robertylewis marked this conversation as resolved.
Outdated
Binary file added tagged_nl2.json.gz
View file
Open in desktop
Binary file not shown.
23 changes: 23 additions & 0 deletions templates/decl.j2
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 }}
Comment thread
robertylewis marked this conversation as resolved.
Outdated
</div>
Comment on lines +41 to +43
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser Aug 3, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm worried the mathjax rendering is going to have quite a large impact on page load times. Could we maybe:

  • Defer mathjax rendering of .informal_statement until the details is expanded
  • Put a "expand informal math" setting in the sidebar next to the color scheme setting, so that users can opt to collapse everything by default and get the associated performance boost.

Copy link
Copy Markdown
Member Author

@robertylewis robertylewis Aug 3, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the details should be collapsed by default, not for performance but because the translations are misleadingly sketchy:

Right now I put it in a <details> menu, expanded by default to make browsing this demo easier. I think they should be collapsed by default in production, at least until the translations improve.

But a toggle also sounds like a good idea.

Do you know how to defer the rendering?

Copy link
Copy Markdown
Member

@eric-wieser eric-wieser Aug 4, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There's a (possibly outdated) question about deferring here: https://stackoverflow.com/a/27952213/102441

Copy link
Copy Markdown
Member

@eric-wieser eric-wieser Aug 4, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This page in the documentation also seems relevant.

Enabling Lazy Typesetting would also be a reasonable option.


<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>
Expand Down
⚡