> I’m trying to decide if it would be quicker to (port to Smalltalk) or
write new code?
> If MMJ code is elegant/well designed, I will spend time reading it.
> If MMJ is badly designed/messy code then I guess it will be quicker just
to write new code without looking at MMJ?
What's the broader context in terms of what you are trying to achieve here,
please. It's not always a good idea to try and answer a question such as
this without first attempting to understand what might lie behind it.
My only relevant experience here is that I recently succeeded in porting
checkmm from C++ to TypeScript. That was just a verifier, and still not
something to undertake lightly. I've neither used or programmed MMJ, but
it's a multi-faceted thing like metamath.exe isn't it - a proof-assistant
with a suite of tooling surrounding it? I would be looking for a good
starting point - some much smaller piece of useful functionality I could
extract out of MMJ on its own, if I was to contemplate porting it.
My intuition (I've never broached this notion before, I look forward to
seeing if it falls completely flat on its face here) is that as things
stand at the moment there are three pillars to working with mm files -
verification, unification, and html generation. And I was planning to
start asking questions about the unification algorithm sometime in the next
few months, as it's the only part I'm really hazy on (you can ununify a
regular proof by removing all the tokens who's expressions don't start with
|- ('thereby'), but I don't know how you put them back in. It's important
because having to specify all the symbols used in a proof would be really
pedantic). That's the piece of MMJ I'd be after first if it was me.
I was lucky in that I consider checkmm.cpp to be very good code, and agree
with you that it probably wouldn't have been worth bothering otherwise.
That there's room for improving the quality of some of MMJ's code has been
discussed here, but to be honest I'd expect that with any larger
codebase, and I don't know what the overall picture is.
Best regards,
Antony
On Sun, Aug 21, 2022 at 5:32 PM [email protected] <
[email protected]> wrote:
> I’m trying to decide if it would be quicker to (port to Smalltalk) or
> write new code?
>
> If MMJ code is elegant/well designed, I will spend time reading it.
>
> If MMJ is badly designed/messy code then I guess it will be quicker just
> to write new code without looking at MMJ?
>
>
>
> What do you think?
>
> --
> 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/CO3PR18MB4960DE0C165129DE46DE8975A46E9%40CO3PR18MB4960.namprd18.prod.outlook.com
> <https://groups.google.com/d/msgid/metamath/CO3PR18MB4960DE0C165129DE46DE8975A46E9%40CO3PR18MB4960.namprd18.prod.outlook.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%2BAj%3DJ0BrXsDPTVSKdzogM-kNN%2B9e3%3DznYzBxnSuJTZWjg%40mail.gmail.com.
