On 04/01/2020 18:28, Mario Carneiro wrote:
* If I recall correctly, Stefan O'Rear made a prototype web app that could load and display theorems from set.mm <http://set.mm>, but I don't think this project made it very far and in particular it was not interactive (allowing to write proofs, check individually, run tactics, save the results, etc).
Here is a link to Stefan's Web test. It would be interesting if someone tried it out. I assume it would be a very good starting point for a possible JS assistant. https://github.com/sorear/smm/tree/master/webtest From the README, it seems it provides commands available to the javascript console, so it certainly provides a good back-end. What would need to be filled-in is a front-end (displaying formulas, etc.) In order to load an assistant, it should not be required to load the full set.mm, including comments and proofs. Definitions and statements would be enough, and whatever that input file is, it shall be cached so that next time the user loads it, a local copy is used. -- 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/afc04500-163a-aeeb-e915-e755bf488344%40gmx.net.
