On Tue, Jan 3, 2023 at 9:51 PM Igor Ieskov <[email protected]> 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 <[email protected]> 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 On Tue, Jan 3, 2023 at 9: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 > > Best regards, > > Igor > > -- > 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/8c4a0c96-7815-497d-aca0-a1d4ae321eb9n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/8c4a0c96-7815-497d-aca0-a1d4ae321eb9n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAJ48g%2BBOaKgi8R8ir6QGnjuo_hOMhm8mCUYdMG2-7RWZoQ%3DdhA%40mail.gmail.com.
