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/d50831cd-555c-4c93-8bc7-ab2a473eceb6n%40googlegroups.com.
