Thierry writes:
> Anthony Barlett recently announced his Typescript verifier `checkmm-ts`,
> Does anyone else wish to join forces and work more together on a common
project rather on "competing" ones?
I ported checkmm.cpp to TypeScript, yes. I think it's important to make a
distinction between a port and a new verifier, for reasons both good and
bad. A port is good because it doesn't add to the pile of fragmented
efforts, and bad because it doesn't add to our overall confidence in
Metamath which is in part derived from having multiple
heterogeneous verifiers. It's a pity it probably can't be counted as my
having "joined forces" with the original author, Eric Schmidt.
Now that I have what I wanted, which is a verifier that runs on the
JavaScript platform which I understand and find fun to hack around with,
I'll probably be doing that for a while. I am definitely up for other
JavaScript platform code I can hack around with and potentially contribute
to. As such I am looking forward to seeing Glauco's verifier project.
It's no secret I have also played around with WASM builds of both
metamath.exe and metamath-knife. I think I drifted away from it because
I'm afraid it feels more like "work" than "fun" to interact with two
different programming languages and the interface between them. Sorry to
whoever that may disappoint. Maybe if others have success there I'll
follow their example eventually.
Best regards,
Antony
On Tue, May 31, 2022 at 6:17 AM Thierry Arnoux <[email protected]>
wrote:
> Hi all,
>
> I notice there are several independent Metamath parser/verifiers in the
> making these days:
>
> - Anthony Barlett recently announced his Typescript verifier
> `checkmm-ts`,
> - Glauco is writing a Typescript program / VsCode extension,
> - Benoît is writing a lexer/parser,
> - Mario and I have been working for a while on `metamath-knife`, and
> I'm working on a VsCode extension for Metamath.
> - There are laudable efforts to maintain and extend `metamath-exe`
> (Wolf) and `mmverify.py` (Benoît)
>
> On one hand that's a sign of a vibrant community and that's very good. On
> the other hand these are fragmented efforts (to paraphrase Mario) and we
> might achieve more if we were all working on a single project.
>
> There is of course a cost for team work, as we need to agree on a
> direction and design choices, and coordinate efforts. This also means
> sometimes making concessions, which is never easy. GitHub is a wonderful
> tool which can help a lot here.
>
> Personally I know the time I can spend on Metamath is limited, so I want
> to make it count - and like everyone I also want to have fun!
>
> My questions to the community are:
>
> - Does anyone else wish to join forces and work more together on a
> common project rather on "competing" ones?
> - What would the right direction be for that? Which steps shall we
> take?
> - I followed Mario's call to work in Rust, I think technically it's a
> good choice. That language is growing in popularity, however it is still
> not as popular as e.g. Python, JS/TS, C++ or java, which pretty much every
> programmer touched. Did that choice exclude too many?
> - What was the rationale for you guys to start a new project rather
> than join an existing one? Are those existing project not well-documented
> enough? Is it too daunting to learn about the existing code base? Are you
> missing some clear "good first task" as GitHub calls them? Are the working
> environment of other projects not welcoming enough? Do you think they are
> not going to the right direction? Are there no other projects advanced
> enough to have a critical mass worth joining? Or is simply the challenge to
> do things alone stronger and more appealing?
>
>
> As far as the project I've chosen to work on, the goal with
> `metamath-knife` and the Metamath VsCode Extension would be to provide a
> feature-rich proof assistant in VsCode just like Lean or MMJ2, or at least
> provide in VsCode the functionalities I had in my Eclipse plugin (I made a
> video about that). I've learned Rust as it was the programming language
> suggested by Mario and because `metamath-knife` was seen as a "new
> community verifier".
>
> All work-in-progress is in GitHub and external contributions are of course
> welcome, though only Mario and I are contributing.
>
> I'd love to learn more about other projects (Benoît, Glauco) even though
> we discussed a bit directly: what are your goals/aspirations? Would you
> welcome external contributions?
> BR,
> _
> Thierry
>
>
> --
> 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/8bd47a1f-ca46-5e8d-c159-75877d3eea5d%40gmx.net
> <https://groups.google.com/d/msgid/metamath/8bd47a1f-ca46-5e8d-c159-75877d3eea5d%40gmx.net?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%2BAa1XKOcDTS%3DwS4%3DWm1JWE2puJObJf8Uf277A7Od5HxpA%40mail.gmail.com.
