Web-based mmj2-like proof assistant

[Igor Ieskov]

Hi all,

I am developing a web-based proof assistant and would like to share current results. The proof assistant is written in ReScript programming language and React UI library. It runs completely in the browser. It uses the same approach for building proofs as mmj2 (but at the moment it doesn’t have all the features mmj2 has). I recorded a video (without verbal explanations) similar to one of the mmj2 tutorial videos in order to demonstrate its features. Any feedback is appreciated.

The demo video (if it is not opening, try to download; and sorry for low quality of the video):

https://drive.google.com/file/d/1JCDffUXkb_J-TiA07aNwK9SBKyaukaA3/view?usp=share_link 

The proof assistant:

https://igorocky.github.io/mm-proof-assistant/demo/v1/index.html

The source code is stored in two repositories. And there is mess with it. I started writing it inside of another project, put some logic into a second repo. Because of that it is not easy to run it locally. But I am going to improve this soon.

The source code:

https://github.com/Igorocky/learn-js-react-app/tree/master/src/metamath 

https://github.com/Igorocky/js-common-functions/tree/master/src/main 

Best regards,

Igor

[Antony Bartlett]

On Tue, Jan 3, 2023 at 9:51 PM Igor Ieskov <igori...@gmail.com> wrote:

I am developing a web-based proof assistant and would like to share current results. The proof assistant is written in ReScript programming language and React UI library. It runs completely in the browser. It uses the same approach for building proofs as mmj2 (but at the moment it doesn’t have all the features mmj2 has). I recorded a video (without verbal explanations) similar to one of the mmj2 tutorial videos in order to demonstrate its features. Any feedback is appreciated.

That's amazing, thanks for sharing.  I think it's a first too - I haven't seen a Metamath unifier running in a web browser before (not web 2.0/ajax style anyway).  I also think it's great that there are now at least four of us actively targeting the JavaScript platform.  2023 really could be the year for Metamath on JavaScript!

That's a good UI, I can see you've put a lot of effort into that.  Who's it targeted at?  I think experienced Metamathematicians are probably comfortable editing .mmp files, and I can't tell how suitable it is for beginners.

On Tue, Jan 3, 2023 at 9:51 PM Igor Ieskov <igori...@gmail.com> wrote:

> The source code is stored in two repositories. And there is mess with it. I started writing it inside of another project, put some logic into a second repo. Because of that it is not easy to run it locally. But I am going to improve this soon.

Yes, I couldn't quite get it running when I tried the usual

npm install

npm run compile

npm start

So it might be good to provide a README.md (and a repository with a sensible name), along whatever other streamlining activities you have in mind.

Any new programs written for Metamath currently represent an impressive achievement.  And you've written a parser, a unifier, and a UI, any of which alone is not a small undertaking.

I'd like to see some reusable packages make their way into the npm repository so that this isn't such a huge mountain to climb.  So that front ends can be thrown together as experiments without having to write all the tooling for parsing, verifying, and unifying. My checkmm package (based on ported code) partially succeeds in that regard, and now I am working on a more general purpose parser, but I won't be at all upset if someone gets there first and/or renders my modest efforts obsolete.

Also, if there are any would-be Metamath developers lurking here while working on their first projects, please feel free to talk about it before you have something that's ready to show off!  Not that I was any different, not posting here until I was reasonably happy with the state of my first project, graphmm.

    Best regards,

        Antony

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8c4a0c96-7815-497d-aca0-a1d4ae321eb9n%40googlegroups.com.

[David A. Wheeler]

That's awesome!

I notice that you don't have a license included - please add one!
If you're going to release as open source software, then you need an OSS license.
MIT is especially common:
https://github.com/IQAndreas/markdown-licenses/blob/master/mit.md
The Apache-2.0 and GPL-2.0+ licenses are also widely used.

A way to "get started" with proofs without any installation steps at all has its appeal!

Sadly, the mmj2 tool has become harder to install and maintain.
One problem: it's in Java, but it calls out to JavaScript code, and the
mechanism it uses for calling JavaScript has been dropped from more-recent versions of Java.
Specifically, mmj2 uses Nashorn. My understanding is that Nashorn's intended replacement is GraalVM.
I don't think this is *unsurmountable*.
Mario looked into this briefly & expected that it wouldn't be hard to switch to GraalVM
<https://github.com/digama0/mmj2/issues/7#issuecomment-428404641>,
but no one has (as of yet) picked up this work.

--- David A. Wheeler

[Glauco]

I'm impressed.

And your "search by pattern" is not even available in mmj2 (as far as I know, see this post https://groups.google.com/g/metamath/c/eUKe3kY4y1o)

Glauco

[Igor Ieskov]

Thanks Antony and David for your feedback!

"Who's it targeted at?"

At the moment I don’t have any particular long term plans for this project. I started it just out of curiosity, Metamath seemed very simple and I wanted to try to automate proofs. When I realized that I cannot achieve desired level of automation, I started watching what existing solutions can do. I liked how mmj2 works because it is also seemed simple but very practical. So I decided to check if I can do something similar. When I was able to repeat the proof from the mmj2 tutorial I wrote this post. Now I am planning to work on two more major features - proving in bottom-up direction and proof explorer, some small UI improvements and writing more tests (the code is tough, I already found few bugs). When I complete these goals, probably, I will use this assistant to learn to create Metamath proofs myself. Editing code in a dedicated code editor is much more comfortable but it is difficult to implement, so I didn’t even choose between what kind of UI to implement. Simple HTML UI was the only option for me.

"it might be good to provide a README.md (and a repository with a sensible name)"

I moved the code to a new repository and provided a README file with instructions. Please let me know if there are any issues with running the project locally.

The new repo - https://github.com/expln/metamath-proof-assistant 

This project depends on @expln/utils npm module. This is my project too ( https://github.com/expln/rescript-utils ) But this is not a usual library. This is just a set of useful functions which I collected in one place to reuse across my other projects. And version N+1 may be absolutely not compatible with version N :) 

"I'd like to see some reusable packages make their way into the npm repository so that this isn't such a huge mountain to climb."

That’s a good idea. As for now I think it makes sense for me to implement remaining features and when the code (underlying data structures) become more stable, I will be able to create some API and publish it as an npm package. I also feel like I need to warn regarding the algorithm I use for unification. I read in the mmj2 documentation that mmj2 first creates syntax trees of expressions and then compares them to find possible substitutions (please correct me if I am wrong). As I understand this approach guaranties quick response for any expressions. But what I implemented is comparing two arrays of integers with some performance improvements (counting parentheses is one of them). And there is no guarantee that this algorithm will work fast for any expressions. So it may turn out that using my future library is not such a good decision :) 

"I notice that you don't have a license included - please add one!"

I added MIT license. Thanks for pointing out to this!

Best regards,

Igor

[Igor Ieskov]

Thanks Glauco!

Best regards,

Igor

[Igor Ieskov]

I fixed few bugs and moved my proof assistant to a new URL - https://igorocky.github.io/mm-proof-assistant/demo/latest/index.html 

 
This URL will always redirect to the latest version of the proof assistant ( to https://igorocky.github.io/mm-proof-assistant/demo/vN/index.html )

Best regards,

Igor

[Thierry Arnoux]

Hi Igor and all,

This looks very promising!

What I implemented is comparing two arrays of integers with some performance improvements (counting parentheses is one of them). And there is no guarantee that this algorithm will work fast for any expressions.

I think this is exactly the way the Metamath C program is working, including using parentheses for performance improvement.

The resulting speed seems to be good enough!

Overall I was not active in Metamath during the second half of 2022, for personal reasons. I hope I can be a more active member of the community in the coming months!

Anyway I've been reading what's going on and I see many initiatives going on around tooling; I think this is exactly what we need!

Best Regards, and all my wishes for 2023 to all Metamath enthusiasts!
_
Thierry

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/9aac3fc2-ea01-4bce-afab-7f08aa99be8en%40googlegroups.com.

[David A. Wheeler]

> On Jan 5, 2023, at 7:07 PM, Igor Ieskov <igori...@gmail.com> wrote:
>
> "it might be good to provide a README.md (and a repository with a sensible name)"
>
> I moved the code to a new repository and provided a README file with instructions. Please let me know if there are any issues with running the project locally.
>
> The new repo - https://github.com/expln/metamath-proof-assistant

Excellent!

I've added an entry that links to your new tool from our list of "other tools" for Metamath. The change is here:
- https://github.com/metamath/metamath-website-seed/commit/7225664b017c800033511abdcff22f390005da34
I linked to the redirecting web page, the repo, and the video.

We regenerate the website daily, so that will be visible tomorrow at this location:
https://us.metamath.org/other.html#mmtools

I have a few quick comments about your tool:
* I suggest adding tooltips to every icon, at least with a short name. Then people can hover over an icon & learn what it does. I would never guess that then 5-points-star is "unify" :-).
* Currently it uses "class1" etc. as a working variable, but these are easily confused with specific names. I suggest using mmj2's convention that &C1 is a working variable. Those are easier to distinguish, and it'd look more like mmj2 as well.
* Once proving in the bottom-up direction is added, for many this will begin to be be comparable to mmj2's functionality, while being a LOT easier to install. mmj2 has a number of specialized tricks, but I don't know if they're as commonly used.
- mmj2 does have mechanisms to prove specific patterns, but those are written in JavaScript and might be easily to copy over to a tool already written in JavaScript.
- mmj2's ability to check definitions is awesome, but probably not critical for a proof assistant.

I hope you'll be willing to continue work on it, it looks promising.

--- David A. Wheeler

[Igor Ieskov]

>>> I think this is exactly the way the Metamath C program is working, including using parentheses for performance improvement.

Thank you Thierry. It is difficult for me to understand from the code if it works the same way, but I see it also intensively uses arrays.

>>> I've added an entry that links to your new tool from our list of "other tools" for Metamath

Thank you David!

>>> I suggest adding tooltips to every icon

It is already implemented. The software I used to record the video didn’t capture tooltips. But they are present on all icons and other ui elements (like texts and text fields to show what hot keys may be used). If it is not working in your browser, could you please write what browser you use and its version?

>>> Currently it uses "class1" etc. as a working variable, but these are easily confused with specific names. I suggest using mmj2's convention that &C1 is a working variable. Those are easier to distinguish, and it'd look more like mmj2 as well.

Yes, I am going to implement this.

>>> mmj2 does have mechanisms to prove specific patterns, but those are written in JavaScript and might be easily to copy over to a tool already written in JavaScript.

My tool is actually written in ReScript (which gets compiled to JavaScript). But anyway I don’t think I could easily copy-paste the code even if the tool was written in JavaScript, because most probably we use different data structures and different algorithms. However, the idea of mechanisms to prove specific patterns is interesting to me. I had an idea to add numerous tactics to automate common proof steps, but I need to gain more experience in creating proofs to understand what common patterns exist. And if there are already some mechanisms, I would like to take a look. Could you send a link to the code in mmj2 sources, or documentation, or just write what is the core idea (whatever is easier)?

>>> mmj2's ability to check definitions is awesome, but probably not critical for a proof assistant.

I’ll remember that there is such area like definitions check and will return to it when I am done with the most important features. However, if you have on hand some links with description of what this is, then could you please send it as well, I will take a look.

>>> I hope you'll be willing to continue work on it, it looks promising.

Thank you!

Best regards,

Igor

[David A. Wheeler]

> On Jan 10, 2023, at 4:06 PM, Igor Ieskov <igori...@gmail.com> wrote:
>
> >>> I suggest adding tooltips to every icon
>
> It is already implemented. The software I used to record the video didn’t capture tooltips. But they are present on all icons and other ui elements (like texts and text fields to show what hot keys may be used). If it is not working in your browser, could you please write what browser you use and its version?

I see, it *does* work, but I had to wait longer than expected before they appeared. Perhaps I'm just too impatient :-).

> >>> mmj2 does have mechanisms to prove specific patterns, but those are written in JavaScript and might be easily to copy over to a tool already written in JavaScript.
>
> My tool is actually written in ReScript (which gets compiled to JavaScript). But anyway I don’t think I could easily copy-paste the code even if the tool was written in JavaScript, because most probably we use different data structures and different algorithms. However, the idea of mechanisms to prove specific patterns is interesting to me. I had an idea to add numerous tactics to automate common proof steps, but I need to gain more experience in creating proofs to understand what common patterns exist. And if there are already some mechanisms, I would like to take a look. Could you send a link to the code in mmj2 sources, or documentation, or just write what is the core idea (whatever is easier)?

The main mmj2 repo is:
https://github.com/digama0/mmj2

mmj2's algorithms aren't sophisticated. Here's a key file for its automation capability:
https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js

> >>> mmj2's ability to check definitions is awesome, but probably not critical for a proof assistant.
>
> I’ll remember that there is such area like definitions check and will return to it when I am done with the most important features. However, if you have on hand some links with description of what this is, then could you please send it as well, I will take a look.

The definitions check algorithm is probably best understood by viewing the
"conventions" page section "Additional rules for definitions". Go here:
https://us.metamath.org/mpeuni/conventions.html
The metamath language itself doesn't distinguish between axioms and definitions, but
in practice we *do* maintain such a distinction as explained there.
The mmj2 code for the definition check is here:
https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/definitionCheck.js

By the way, there's a trick you could use in your JavaScript proof assistant:
encode the current proof-in-development in the hashcode ('"#" and text after the URL).
Every time there's an edit, update the hashcode. That will give you undo/redo
for free, make it trivial to save/load proofs, and it would also make it trivial
for people to share proofs with others (just share a URL).
I recommend you not store the entire program state (the .mm files would be enormous),
though the names of the databases might be helpful. See:
https://www.scottantipa.com/store-app-state-in-urls
https://news.ycombinator.com/item?id=34312546
I'm sure there are pros and cons, but I thought I should mention it.

--- David A. Wheeler

[Thierry Arnoux]

Hi Igor,

Ok, let me give you here some quick and random feedback:

Your examples works, but in many cases I do not manage to replace metavariables. For example in "spcgv", when I want to replace "setvar1"  by e.g. "x", or in "brab2a" when I want to replace "class1" by anything.
Every time I get a message "No substitution can be extracted from the provided expressions." How can I deal with that?

It's possible to edit a step's formula using ALT-left click, why not a simple click? (that's why I naturally tried first, then I saw the tooltip...)

If when creating a new step I change my mind, it seems there is no way out of actually creating the step and then deleting it. I end up writing some dummy, and then deleting the step. It would be nice if e.g. just ESC would get you out of the step edition mode.

When "Justification cannot be determined automatically", it would be nice to find out what fails: was an unification found, but distinct variables conditions were missing, or was a unification found, but no matching for (such and such) hypothesis, etc...

Of course more automation would be nice...

On 06/01/2023 19:17, Igor Ieskov wrote:

[Igor Ieskov]

Hi Thierry,

>>> It's possible to edit a step's formula using ALT-left click, why not a simple click? (that's why I naturally tried first, then I saw the tooltip...)

I reserved a simple click for future - I am planning to implement a feature when a simple click on any symbol will highlight the smallest syntax subtree the symbol is included into. I hope this feature will simplify exploring long statements and also it should make it easier to copy subexpressions.

>>> If when creating a new step I change my mind, it seems there is no way out of actually creating the step and then deleting it. I end up writing some dummy, and then deleting the step. It would be nice if e.g. just ESC would get you out of the step edition mode.

That’s right, currently a user is forced to type at least one dummy symbol in that situation. I was trying to implement the editor in the most simple way for me for not to spent a lot of time on ui development when some core features are not ready. Unfortunately, this simple use case is not so simple to fix. But I will definitely fix it in the future. 

>>> When "Justification cannot be determined automatically", it would be nice to find out what fails: was an unification found, but distinct variables conditions were missing, or was a unification found, but no matching for (such and such) hypothesis, etc…

Yeah, I also though about that. Unfortunately I don’t see any simple fix for this at the moment. Moreover the unification algorithm is still under development and I am actively modifying it now when developing bottom-up proofs. But for sure I will try to improve this in the future. BTW, what is current behavior of mmj2 in a similar situation?

Thanks Thierry for your feedback! 

And next follows the most difficult part of my response (at least for me) :) 

>>> Your examples works, but in many cases I do not manage to replace metavariables. For example in "spcgv", when I want to replace "setvar1"  by e.g. "x", or in "brab2a" when I want to replace "class1" by anything.

If I am getting you correctly, you started with an empty page, read all the set.mm, added “spcgv” by searching it by label. As a result you’ve got the state as follows:

Variables:

    var1 setvar setvar1

    var2 class class2

    var3 wff wff3

    var4 wff wff4

    var5 class class5

Disjoints:

    setvar1,wff4,class2

stmt1-spcgv.11: |- ( setvar1 = class2 -> ( wff3 <-> wff4 ) )

stmt1:|- ( class2 e. class5 -> ( A. setvar1 wff3 -> wff4 ) )

Then you tried to replace setvar1 with x and you’ve got “No substitution can be extracted from the provided expressions.” 

In that case it behaves exactly as I programmed it, though I am not sure if this is correct as for a proof assistant. And I need your and others experienced metamath developers help to verify this. This case doesn’t work because of disjoints. The Metamath book explains how to check disjoints when we are verifying a proof, but I have not found any explanation of how to check disjoints in a proof assistant (or maybe I have not read till that place in the book or skipped it unintentionally :) ) So I came up with the following rules myself. When you provide “Replace what” = [some sequence of active symbols] and “Replace with” = [another sequence of active symbols], the program searches for all possible substitutions by means of which we can get from [some sequence of active symbols] to [another sequence of active symbols]. In your example there is only one possible substitution setvar1 -> [x]. Then the program adds all other active variables to this substitution replacing them by themselves. So as a result we have such substitution:

setvar1 -> [x]

x -> [x]

ph -> [ph]

class2 -> [class2]

… and so on for all other variables defined in set.mm and all the work variables. 

I introduced this by analogy of applying substitutions during proof verification, when we have to apply a substitution simultaneously for all the variables in the assertion used in the proof step.

Next the program checks disjoints for this substitution. setvar1 results in [x] (an expression consisting of only one symbol) and class2 results in [class2] (also an expression consisting of only one symbol). Then similarly to the checks in proofs:

1. “the two expressions must have no variables in common”: [x] and [class2] have no common variables - this is passed.

2. “each possible pair of variables, one from each expression, must exist in an active $d statement …”, i.e. x and class2 must be in a disjoin group - this fails. So the entire substitution is considered invalid and the programs shows “No substitution can be extracted from the provided expressions.”

This is possible to fix by adding a disjoint “x,wff4,class2”, so you’ll end up with two disjoints:

Disjoints:

    setvar1,wff4,class2

    x,wff4,class2

Then the replacement should work. 

Please let me know if this is what is expected from a proof assistant. If this is correct behavior, then I will consider adding some messages to the ui explaining why no substitution can be found or even adding missing disjoints automatically.

Best regards,

Igor

[Igor Ieskov]

Hi Thierry,

Sorry, I have not replied regarding the attached json file with an editor state. I saw there are few statements marked as " should work here ". But currently it is not easy to debug such issues, and I am also modifying the unification algorithm at the moment. So I decided to postpone this issue until I finish current changes. Maybe this issues will be resolved in the new code, otherwise it will be easier for me to investigate it because I am adding additional debug utilities.

Best regards,

Igor

[David A. Wheeler]

On January 11, 2023 2:42:10 PM CST, Igor Ieskov <igori...@gmail.com> wrote:
>
>
>Hi Thierry,
>
>*>>> It's possible to edit a step's formula using ALT-left click, why not a

>simple click? (that's why I naturally tried first, then I saw the

>tooltip...)*

>
>I reserved a simple click for future - I am planning to implement a feature
>when a simple click on any symbol will highlight the smallest syntax
>subtree the symbol is included into. I hope this feature will simplify
>exploring long statements and also it should make it easier to copy
>subexpressions.

I like that featurevidea, but I think "normal left click" to edit the box, vs. Although left click to do a special selection, would be much more intuitive.

In particular, if you never discovered the special selection option bur can edit, you can get things done. The reverse isn't true.

[Igor Ieskov]

Ok, that makes sense. I changed it to a simple click in v3.

https://igorocky.github.io/mm-proof-assistant/demo/v3/index.html

Best regards,

Igor

[Thierry Arnoux]

Hi Igor,

Thanks for all answers, and especially the change for the single click!

I understand very well not everything is simple, and you have to move on step by step.

Concerning the substitution function: thanks to your explanations, I could make it work in cases which previously blocked!

I think here I would make a difference between the UI substitution function, which is here to help the user, and the substitutions checked when applying theorems.

The later requires to follow distinct variables requirement, and it's very nice that your proof assistants follows with that along the way (that is a weak point of MMJ2 in my opinion, as it seems to only worry about disjoint variables after the whole proof is complete, and sometimes miss some).

However It looks like for the former, in the example we use, an additional burden is placed on the user to manually add new DV for UI substitutions. Actually, I think ideally the UI would instead help the user and automatically turn the DV restriction from "setvar1,wff4,class2" into "x,wff4,class2". Indeed the first one disappears (since setvar1 gets replaced), and the second one is the same DV where "setvar1" has been substituted by "x".

Of course it's not just simple substitutions, if a more complex substitution is done, the UI would have to all all variables to the new DV restrictions... so it's probably easier said than done - but that would be another great feature.

Keep it up!

_
Thierry

On 11/01/2023 21:42, Igor Ieskov wrote:

Hi Thierry,

And next follows the most difficult part of my response (at least for me) :) 

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e4e7deb6-06e7-41a3-88a4-a2adcdf1293en%40googlegroups.com.

[Thierry Arnoux]

Ok, one more quick remark (now that I know how to use substitutions!):

Currently, the tool blocks if two steps are the same. One has to manually remove the step, and update any justification using that step.

MMJ2 automatically merged them, IIRC. It would be very nice to have the same mechanism (automatically updating corresponding justifications too, of course!)

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2961bd35-1f93-8cce-feb2-760ace5ae4db%40gmx.net.

[Igor Ieskov]

>>> However It looks like for the former, in the example we use, an additional burden is placed on the user to manually add new DV for UI substitutions.

That's nice to know that my implementation of disjoint checks in the proof assistant is not wrong. Yes, my intent was to not allow (at least to decrease possibility of) creating valid proofs which will fail in metamath.exe because of disjoints or similar kind of issues (my experience in creating MM proofs is very small, so I cannot imagine what kind of issues may arise). So as the very first version I implemented it in the strictest way I could. Now, having your feedback, I will think on how to make it more user friendly. My current ideas what I want to try: 

a) in the substitution dialog, allow users to temporarily disable disjoints (all at once or only some of them) to see how this affects results;

b) add missing disjoints automatically if this helps to make substitution valid (once a user permits this);

c) try to handle automatically simple use cases as in the example with class1->x;

d) something similar to temporarily disabling disjoints but in cases when "justification cannot be found automatically" to make it easier to understand how disjoints affect unification;

>>>  MMJ2 automatically merged them, IIRC. It would be very nice to have the same mechanism (automatically updating corresponding justifications too, of course!)

I have not realized that identical statements could appear as a result of substitution. Now I will add this case to my plans of what to do. Thanks for the idea :)

Best regards,

Igor

[Igor Ieskov]

Hi all,

I made few changes in v4:

- short names for work variables (&Cn, &Sn, ...);

- variables are highlighted with different colors depending on their types (only in the editor tab);

- automatic detection of missing disjoint variable groups when applying a substitution (so now substitutions are easier to do for users in the cases like the one with spcgv described earlier in this thread);

Work variable names and colors are configurable on the settings tab.

https://igorocky.github.io/mm-proof-assistant/demo/v4/index.html

Best regards,

Igor

[Igor Ieskov]

Hi all,

I implemented bottom-up proofs in v5. In order to start proving bottom-up it is necessary to select one statement and click "unify" button. It is not very fast, but for not big statements it works well.

Demo video - https://drive.google.com/file/d/1cjJnvlNGACAmlEnlvxzInqmIqE5dl-0Z/view?usp=sharing  

In the demo video I am trying to repeat (as close as possible) proof steps from this mmj2 tutorial https://www.youtube.com/watch?v=vE3v175cMKM&t=217s

https://igorocky.github.io/mm-proof-assistant/demo/v5/index.html

Best regards,

Igor

[David A. Wheeler]

> On Feb 10, 2023, at 4:56 PM, Igor Ieskov <igori...@gmail.com> wrote:
>
> Hi all,
>

> I implemented bottom-up proofs in v5. In order to start proving bottom-up it is necessary to select one statement and click "unify" button. It is not very fast, but for not big statements it works well.
>
> Demo video - https://drive.google.com/file/d/1cjJnvlNGACAmlEnlvxzInqmIqE5dl-0Z/view?usp=sharing
> In the demo video I am trying to repeat (as close as possible) proof steps from this mmj2 tutorial https://www.youtube.com/watch?v=vE3v175cMKM&t=217s
>
> https://igorocky.github.io/mm-proof-assistant/demo/v5/index.html

WOW! That is *so* cool. That looks like enough functionality that it could be seriously used,
though I'm sure there are many things that could be added.

The fact that there's no "install" step required for this prover is especially neat.
That does reduce a barrier to getting started.
The unification may not be fast, but the demo suggests it's okay.
I suspect there are easy tricks that could make it faster in JavaScript,
and a WebAssembly routine could eventually be added if that becomes a true bottleneck.

What are the "key" things you think it's missing, especially in comparison to mmj2?

--- David A. Wheeler

>
> Best regards,
> Igor
>
> On Monday, January 23, 2023 at 9:51:41 AM UTC+1 Igor Ieskov wrote:
> Hi all,
>
> I made few changes in v4:
> - short names for work variables (&Cn, &Sn, ...);
> - variables are highlighted with different colors depending on their types (only in the editor tab);
> - automatic detection of missing disjoint variable groups when applying a substitution (so now substitutions are easier to do for users in the cases like the one with spcgv described earlier in this thread);
>
> Work variable names and colors are configurable on the settings tab.
>
> https://igorocky.github.io/mm-proof-assistant/demo/v4/index.html
>
> Best regards,
> Igor
>
> On Friday, January 13, 2023 at 10:59:53 AM UTC+1 Igor Ieskov wrote:
> >>> However It looks like for the former, in the example we use, an additional burden is placed on the user to manually add new DV for UI substitutions.
>
> That's nice to know that my implementation of disjoint checks in the proof assistant is not wrong. Yes, my intent was to not allow (at least to decrease possibility of) creating valid proofs which will fail in metamath.exe because of disjoints or similar kind of issues (my experience in creating MM proofs is very small, so I cannot imagine what kind of issues may arise). So as the very first version I implemented it in the strictest way I could. Now, having your feedback, I will think on how to make it more user friendly. My current ideas what I want to try:
>
> a) in the substitution dialog, allow users to temporarily disable disjoints (all at once or only some of them) to see how this affects results;
> b) add missing disjoints automatically if this helps to make substitution valid (once a user permits this);
> c) try to handle automatically simple use cases as in the example with class1->x;
> d) something similar to temporarily disabling disjoints but in cases when "justification cannot be found automatically" to make it easier to understand how disjoints affect unification;
>
>
>
>

> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/a8ccebbc-1fca-4d52-87fb-cf9928d72260n%40googlegroups.com.

[Igor Ieskov]

Thanks David!

>>> What are the "key" things you think it's missing, especially in comparison to mmj2?

1) I think one of the "key" missing things is ability to help a user to understand why a statement doesn't unify. As also Thierry noted earlier, currently the app shows only this message "Justification cannot be determined automatically".  Or another message is possible too "Justification for this statement is incorrect". But the app doesn't explain what is the reason. That's my next goal. I don't see any trivial or simple solution, so it may take some time to implement. 

2) Another, although maybe not a "key" thing, is to have predefined "tactics" to prove some common cases, for example, prove by induction or prove by case analysis. This not necessarily has to result in complete ready proofs, but it may create another new statements which help a user to move in the desired direction (similar to what I saw in Coq proof assistant). 

3) As you mentioned mmj2 uses some useful heuristics. I also would like to add heuristics to improve automatic proof search.

4) Finally, not key at all, but what should improve user experience and may be achieved relatively easy (implementation still may require a lot of time but at least everything is clear for me in terms of how to implement):

a) exit edit mode by pressing ESC key

b) highlighting syntax subtrees by clicking them

c) graphical visualization of justifications

d) proof explorer for the loaded *.mm file

e) sharing proofs via URLs (as you suggested and I find this very useful for collaboration). I want to implement this after some time, because when I implement it, I will have to support backward compatibility between different versions, so I want to wait when internal representation of the editor state becomes stable (no frequent changes in the code).

Currently my plan is to work on the 1st and 4th items.

Best regards,

Igor

[Glauco]

Hi Igor,

the .mm parser is REALLY fast.

Does it also do validation?

How is it implemented? Server side? Javascript? Webassembly?

Thanks for this cool tool.

Glauco

[David A. Wheeler]

> On Feb 11, 2023, at 5:00 AM, Igor Ieskov <igori...@gmail.com> wrote:
>
> Thanks David!

You're very welcome! This version really has come a long way:
https://igorocky.github.io/mm-proof-assistant/demo/v5/index.html

One broad suggestion: Could you give it a short & less generic name,
since there are other Metamath proof assistants?
Naming is hard, but a short unique name will make it easier to discuss & find.
And I think this is *very* worthy of discussion & being found.

You might want to include, on the screen or an "about" option, a link to the
GitHub repo for the code (so people can review/contribute). I understand that is currently:
https://github.com/expln/metamath-proof-assistant (MIT license).

> >>> What are the "key" things you think it's missing, especially in comparison to mmj2?
>
> 1) I think one of the "key" missing things is ability to help a user to understand why a statement doesn't unify. As also Thierry noted earlier, currently the app shows only this message "Justification cannot be determined automatically". Or another message is possible too "Justification for this statement is incorrect". But the app doesn't explain what is the reason. That's my next goal. I don't see any trivial or simple solution, so it may take some time to implement.

Whoa, that's a very high bar.

I suggest working on other things first & getting back to that later (if ever). In particular, if you add tactics & some automation, the reason for that answer will change, so I suggest working on some predefined tactics/heuristics first.

If your intent is to just determine why "this statement doesn't unify with this other specific statement", you could try to find the longest match & identify where it finally fails. That seems doable. You could even walk across the database & report the longest incomplete match, but I don't know if it'd be helpful; it'd probably report some very general but unrelated theorems. But I think trying to answer "why can't I automate this in general" is best delayed for a long time. I can be wrong, of course :-).

> 2) Another, although maybe not a "key" thing, is to have predefined "tactics" to prove some common cases, for example, prove by induction or prove by case analysis. This not necessarily has to result in complete ready proofs, but it may create another new statements which help a user to move in the desired direction (similar to what I saw in Coq proof assistant).
>
> 3) As you mentioned mmj2 uses some useful heuristics. I also would like to add heuristics to improve automatic proof search.

You could easily combine 2 & 3. Just create a first tactic called "auto" or similar that tries to apply a few simple rules to automatically prove a few simple/common cases. I would devise them so that eventually tactics could be called internally (e.g., by other tactics & maybe even a scripting language). Then make it so a user can select a tactic to a selected set of statements, and you're off.

mmj2 has a few simple heuristics that it applies automatically its default configuration.
You could make them either fully automatic or the basis for an "auto" tactic. Code here
(I think Mario wrote more or all of this):
> https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js
Don't feel you have to use it exactly, and it might be better split into different
tactics (mmj2 doesn't really support multiple different tactics, a big weakness of it).

Even a few small automations could make a big improvement in usability.

> 4) Finally, not key at all, but what should improve user experience and may be achieved relatively easy (implementation still may require a lot of time but at least everything is clear for me in terms of how to implement):

User experience improvements can make a big difference. I think that's more key than you realize, and I bet a few easy ones would make all the difference.

> a) exit edit mode by pressing ESC key

Yes! Existing with the ESC key would be a big help.

> b) highlighting syntax subtrees by clicking them

To simplify replacing them, I guess?

> c) graphical visualization of justifications

Graphical visualization of justifications is probably not very helpful, they tend to be a mess once they become non-trivial.

I would instead prefer an optional simple column, to the left of the statement proved, showing JUSTIFICATION_NAME LIST_OF_REFERRED_STATEMENTS (similar to how mmj2 works now). I'd also make the default statement names shorter (so that justification text takes less space), e.g., shorten "stmt" to "s" or some such. In the future, as a bonus, it'd be nice to be able to rename step names - they don't matter for the final proof, but it might make proving things easier.

> d) proof explorer for the loaded *.mm file

A nice-to-have, but I think you can delay that. The metamath website already provides a proof explorer that people can use.
You could provide a link that opens a new tab to us.metamath.org and get a lot of the way there.

> e) sharing proofs via URLs (as you suggested and I find this very useful for collaboration). I want to implement this after some time, because when I implement it, I will have to support backward compatibility between different versions, so I want to wait when internal representation of the editor state becomes stable (no frequent changes in the code).

Cool, glad you liked the idea. The rationale for delay makes sense, though I can't wait to use it :-). Once you implement 4(e), undo/redo becomes trivial (you can let the browser do it!). I suspect there's no need to compress it, and you'll get decent results from encodeURIComponent(JSON.stringify(your_representation_here)). Of course, there's the question of what your_representation_here is :-). Just don't stick the whole MM database in there :-).

> Currently my plan is to work on the 1st and 4th items.

As I said, I'd delay #1 (that is likely to be *hard* unless you really back off on your plans).
I'd love to see small increments on #4, and a little automation (#2/3).

Regarding user improvements, most people will want to load the current set.mm & iset.mm,
so making that easier would be helpful. If there was an easy way to download it straight
from the web, that might make getting started easier. I could easily configure
us.metamath.org's CORS settings so the script could always download .mm files from us.metamath.org
no matter where it started from.

You might want to walk through the mmj2 tutorial to see what ideas are
worth stealing. I recorded it on Youtube here:
https://www.youtube.com/watch?v=87mnU1ckbI0
The text is here:
https://github.com/digama0/mmj2/tree/master/mmj2jar/PATutorial

Once you're further along, I'd be happy to work with you to create a tutorial
if you'd like. I'd probably want to build on the same examples from the mmj2 tutorial.

It's your project, so take my comments with a bucket of salt.
I really do think this is neat though!

--- David A. Wheeler

[David A. Wheeler]

(Replying to myself)

Nevermind, I see you can already rename statements in
<https://github.com/expln/metamath-proof-assistant> /
<https://igorocky.github.io/mm-proof-assistant/demo/v5/index.html>!
You clearly demo'ed it too.

When renaming, I *do* wish that either RETURN or ESCAPE would save the name.
I'd prefer shorter default statement names, because I hope to eventually see them &
their justification names on screen, but clearly the functionality is there already.

I don't see how to create hypothesis statements in the tool, that's probably more important
if it's not already there (I didn't see how to do that).
I recommend not using "h" as a prefix to indicate that (mmj2 does that,
but I don't think that should be repeated). I think a button that sets/unsets
a statement's "hypothesis" flag would be great, and then just have a special
onscreen marker for hypotheses.

--- David A. Wheeler

> --
> You received this message because you are subscribed to the Google Groups "Metamath" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/C2593B77-C1F2-45F5-8523-E347EEF5C569%40dwheeler.com.

[Jim Kingdon]

On 2/11/23 07:39, David A. Wheeler wrote:

> 1) I think one of the "key" missing things is ability to help a user
> to understand why a statement doesn't unify.

I have only an approximate idea of whether this is easy or hard, but I
will say that even modest improvements here would be helpful. For
example, it may be easier to detect particular cases than every possible
"way" a statement can't unify. One of the more time consuming things
that happens to me when using mmj2 is that a unification which I
expected to happen doesn't, and then I need to look at (sometimes long)
expressions to figure out what parts don't match.

[Igor Ieskov]

>the .mm parser is REALLY fast.

>Does it also do validation?

>How is it implemented? Server side? Javascript? Webassembly?

Thanks Glauco. Yes, the parser validates syntax and some other rules like no duplications of labels, a symbol declared as a constant cannot be redeclared as a variable, expressions must begin with a constant, and so on. If you try to load an invalid mm file you'll probably get an error message. I cannot state that I implemented all the possible validations but I tried to do as much as I could following the Metamath book. If you mean validation of proofs, then no, the parser doesn't validate proofs. However, there is a function to validate proofs, but it is used only in tests to check if a proof generated by the proof assistant is successfully verified by the standard verification algorithm. 

Parsing is implemented in a very straightforward way. Entire mm file content gets stored in a string variable. Then I use local int variables to store indexes of some important parts like last char read, begin and end of current token, etc. The main idea is to make necessary decisions and checks using only indexes and then "substring" only required parts of mm file content  (labels, math symbols etc.) , and do not "substring" what is not actually required. I think Mario also mentioned similar approach in one thread with discussion of performance of proof verifiers.

Everything runs in a browser. This proof assistant doesn't have server side. It runs only in JavaScript. To be honest I am also impressed how fast it parses. I think, besides that approach with indexes, modern JS engines make very good optimizations. Also I don't exclude that ReScript compiler when generating JS code may do some optimizations. But I have not analyzed generated JS code, so I cannot say much on that. You also may notice that the proof assistant runs in two threads in a browser, but this is done not for performance. One thread is actually doing some task and another renders UI. This is done to make UI responsive when executing long running tasks and also to have ability to terminate such tasks if they become too long.

Here are some references to parser and proof verifier implementations:
Parser, which builds AST (abstract syntax tree) - https://github.com/expln/metamath-proof-assistant/blob/32d904911228f69a716a4f328a525acfd4e31d9b/src/metamath/mm-utils/MM_parser.res#L44  (parseMmFile function in MM_parser.res).

Parser, second part (well, actually not parser, but it does further processing after building AST) - https://github.com/expln/metamath-proof-assistant/blob/32d904911228f69a716a4f328a525acfd4e31d9b/src/metamath/mm-utils/MM_context.res#L1004 (loadContext function in MM_context.res).

Proof verifier - https://github.com/expln/metamath-proof-assistant/blob/32d904911228f69a716a4f328a525acfd4e31d9b/src/metamath/mm-utils/MM_proof_verifier.res#L255  (verifyProof function in MM_proof_verifier.res)

Thanks David and Jim for useful ideas. I have what to reply to each suggestion/idea, but unfortunately I don't have enough time to do this in this email. I will partly reply here, and I will reply for remaining part in my next email.

>As I said, I'd delay #1 (that is likely to be *hard* unless you really back off on your plans).

>I will say that even modest improvements here would be helpful

I would agree with Jim that some hints from the program explaining why something doesn't work as expected would be helpful. Moreover, this is one of the most interesting parts to implement for me :) I have an idea what I can try to do. In few words, I will try to create a dialog similar to proving bottom-up with different parameters. For example don't verify disjoins, verify disjoints but skip this ones, and so on. So a user can switch them on and off to find out when unification stops working. Also I may try to record everything interesting what happens during unification and then present this info to a user in some readable format so the user should be able to find the place when things don't go the way he/she wants. I also will check if I can detect particular cases and notify a user about them as Jim suggested. 

In general, I will not stop implementing other useful things, but I cannot delay working on that part with hints for users because this is very interesting for me :)

>One broad suggestion: Could you give it a short & less generic name,

since there are other Metamath proof assistants?

Sure. I will come up with some short name. And also I will shortly move it to another URL - https://expln.github.io/...

>Regarding user improvements, most people will want to load the current set.mm & iset.mm,
>so making that easier would be helpful. If there was an easy way to download it straight
>from the web, that might make getting started easier. I could easily configure
>us.metamath.org's CORS settings so the script could always download .mm files from us.metamath.org
>no matter where it started from.

That's a good idea. I saw in another thread you've already configured CORS. Thanks for that. I will implement loading of set.mm and iset.mm from  us.metamath.org

I will reply to the remaining items a bit later :) Thanks for the feedback and new ideas!

Best regards,

Igor

[Glauco]

Hi Igor,

below I tell what I've come up with, in yamma.

First, I'll write the short story, then I'll elaborate a bit about the theory and the challenges.

The short story:

yamma has two kinds of diagnostic messages for unification failure.


The first kind of message, suggests how to fix the unification error. Two examples:

"Unification error: referenced statement is '|- ph' but it was expected to be '|- ( ps -> ph )'"

(see https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L329 for the full unit test)

or

"Unification error: statement is '|- ch' but it was expected to be '|- ( &W1 <-> &W2 )'"

(see https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L498 for the full unit test)

The first example is a diagnostic highlighted on the hyp label, referencing a formula that doesn't match what's expected.
The second example is a diagnostic on the statement itself (the 'main' formula cannot be unified with what's expected by the step label)


The second kind of messages, involves substitution of working vars. Example:

'Working Var unification error: the  working var &W2 should be replaced with the following subformula, containing itself ( &W2 -> ph )'

(see https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L420 for the full unit test)



Now, a bit of 'theory' (as far as I understand it)

There are two categories of unification:

1. single statement

2. multiple statements

With single statement unification, you're trying to find the mgu for both the logical variables (the theory's variables) and the (possible) working variables. You could use a Martelli Montanari algorithm on the whole proof, and it will be clean and "secure", but you'll not get a super-informative error message.
That's why, for the single statement unification, I've gone for a 'custom' approach, that allows for some better error message.

With multiple statement unification, you're trying to find the mgu for all the working vars in the proof (because logical variables have already been 'substituted').
Here, I've gone with the 'pure' Martelli Montanari algorithm.
It can fail either
- with a 'clash fail' error (for metamath, it means two constants don't match; something like '->' was expected, but you have '<->' )
or
- with an 'occur check fail' (a working var should be replaced with a formula strictly containing itself)

Hope this can give you some ideas.

 

[Igor Ieskov]

Sorry, I missed one question which could be easily answered:

> I don't see how to create hypothesis statements in the tool

This is implemented. Each statement is prefixed with an upper case letter  either P (provable) or H (hypothesis). Alt-left-click allows to change it. This is demonstrated  at 5:49 in this video - https://drive.google.com/file/d/1JCDffUXkb_J-TiA07aNwK9SBKyaukaA3/view

-

Igor

[Igor Ieskov]

>One broad suggestion: Could you give it a short & less generic name,
>since there are other Metamath proof assistants?

That’s done! The new name is metamath-lamp “Lite Assistant for Metamath Proofs”.
I renamed the repository accordingly:
https://github.com/expln/metamath-lamp
I guess I need to create a pull request to make corresponding changes on https://us.metamath.org/other.html ? I will try after sending this email.

> You might want to include, on the screen or an "about" option, a link to the
> GitHub repo for the code (so people can review/contribute). I understand that is currently:
> https://github.com/expln/metamath-proof-assistant (MIT license).

Good point. I will add such a link. Yes, MIT license, but the new URL is https://github.com/expln/metamath-lamp

> But I think trying to answer "why can't I automate this in general" is best delayed for a long time.

I thought on this, and finally concluded that this is not even a “nice to have” but this is “must have” feature. The reasoning is as follows. Users will ask me “why this doesn’t unify” or “why this cannot be proved automatically”. Currently the only solution is to reproduce the case locally and debug. But this is too hard because I debug by small steps and I don’t see a bigger picture. Thus I conclude that I need some kind of log of main events to understand faster what’s going on. So I feel like I cannot delay development of this feature.

> You could easily combine 2 & 3. Just create a first tactic called "auto" or similar that tries to apply a few simple rules to automatically prove a few simple/common cases.

I don’t have enough experience to figure out what are the common cases. I need to spend some time practicing in creating proofs first. And this is related to the tutorial topic (please see my response on tutorial topic below).

> mmj2 has a few simple heuristics that it applies automatically its default configuration.
> You could make them either fully automatic or the basis for an "auto" tactic. Code here
>(I think Mario wrote more or all of this):
>> https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js

Thanks for the reference. I will check and return back to you and Mario with questions when I will be closer to writing heuristics.

> Even a few small automations could make a big improvement in usability.

If anyone sees such small automations please let me know. I have experience in writing code which manipulates metamath statements, but this adds almost nothing to my ability to create actual proofs, so such kind of small improvements are not visible to me at the moment.

> > b) highlighting syntax subtrees by clicking them
> To simplify replacing them, I guess?

Yes, but not only. This should also make easier to copy subexpressions. Currently unexperienced users like me have to count parentheses which is too tedious.

> I would instead prefer an optional simple column, to the left of the statement proved, showing JUSTIFICATION_NAME LIST_OF_REFERRED_STATEMENTS (similar to how mmj2 works now).

That’s doable. I will add this to my todo list and implement in some time.

> You might want to walk through the mmj2 tutorial to see what ideas are
> worth stealing. I recorded it on Youtube here:
> https://www.youtube.com/watch?v=87mnU1ckbI0
> The text is here:
> https://github.com/digama0/mmj2/tree/master/mmj2jar/PATutorial

Yeah, I watched it few times and will watch one more time with pleasure. Moreover, I have now more understanding of the processes under the hood, so I am able to catch more details. (When I watched it for the first time few years ago it was like magic to me :) )

> Once you're further along, I'd be happy to work with you to create a tutorial
> if you'd like. I'd probably want to build on the same examples from the mmj2 tutorial.

Of course! This is a great opportunity for me to get more experience in creating proofs and simultaneously help other metamath newcomers to get acquainted with it. If you can provide those mmp files from us.metamath.org, and additionally some json file which will work as a table of content for the tutorial, then I will parse them and represent in my app. Such an interactive tutorial could be a good starting point for beginners. So, once you think my app is ready to become a tutorial for Metamath we may start a separate email thread and discuss details of implementation of such tutorial. Currently I think the tool requires more testing, because I implemented some algorithms by intuition and I have not analyzed everything with mathematical rigor.

> Nevermind, I see you can already rename statements

In the previous versions it was not “true” renaming. Justifications were not updated. But in the v6 renaming of statements updates justifications.

> below I tell what I've come up with, in yamma.

Thanks, Glauco, for the ideas. I checked your test cases and I see similar validations may be implemented in metamath-lamp too.

> 'Working Var unification error: the  working var &W2 should be replaced with the following subformula, containing itself ( &W2 -> ph )'

Could you please explain why a working var cannot be replaced by a subformula containing itself? It is possible in mm-lamp and I don’t see any reason why it should not be possible.

> Hope this can give you some ideas.

Definitely! Thank you, Glauco!

I implemented few new features and moved my tool to a new URL - https://expln.github.io/lamp/latest/index.html

1) Exit edit mode on ESC, save changes on Enter on all text fields in the editor. (To start a new line in a multiline text editor press Shift+Enter, this is not mentioned on tooltips, but I will add it in the next versions )
2) Shorter names for statements and “true” renaming of statements when justifications are also updated with the new statement label.
3) In substitution dialog, now it is possible to see hints why some substitutions are invalid.
4) A new parameter in bottom-up proofs - “Derive from root statements”. It was present in v5 and it was always “true”. But it significantly decreases performance and I expect it to be not necessary in many cases. So I added it to the bottom-up dialog and set its default value to false. Users will be able to decide if they want to use it or not. I understand that I have to provide here more details on how bottom-up exactly works in mm-lamp and in particular what the new parameter does. But unfortunately I don’t have time right now. I will write this a bit later.

The demo video below demonstrates #3 feature and the use case when #4 feature could be useful.

https://drive.google.com/file/d/1nIigII46Z8l1xk9VRWlPT9_N-VcNTh2R/view?usp=sharing

Current latest version is https://expln.github.io/lamp/v6/index.html

-
Igor

[Igor Ieskov]

Hi all,

I have released version 7 of metamath-lamp with bug fixes and a few new features.

https://expln.github.io/lamp/v7/index.html

Here is a demo https://drive.google.com/file/d/1haJff_AN1M6HZGrWXsgqzrxq-Di84gmZ/view

I used the text-to-speech function of my video editor to add voice explanations in the demo. It might sound a bit unusual, but believe me this is much better than listening to what I retrieve when recording my own voice.

In the demo I used the “my-editor-state.json” set of statements provided by Thierry in one of the posts above (on Jan 11 2023, if anyone wants to find it quickly).

Thank you Thierry for providing “my-editor-state.json”. It allowed me to discover some use cases I was not aware of before and helped me a lot in improving mm-lamp. I also saved it in the source code and implemented a few tests based on it - https://github.com/expln/metamath-lamp/blob/4b25515acb8174086cd970d1b10cc4a26821dbba/src/metamath/test/resources/int-test-data/restore-missing-disjoints/editor-initial-state.json

Few things I want to mention:
- I edited the demo video and cut out some long running phases of unification and bottom-up proving for the demo to be shorter. So in reality mm-lamp might be slower.
- While recording the demo I realized that exporting local variables (this is a new feature explained at the end of the demo) might not work well if such variables are not used explicitly in the statement being exported or its hypotheses but are used in its proof. I have not tried to reproduce this bug but I see in the code that this may happen. I am going to fix this in a future version.
- I forgot to update some tooltips with hotkeys. Here are the correct hotkeys: 1) to start editing a statement, variables or disjoints - left click it; 2) to save the changes - press Enter; 3) to start a new line in variables or disjoints text fields - press Shift Enter.

If anyone sees any mistakes in the current design or finds any issues or bugs, please feel free to let me know. Any feedback is appreciated. For issues and bugs it’s probably better to use the “Issues” section of the repository https://github.com/expln/metamath-lamp/issues

David, I walked through the mmj2 tutorial. Please find some my thoughts below:

1) currently mm-lamp doesn’t allow adding comments. I am going to implement this.

2) undo/redo is also not supported in mm-lamp. Most probably I will not be able to implement this feature by storing the editor state in the URL as you mentioned because internal representation of the editor state is actually more than we may see in the local storage. I could store editor states to the local storage after each modification (I mean keeping all previous versions of editor states). But then I am limited by the available amount of the local storage which is usually not too big. I keep thinking on how I can implement this feature.

3) mmj2 can keep few identical statements and mm-lamp cannot. I cannot change this because this lies in the core - it allows me to simplify some parts of the code. Please let me know if this is a vital or very handy part of creating proofs. If it is needed to keep few possible proofs for a single statement then I will try to implement multiple justifications for a single statement.

4) Renumbering of statements, loading existing proofs - I am going to implement this.

5) mm-lamp cannot automatically prove “|- ( ; 9 5 + 1 ) = ; 9 6”. I hope this will be resolved once I start adding heuristics.

6) Search capabilities of mmj2 are profound, I need some time to learn this and figure out what I can steal.

Best regards,

Igor

[Igor Ieskov]

Hi all,

I have implemented a few new features in the version 9 of mm-lamp https://expln.github.io/lamp/v9/index.html :

1. Reading the set.mm file from us.metamath.org.

2. Possibility to share editor state via URL and JSON.

3. Possibility to add a description with basic formatting.

4. Showing a proof table for the proof being exported.

Here is a short demo (without sound) https://drive.google.com/file/d/1sM19TfF-7nRfhnnsKA_i_1I0H18mUyX5/view 

A few comments on the new features:

1. Reading the set.mm file from us.metamath.org. This is configurable, other URLs may be added on the settings tab. When an editor state is exported, if all the loaded mm files are loaded from the Web then they will be automatically reloaded when this state gets imported. For each URL a user is asked if they want to load data from that URL. The user has the possibility to mark some URLs as “trusted” then data will be loaded from such URLs without asking. This is also configurable on the settings tab.

2. Possibility to share editor state via URL and JSON. Such URLs contain a Base64 encoded editor state. It may be decoded with many online Base64 decoders if for some reason a URL is not opened by mm-lamp but it is needed to see its content. GitHub IO limits URL length so that only about 5K characters in the editor state may be shared via URLs without problems. Exporting/Importing to/from json doesn’t have this limitation. 

3. Possibility to add a description with basic formatting. Initially I planned to use some existing advanced component which is capable of rendering markdown. But then I realized that I don’t control what is injected into the page which makes XSS attacks possible. So I ended up implementing my own markup language which produces simple html without the risk of XSS attacks (at least I think so, if anyone finds such a possibility, please let me know). As a downside, formatting is very basic. But I can add new formatting features if needed.

And one more note. The previous version of /latest/index.html page truncated a query string when redirecting to the actual latest version page. That made redirection with the editor state in the URL impossible. I updated that page (added a programmatic redirection). But a browser may cache the old version. So, if opening a URL with an encoded editor state doesn’t load that state, probably clearing of the cache will help.

This is the link from the demo - proof

-

Igor

[Igor Ieskov]

mm-lamp v10 is released with few new features:

1. Autocompletion for parentheses - when you type an opening parenthesis followed by a space then the closing parenthesis is added automatically and the cursor is placed in between those parentheses.

2. Syntax validation and “syntax aware” selection.

3. Graphical visualization of justifications.

The below demo almost repeats the proof from the v1 demo but using the new features this time:

https://drive.google.com/file/d/1IwdHLpQreZ_1CJFZJmptRJc2unO8aNh4/view?usp=sharing

Best regards,

Igor

[David Starner]

--

You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4c913c14-d74b-4457-a6af-f6fd5dcc5e13n%40googlegroups.com.

[David A. Wheeler]

> On May 9, 2023, at 7:53 AM, Igor Ieskov <igori...@gmail.com> wrote:
>
> mm-lamp v10 is released with few new features:
>
> • Autocompletion for parentheses - when you type an opening parenthesis followed by a space then the closing parenthesis is added automatically and the cursor is placed in between those parentheses.
> • Syntax validation and “syntax aware” selection.
> • Graphical visualization of justifications.
>
> The below demo almost repeats the proof from the v1 demo but using the new features this time:
>
> https://drive.google.com/file/d/1IwdHLpQreZ_1CJFZJmptRJc2unO8aNh4/view?usp=sharing

This is awesome!. Thanks for continuing this work.
I think the ability to "create proofs without installing anything" is a potential game-changer
in terms of making it easier for people to start creating Metamath proofs.

--- David A. Wheeler