-
Notifications
You must be signed in to change notification settings - Fork 5
/
Copy pathtodo.txt
124 lines (121 loc) · 6.88 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
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
- add a filter by source file to the explorer.
- add possibility to reorder mm files in the context
- add a test for disj in MM_asrt_syntax_tree.unify()
- rename tabs by Alt+click
- docs:
- debug bottom-up proof for:
hyp1: |- ( ph -> A e. RR )
hyp2: |- ( ph -> B e. RR )
hyp3: |- ( ph -> K e. RR )
qed: |- ( ph -> ( ( K x. A ) + -u ( K x. B ) ) = ( ( K x. A ) - ( K x. B ) ) )
- Check why "resetNestingLevel" and "allLabels" appear in the exported JSON.
- Embed the "current version of Metamath-lamp" in the exported JSON
https://github.com/expln/metamath-lamp/issues/128
- implement text comments for statements
- fix a bug: set "auto unify all" = true. Update settings - an error occurs.
- check where MM_context and MM_parser may throw an exception
- add a few options to the proof tree explorer: show essentials only, show unproved steps only, show number of unproved steps for each source.
- implement "a macro is running" mode when popups are not appearing (so the screen is not blinking)
- there should be quick access to frequently used macros from the buttons bar
- the macro display name should be a functions of the global context
- fix a bug: completed proof should not be shown in macros.
- write tests for example macros
- write tests for different cases of "inline proof"
- simplify actUnify() in MM_cmp_editors.
- minimize compressed proof by placing the least used labels in the beginning
- try to implement proof minimization https://github.com/metamath/set.mm/pull/3790#issuecomment-1913042661
- 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.
- 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
- review usages of "alias", it may be empty.
- implement a builder of statements.
- check if adding a cache to proveStmtBottomUp() (for getParents) improves performance.
- 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.
- 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 out statements so they are present in the editor but don't participate in the proof
- 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)
DONE:
- fix a bug: in eliminate variables rename labels if there were merges of duplicates.
- show security warning in the macros dialog.
- implement caching in the API.
- allow to set args1 == args0 fast on UI.
- improve performance of "Unify All".
- update syntax tree structure in fragment transforms. Also add possibility to use only the final result.
- 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.
- 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.
- the proof viewer fails for incorrect proofs
https://github.com/expln/metamath-lamp/issues/184
- implement pagination in MM_cmp_pe_frame_full.res
- autofocus label selector after scope is set to StopBefore or StopAfter
- add "About" page.
https://github.com/expln/metamath-lamp/issues/72