forked from expln/metamath-lamp
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathtodo.txt
90 lines (89 loc) · 5.01 KB
/
todo.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
- export in uncompressed-essential and compressed-essential formats
- remember last selected scope for each source
- add "Search" tab
- when automerging two stmts, if both have same jstf then select the upper one (write a test to check bad references before duplications)
- extract wrk logic from MM_cmp_pe_frame_full and cover it with tests.
- Try: in proofNode.parents use an array before some threshold and a hashMap after the threshold.
- improve performance of the fragment selector in the cmp_pe_full by reusing existing proof.
- make "compact mode" and "small buttons" default on mobile.
- remove selector from the url added by the explorer. Steps to reproduce:
load set.mm, find r19.12 in the explorer, open r19.12 to see its proof - error in the console:
DOMException: Failed to execute 'querySelectorAll' on 'Document': '#tbl-r19.12 .step' is not a valid selector.
- freeze pagination in the explorer
- fix a bug:
when I was proving "cotval-hyp" one label became uneditable.
- optimize re-rendering for all tabs.
- in the bottom up prover use existing vars together with new vars
- move some dependencies to devDependencies.
- review usages of "alias", it may be empty.
- implement a builder of statements.
- add "About" page.
- check if adding a cache to proveStmtBottomUp() (for getParents) improves performance.
- in the "search" dialog, in the pattern text field, replace variables with their types.
- provide more info on substitution found when "Could not match essential hypothesis #1"
- write a test for allowNewDisjForExistingVars
- add an int test when a hyp is used in a bottom-up proof being applied.
- proof tree improvements:
- pass error icon from src to all unproved children
- sort srcs by var type, hyp, asrt
- filter by asrt, min number of srcs
- In prove bottom up, similar to checks for var types and hyps, also check assertions without eHyps for node.dist==maxDepth.
- write tests for collecting debug info
- before merging of statements check if some statements should be moved up because they are referenced by above statements and don't merge in that case.
- autofocus label selector after scope is set to StopBefore or StopAfter
- in cmp_search use array2.slice and store idx in the rendered elem the same way as in cmp_bottom_up
- add an int test with few hypotheses.
- apply colors to search results, substitutions.
- write tests for both versions of verifyDisjoints (in MM_subs and MM_wrk_editor)
- add possibility to comment statements
- make error messages more informative: add the statement caused the error (for example in "variables" or in justifications).
- write tests for editorState -> proofTree -> editorState.
- correct methods related to movement of statements, they became incorrect after automatic reordering.
- use Async/Await.
- precalculate number of combinations (store in an array)
- use uncurried functions everywhere
- replace a[i] with a->Js_array2.unsafe_get(i), or open Belt and replace with Option.getExn
DONE:
- print a proof table in the "show proof" dialog (with possibility to hide floatings).
- Click on section name to edit it.
- fix a bug:
1. open visualization
2. delete jstf - visualization disappears
3. unify all
AR: visualization is not showing
ER: visualization is showing
- don't re-render cmp_user_stmt when it is not necessary.
- hide "plus" button on nodes without children in the proof tree.
- store last selected file source type.
- add "terminate" button to the file web loader.
- add "restore defaults" buttons to Settings.
- move word "justification" outside the paper.
- hide delete button for an empty justification.
- improve performance of MM_cmp_proof_node
- error messages for some specific cases
* number of args doesn't match
* could not prove type of floating
* missing disjoint
* failing disjoint
- tooltip: To start a new line in a multiline text editor press Shift+Enter
- load *.mm files from metamath.org
- Make new stmt prefix configurable.
- fix a bug:
1) load an MM file, apply changes;
2) load same file in the same file selector - nothing happens.
- prefix for new statements
- remove tabs with non-existent frames after ctx reload.
- show visualization for statements marked with '~'.
- fix a bug: goal is re-defined but the statement is not marked with red background.
- fix a bug: pressing Enter in the explorer filters on mobile doesn't apply filters.
- fix a bug: not possible to select ( ph -> ps ) part in the statement below (in the explorer):
|- ( ( ph -> ps ) -> ( ph -> ch ) )
- add vertical-align=top to proof tables in the explorer
- Specify in the guide the version of mm-lamp which it was written for
- implement table view in the editor.
- add onEnter and onEscape wherever possible.
- allow editing of settings in the temp mode
- check if copy to clipboard should return a promise
- do not repeat references to hypotheses in proof tables, example - dimkerim has 279 rows in mm-lamp and 270 on https://us.metamath.org/mpeuni/dimkerim.html
- add "items per page" to PE index.
- Automatically create correct labels for hypotheses.