Progress: first translations from set.mm into new Ghilbert

[Raph Levien]

One of the mistakes I feel I made in the previous prototype was not putting enough emphasis into translation between Metamath and Ghilbert. So this time around, I'm prioritizing that. I'm also getting pretty well settled at Recurse Center and able to focus on cranking out code.

The current github master can translate the propositional calculus fragment from set.mm into Ghilbert and check it. The checking also produces HTML output, at present just the source with a bit of style annotation.

The translation is crude, and could be refined in a number of directions. I'm not removing parentheses that are made redundant by the precedence rules. I've also got one line per step, each with a label whether it's used or not. It's also not including any result lines (which means that the automatic translation of id fails to check and needs to be fixed up manually).

Obviously the propositional calculus fragment is the easy part, I don't have to deal with distinct vs free/bound variables. But it is a start, and I feel I can iterate on the presentation. I'd like to shoot for a reasonably nice Web presentation of existing set.mm proofs for the next couple of weeks or so. When it's in a bit better shape, I'll uploaded it to static serving somewhere. (Advice? In the medium term I'd like static generation to run on a webhook whenever there's a commit to the github repo)

One of the things I feel particularly good about is using a script to guide the translation. The main advantage, I think, is coping with the continuing evolution of set.mm. This is important because I don't want to fork a snapshot, but have Ghilbert and Metamath continue to develop in parallel. The script also gives more flexibility in dealing with edge cases; anything that doesn't work in Ghilbert can be skipped or rewritten as needed.

Raph