> 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/6D20B2AC-F550-4598-A5E9-6E0985549BD0%40dwheeler.com.
