Add ability to renumber steps. Fixes #18

david-a-wheeler commented 1 year ago

Here's a modification to metamath-lamp that implements issue #18. It's not a lot of code, but it's really helpful.

This is my first time writing code in Rescript, and I haven't used OCaml in a long time either. But I tested this on a variety of files (including all 4 JSON files in the guide) and it seems to work without issue.

Try it, I think you'll like it.

david-a-wheeler commented 1 year ago

You'll notice this is my second PR on this issue. Sorry about that. I did start my implementation against "develop", but when I create the PR I forgot to set it "develop" & it create a huge change against master.

This PR is a small change against the develop branch.

david-a-wheeler commented 1 year ago

P.S. I made the menu item "Renumber numbered steps", not the simpler "Renumber steps", because I wanted to hint to the user that this only renumbers the steps with number labels.

t's not very obvious in the UI that you can rename any step to an alphanumeric instead of just numerics - wording the entry this way hints at functionality they might not guess otherwise. Adding this word helps discoverability.

expln commented 1 year ago

This is my first time writing code in Rescript, and I haven't used OCaml in a long time either.

No worries, your code looks great.

But I tested this on a variety of files (including all 4 JSON files in the guide) and it seems to work without issue.

Manual testing is good. But we have to cover such functionality with unit tests too. I left a review comment regarding this.

Try it, I think you'll like it.

Sure, this is cool!

You'll notice this is my second PR on this issue. Sorry about that. I did start my implementation against "develop", but when I create the PR I forgot to set it "develop" & it create a huge change against master.

No worries :)

P.S. I made the menu item "Renumber numbered steps", not the simpler "Renumber steps", because I wanted to hint to the user that this only renumbers the steps with number labels. t's not very obvious in the UI that you can rename any step to an alphanumeric instead of just numerics - wording the entry this way hints at functionality they might not guess otherwise. Adding this word helps discoverability.

Good idea. I agree.

expln commented 1 year ago

we have to cover such functionality with unit tests too. I left a review comment regarding this.

Unfortunately you will not find this comment. I wrote a big comment with few explanations related to the mm-lamp code and unit testing, but I forgot to press "save comment" button and I proceeded directly to hitting "submit PR review" button. This submitted all my previous comments but looks like it deleted that unsaved comment. For now I have to go. I will recreate that comment in approx. 12 hrs.

david-a-wheeler commented 1 year ago

Manual testing is good. But we have to cover such functionality with unit tests too.

Fair enough.

I left a review comment regarding this. ... Unfortunately you will not find this comment. I wrote a big comment with few explanations related to the mm-lamp code and unit testing, but I forgot to press "save comment" button and I proceeded directly to hitting "submit PR review" button.

I'm sad that it got lost, I would have liked to have read it.

I'll look for existing test examples and try to follow your conventions.

david-a-wheeler commented 1 year ago

I'd love to hear more about testing. I only did a quick look, but on the quick look I didn't see how you test embedded functions in Rescript, at least if you want tests in separate files.

I see you're using an RSpec-inspired test approach (describe... it). That not my personal preference, but I'll be happy to comply once I know how to do it in this case :-).

david-a-wheeler commented 1 year ago

I'll make the code changes tonight. I'll also create the tests tonight if I can figure out how to do that :-). Suggestions on what to mimic when testing, or in general what you'd like to see in tests, would be eagerly read :-).

expln commented 1 year ago

I've just started composing a response. Please wait for it.

expln commented 1 year ago

I'd love to hear more about testing. I only did a quick look, but on the quick look I didn't see how you test embedded functions in Rescript, at least if you want tests in separate files.

Sure. Here is some additional info which should be useful for changes in this PR. Sorry, my response is long, but this is the required minimum what I think I had to tell you.

Files beginning with MMcmp are very coupled with UI related things like React, DOM, window global variable and so on. Files beginning with MMwrk must not depend on all that UI related things. cmp stands for "component". Usually one cmp file contains one React component. However, this is not so strict rule, and there are few exceptions. wrk stands for "worker". The reason why wrk files should not depend on UI related things is that those files could be used in a worker thread. Worker threads don't support many features which are supported in the main thread. If such a UI related feature appears in a worker thread it usually leads to a compilation error or a runtime error. Some of the wrk files are used in a worker thread, some of them are not used but could be eventually used if needed.

If an algorithm doesn't depend on UI features, like the one in this PR, I usually move such an algorithm to a wrk file. The best place for renumbering algorithm is MM_wrk_editor.res. Please place the new functions at the bottom of this file. Then you will have to export the "main" function by placing its signature to the interface file - MM_wrk_editor.resi. The signature should be as follows:

let renumberSteps: editorState => result<editorState,string>

You may name it renumberNumberedSteps if you wish. BTW, what about "Renumber numeric steps" for the number not to appear in two consecutive words?

The function returns result<editorState,string> because there could be an error during renumbering. However, if your implementation will return not changed state in the case when renumbering is not possible that's also fine. But it would be of course more user-friendly if mm-lamp can explain a user why renumbering is not possible. Please see below why renumbering could be impossible.

Another problem with cmp files is that they are hard to test. Basically, there are no unit tests for the UI related logic in mm-lamp. All unit and integration tests are written for wrk files. Once you place your code into MM_wrk_editor.res and export it via MM_wrk_editor.resi, you will be able to use it in MM_cmp_editor.res and also writing unit tests will become easier.

There are also some conventions related to "act" and "rnd" functions in cmp files I use, but to make my response not too long I will explain it after you are done with wrk files. There will be not too much to update in the cmp file.

Regarding regex, I meant that you also could use regex to check if a string consist of digits only. Here is an example (from Xml_to_React.res file):

let fontSizeValuePattern = %re("/^\d+(.\d+)?em$/")
switch attrValue->Js_string2.match_(fontSizeValuePattern) {
    | None => Error(`"font-size" attribute should be specified using "em" units.`)
    | Some(_) => Ok(())
}

In your case you could write like that:

let renumberable = label => label->Js_string2.match_(digitsOnlyPattern)->BeltOption.isSome

However, I am not sure if this will work faster than your implementation when you split string into an array. So, that's up to you.

Now regarding tests. There is an example of tests for the editor related functions - https://github.com/expln/metamath-lamp/blob/feature/16-display_HYP_as_jstf_for_hyps/src/metamath/test/MM_wrk_editor_test.res

You may notice I also recently started adding unit tests at the bottom of that file. Please create new file for your tests for our PRs not to conflict and also because that file is already big, and it is going to become a lot bigger. Please name the new test file MM_wrk_editor_renumber_test.res Currently, there is no naming convention for the tests. The structure of tests is simple - you create initial editor state, then modify it with the renumberSteps function and check that the new labels and justifications are as expected.

Regarding the renumbering algorithm. I suspect that stepNumber := stepNumber.contents + 1 may be not enough in some cases. Here is how I planned to implement renumbering:

Renumber all renumberable steps to some intermediate label. Renumbering to some intermediate label is required to make "free" some smaller step numbers which could be used closer to the bottom of the editor. You may find what prefix you should prepend to each renumberable label and rename each step by prepending it with that prefix.
After renaming each step use MM_wrk_editor.replaceRef() function to update justifications. This function returns result<editorState,string>, that's why, at the beginning, I recommended for the renumberSteps function also return result<editorState,string>. Why renumbering could be impossible: if, for example, one of the justifications is not parsable. In that case we cannot modify that justification, therefore we cannot do renumbering, otherwise we can introduce chaos to what a user has done so far. Actually renumbering menu item should be inactive if the editor has errors. Then a user will not be able to call renumberSteps function at all, so it is not vital for it to return an error message, but if you have time to implement it, this would be nice (this will make renumberSteps function more independent).
After intermediate renumbering is done, do the final renumbering. This time use MM_wrk_editor.createNewLabel() function. It already does some checks and returns a label which can be safely used for provable steps. This function doesn't support labels for hypotheses.

I recommend you first implement renumbering only for provable steps since the algorithm is a bit complicated. Then you may write tests. And then add the required code for hypotheses.

david-a-wheeler commented 1 year ago

Thank you, this is great!

You'll probably see a PR copying some of that text into the docs/ directory :-).

I'm happy to create a new work file, and that also resolves my concern about how you get "into" the UI component to test much of the functionality.

Renumbering to some intermediate label is required to make "free" some smaller step numbers which could be used closer to the bottom of the editor. ...

The renumbering algorithm you outlined seems unnecessarily complicated. I already implemented renumbering, and it already works on any type of step and in all cases. There's no need for intermediate labels, nor for "freeing" any space. My algorithm uses a single pass and a hash table to track the renumbering as you go. It doesn't return until the process is done. Remember, a step can only legitimately refer to a previous label.

I could tweak my algorithm to replace unknown steps with a strange step value, and the relabel a later step if it's seen. That would gracefully handle screwed-up data, without imposing unnecessary complexity in the normal case. I also think it'd be better if the editor simply forbid renumbering while there's an error, because preventing errors is preferable to recovering from them.

Why renumbering could be impossible: if, for example, one of the justifications is not parsable. In that case we cannot modify that justification, therefore we cannot do renumbering, otherwise we can introduce chaos to what a user has done so far.

I can't see how a justification is "unparseable" for renumbering. Here's a proof that nothing is unparseable for renumbering:

A justification has a ":" or it doesn't: If it doesn't, it's empty or is a bare ref, so just return it; there's nothing to renumber.
If the justification has a ":", the first ":" separates the LHS (the steps) from the RHS (a ref, which might be bogus but will be retained whatever it is).
The LHS of the ":" has 0 or more space-separated labels. If it's 0, we're done, return with ":" ++ RHS.
If the LHS has 1 or more space-separated labels, the labels have either previously been defined (so we can rename them) or they aren't. If they aren't, the data is bogus, and frankly I didn't care about that case. That's easily addressed if we want to harden this, as we can rename it to anything we want - we can just rename them to something random; a weird prefix + 64 bits of randomness would be plenty. Relabel each step, join with a space, and return LHS ++ ":" ++ RHS.

david-a-wheeler commented 1 year ago

I suspect that stepNumber := stepNumber.contents + 1 may be not enough in some cases.

It covers all cases, unless you want to allow configuration of different starts & increment values, which I don't think we need to do. I use larger increments in mmj2, but in metamath-lamp I don't think that is important. Last I checked, you can always add 1 to get an integer's successor :-).

It's true that this will fail when we hit Rescript's MAXINT, 2147483647, which is imposed by JavaScript's bit operators (the only portable way to tell JavaScript "this is an integer, make it go fast"). But a proof more than 2 billion steps should be broken up; I sure wouldn't want to use this UI to handle it :-).

david-a-wheeler commented 1 year ago

Ah, now I see where the "can't parse" difference comes from. I think it's from the function parseJstf in worker/MM_wrk_editor.res (snippet below).

I don't call that function, and I don't use just split(":). I instead use:

 Js.String2.splitAtMost(jstfText, ":", ~limit = 2)

There's at most two entries. For renumbering I don't care what ref says, it could even have multiple ":"s. It'll be erroneous, but it'll be unchanged.

For completeness, here is that code:

let parseJstf = (jstfText:string):result<option<jstf>,string> => {
    let jstfText = jstfText->Js_string2.trim
    if (jstfText->Js_string2.length == 0) {
        Ok(None)
    } else {
        let argsAndAsrt = jstfText->Js_string2.split(":")
        if (argsAndAsrt->Js_array2.length != 2) {
            Error(`Cannot parse justification: '${jstfText}' [1].`)
        } else {
            Ok(Some({
                args: argsAndAsrt[0]->getSpaceSeparatedValuesAsArray,
                label: argsAndAsrt[1]->Js_string2.trim
            }))
        }
    }
}

david-a-wheeler commented 1 year ago

Life is intervening. I won't get that update to you tonight. Hopefully I'll have a chance soon.

david-a-wheeler commented 1 year ago

I believe I can write the wrk function to first detect two error conditions, and bail if they're present:

A state with editing errors. That would prevent, for example, trying to renumber the steps if a justification hyp refers to a label that doesn't precede it.
A hypothesis with a number-only label. That would be a bad idea anyway, as hypotheses labels are global in a database, so they wouldn't work in a database that used '1' as a symbol for example. By refusing to process them problems go away.

If we prevent those bad things, then the renumbering algorithm can be simple. I'll write it defensively to try to deal reasonably with really bad data if it slips through, but those situations would only happen if there was another bug in the editor.

The editor should also shade out the renumber option if there are editor errors, as an aid to the user. But if the wrk function rejects it anyway, then other problems simply can't occur.

expln commented 1 year ago

The renumbering algorithm you outlined seems unnecessarily complicated. I already implemented renumbering, and it already works on any type of step and in all cases. There's no need for intermediate labels, nor for "freeing" any space. My algorithm uses a single pass and a hash table to track the renumbering as you go. It doesn't return until the process is done. Remember, a step can only legitimately refer to a previous label.

Ok, I've just took a closer look at your algorithm, maybe you are right.

I can't see how a justification is "unparseable" for renumbering.

It is very simple. A justification may be:

An empty string.
Non-empty string in the form LHS ++ ":" ++ RHS, where LHS is 0 or more space-separated labels, RHS is a non-empty string. Currently, MM_wrk_editor.parseJstf() doesn't validate emptiness of RHS, but it should.
Other formats are considered invalid.

now I see where the "can't parse" difference comes from. I think it's from the function parseJstf in worker/MM_wrk_editor.res (snippet below).

I don't call that function, and I don't use just split(":)

Not reusing existing functions without strong enough reason for that will make code review harder for me.

For renumbering I don't care what ref says, it could even have multiple ":"s. It'll be erroneous, but it'll be unchanged.

A user could have typed Label1 :abel2 : asrt instead of Label1 Label2 : asrt (notice how close L and : on a qwerty keyboard are). Maybe you mean that your algorithm will leave this unchanged anyway. But this is difficult to reason about. It is much easier to stop if such situation is detected and let user decide how to correct the data.

If we prevent those bad things, then the renumbering algorithm can be simple. I'll write it defensively to try to deal reasonably with really bad data if it slips through, but those situations would only happen if there was another bug in the editor.

I am not sure what you mean by to deal reasonably with really bad data. In order to simplify things and not to think about different possible scenarios, mm-lamp is using (or tends to use) the aforementioned approach stop if bad data is detected and let user decide how to correct the data.

david-a-wheeler commented 1 year ago

Not reusing existing functions without strong enough reason for that will make code review harder for me.

100% agree in general, though I don't think using split will make it harder :-).

But for robustness' sake, I can certainly "stop processing & just return an error message" instead if there is more than 1 colon.

Unfortunately that means a simple "map" won't work, because I can't stop if there's an error. It's not as obvious to me how to "stop processing on error" other than using exceptions, so looks like I'll have use an exception to stop the processing, then catch it to return an error result. I've been preferring result types so far, but I don't see a way to stop mapping on error.

david-a-wheeler commented 1 year ago

Note: I am not done. I've pushed my draft progress in case you wanted to comment. The code is moved and compiles. The one trivial test I have doesn't pass, I'll have to debug that later.

expln commented 1 year ago

Not reusing existing functions without strong enough reason for that will make code review harder for me. 100% agree in general, though I don't think using split will make it harder :-).

That's definitely what I don't want to see in the code :) There are already almost all required functions to do a renumbering. Your code reinvents some of them. I will not be able to accept it. I would like to see the implementation of renumbering written in a higher level of abstraction. I understand you don't know the code base well, so implementing it as I would like to see it is near impossible for you now. I am going to provide a sketch of "higher level of abstraction" algorithm I am thinking of. This algorithm will resolve the problem of catching exceptions too. But this will happen not earlier than in 12 hrs. I am just letting to know you that the algorithm should be changed much. You may continue developing or wait when I send that sketch.

It also may appear that I am completely wrong, and your approach is indeed better than what I am thinking of now. But I will know this only when I try to write such a sketch.

expln commented 1 year ago

@david-a-wheeler

Hi David,

I have committed the initial version of the renumbering algorithm to the develop branch. https://github.com/expln/metamath-lamp/commit/4039ab7d918d3e3e65ed0f56cde212acac5bfe79

You also may notice I used an approach for testing other than I explained you previously. The one I used in this commit is harder to setup, so I didn't mention it.

The comments in the code should give you some explanations regarding the algorithm and the test approach. However, I will provide more detailed response here in this PR tomorrow.

If you see this commit before my detailed explanations, and you have questions, please write them here, it will make my response more to the point.

david-a-wheeler commented 1 year ago

I have committed the initial version of the renumbering algorithm to the develop branch. https://github.com/expln/metamath-lamp/commit/4039ab7d918d3e3e65ed0f56cde212acac5bfe79

Okay, cool! My goal was to help add capabilities to the tool. So since it's getting in there, it doesn't matter to me if I wrote it or not. This will make it easier to create "prettier results".

I presume you'll tweak the editor code to use it.

The comments in the code should give you some explanations regarding the algorithm and the test approach. However, I will provide more detailed response here in this PR tomorrow.

Thanks. I'd eventually like to help you if I can. I certainly learned a lot from this process (esp. Rescript, React, and how this particular code base is organized). While it ended up not beign the final code, I did have something working - which I figure isn't bad for a first try with limited time.

david-a-wheeler commented 1 year ago

I tried to document some of the things I learned in this PR. Here's the result: https://github.com/metamath/lamp-guide/pull/80

This may help someone in the future..!

expln commented 1 year ago

Sure, I will add the renumbering to the UI.

Definitely your code is very good, especially taking into account the amount of time you spent to write a working algorithm. Objectively, the algorithm you proposed is much faster than mine. Complexity of your algorithm is O(num_of_steps), mine is not better than O(num_of_steps^3). Maybe I will have to switch back to your algorithm in the future due to performance. The only reason I could not use the algorithm proposed by you is that at the moment I am not ready to deviate much from the approaches I was using so far.

I am sorry that this PR ended up this way. Thank you so much for the time you spent on it!

david-a-wheeler commented 1 year ago

Objectively, the algorithm you proposed is much faster than mine. Complexity of your algorithm is O(num_of_steps), mine is not better than O(num_of_steps^3).

Mine's faster, but if number is steps is large enough to matter, the proof probably needs to be broken up.

I don't feel bad about the outcome. All I care about is "what the tool does". My code wasn't what you merged, but my code worked & I learned a lot in the process. I've created a PR for the guide that captures some of what I learned, which may help me or others in the future.

The renumbering will let me show a "pretty proof" in my demo video.

I'm really looking forward to this v11 release. Quite stellar.

expln commented 1 year ago

The renumbering will let me show a "pretty proof" in my demo video. I'm really looking forward to this v11 release. Quite stellar.

Sure, I will include renumbering in v11. I finished short/long click remapping today. Also changing P<->H by justification text is implemented. I didn't have time to document everything properly in corresponding issues, but I will do that. Looks like only renumbering is remaining from "major" features to support the demo.

expln / metamath-lamp

Add ability to renumber steps. Fixes #18 #101