Hello there metamath community! I wanted to ask you all 3 questions related to proof assistants:
1. What proof assistant are you currently using? 2. What are some (not so obvious) features of your proof assistant that you like and that you would like to see recreated in future proof assistants? 3. What are some things you don't like about your proof assistant that future proof assistants should avoid? The reason I ask these question is on one hand to create a useful thread for anyone else who might try to create a proof assistant in the future and on the other hand to gather some information for my own upcoming proof assistant called mmt1, with which I aim to create a modern remake of mmj2. This means that the core proof assistant functionality will remain (mostly) the same, while at the same time I want to add much more features that weren't possible when mmj2 was created. As of right now the feature set includes: - A build in theorem explorer: You can browse any database without having to generate html pages and open them in a separate program/window. - A more modern editor: mmt1 uses monaco-editor, a standalone version of vscode's editor, enabling features such as multi-cursor editing and the ability to edit very large files. - A more modern UI: Both in style and functionality. Including a tab system, so that you can have multiple editor and theorem explorer instances open at the same time. - Preview unicode feature: While developing proofs you can activate a live unicode preview that will make reading your proofs easier. - An extended .mmp syntax: You can now also express comments, headers, constant statements, variable statements, floating hypotheses, axioms and theorems with temporary variables/floating hypotheses. - Add to database feature: You can add theorems, axioms, etc. to the database with the click of a single button. Together with the extended syntax this allows you to create entire metamath databases without ever touching a .mm file - An easier installation: Installing mmt1 will be as simple as clicking an installer. No downloading old java versions or adjusting script parameters required. Hopefully the first version of mmt1 will be ready in about 1 to 3 months. Until then I still want to add the following: - Complete recreation of mmj2's unifier: As of right now mmt1 only has mmj2's original unifier (which is only able to fill in refs given an assertion and hypotheses) - Preview unify: It would be useful to see a preview of what triggering the unifier will do within the unicode preview - A more powerful search tool: Right now mmt1's search capabilities are still very limited - mmj2's definition checker - More overall polish: More settings, less hardcoded values, some nicer styling, etc. As for the tech-stack I went with tauri 2.0 as my overarching framework, which means that most of the application is written in rust, while the ui is written using html/css/js (and displayed using the OS's webview). I also chose svelte 5 as my frontend framework to allow component based development and (as mentioned above) I went with monaco-editor as my editor. Lastly I still had a few more questions about metamath and set.mm: - What does the ! at the beginning of statements do in mmj2? I think I read somewhere that it was an undocumented change. Is anyone nevertheless able to come up with an informal description of how it impacts the unifier? - I want to be able to syntax highlight variables without having to hardcode the colors. Right now it seems the only way I can do this would be to parse the htmlvarcolor setting, which would be pretty tedious. Would it be possible to add a varcolorcode setting to the typesetting comment, which assigns a variable colorcode to a typecode? And if not: How does mmj2 derive the colors for it's syntax highlighting? Are they hardcoded? - In mmt1 the table of contents is replaced by an explorer on the left side of the screen, similar to e.g. vscode's file explorer, only with headers instead of folders. This however requires that all headers are exactly one header depth below their parent header. set.mm follows this rule in with all headers but 3 in Jim Kingdom's mathbox. Would it be ok (specifically for Jim Kingdom himself) to change the header depth of those 3 headers? I hope that asking for these changes isn't too much given that I have not yet contributed to set.mm myself. Best regards, Marlo Bruder -- 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 visit https://groups.google.com/d/msgid/metamath/b04c1858-ef29-4e89-b806-ba96aabb2397n%40googlegroups.com.
