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/v*N*/index.html )
Best regards, Igor On Friday, January 6, 2023 at 1:14:14 AM UTC+1 Igor Ieskov wrote: > Thanks Glauco! > > Best regards, > > Igor > > On Friday, January 6, 2023 at 1:07:57 AM UTC+1 Igor Ieskov wrote: > >> 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/9aac3fc2-ea01-4bce-afab-7f08aa99be8en%40googlegroups.com.
