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 On Thursday, January 5, 2023 at 5:14:42 PM UTC+1 David A. Wheeler wrote: > > > On Jan 3, 2023, at 4:51 PM, Igor Ieskov <[email protected]> wrote: > > > > 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 > > 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 > > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4b614e9e-6fdc-4965-b306-97b1704652c6n%40googlegroups.com.
