Hi Marlo,
First of all, congratulations on starting/announcing your project!
What proof assistant are you currently using?
I also use Yamma.
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?
Maybe it's obvious, but I like the fact that it's integrated in the
VsCode IDE.
What are some things you don't like about your proof assistant that
future proof assistants should avoid?
In terms of features I'm missing, I would really like to have the
"select smallest class/wff" feature I had in Emetamath. This should not
be too hard, and I think this would be of great help.
The "one-click publish" feature you describe would be nice. With Yamma
we have to copy-paste the MMT files, a very acceptable burden ! :)
Back in 2010 I wrote a plugin for Eclipse : http://emetamath.tirix.org/
It basically encapsulated MMJ2 and offered some of these nice features:
* browsing of the database by chapters and sections,
* syntax highlighting,
* several editor panes, native search/replace, etc.,
* navigation to theorem declaration using the contextual menu,
* hover-popup with information about the symbol/theorem,
* that "select class/wff" feature I mentioned above...
I later made a video showing those features: https://youtu.be/BsEyW3vBcsE
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.
Are you using metamath-rs
<https://github.com/metamath/metamath-knife/tree/main/metamath-rs> as a
library or rewriting it from scratch? Is the project going to be open
source?
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?
This is a signal to MMJ2 that it should use the more advanced
"auto-transformation" on those steps.
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?
My solution in "Emetamath" was to add a dialog for users to choose the
colors. I'm not sure how much in common you have with vscode, but you
might be able to set extension-specific settings, using JSON files in
the project's .vscode directory.
Good luck with your project!
_
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 metamath+unsubscr...@googlegroups.com.
To view this discussion visit
https://groups.google.com/d/msgid/metamath/61ca1e20-d245-4fcf-82f0-9d20fe2f6330%40gmx.net.
