--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/ddc0991a-7f2d-4f50-92f4-e504e4f038c9n%40googlegroups.com.
--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/61681cd8-f663-4bd3-b650-06d076be97b1n%40googlegroups.com.
--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/e96ad325-e3c6-4689-9ad7-b5a25a2860a9n%40googlegroups.com.
While we're talking about unifiers, I'm still in the market for one which is api based with a thin command line wrapper.
3. A unifier api would allow a programmer to focus on the front end of a proof assistant (my personal conceit, since 2018, is that I'd like to see/write an Incredible Proof Machine (vertex-edge-graph drag and drop toy proof assistant) with a Metamath back end, and, oh, maybe a maxGraph front end).
Hey Antony,While we're talking about unifiers, I'm still in the market for one which is api based with a thin command line wrapper.
Could you elaborate on your proposal a bit? When you say "thin command line wrapper", do you mean a fully functional proof assistant (like a minimalist metamath.exe) or simply a command line tool that let's you call the proof assistant functionality (unify step, renumber, etc.)?
3. A unifier api would allow a programmer to focus on the front end of a proof assistant (my personal conceit, since 2018, is that I'd like to see/write an Incredible Proof Machine (vertex-edge-graph drag and drop toy proof assistant) with a Metamath back end, and, oh, maybe a maxGraph front end).
Another interesting proposal. Are you suggesting a drag and drop proof assistant where the proof lines are represented as vertices and hypothesis dependencies as edges? What would the advantage of such a proof assistant be in your opinion?
--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/33412bc3-bde8-489a-a69b-ed6fa7f0b958n%40googlegroups.com.
--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/33412bc3-bde8-489a-a69b-ed6fa7f0b958n%40googlegroups.com.
About an API for a proof assistant, the LSP (Language Server Protocole) is a protocole for interactions between editors/IDE's and language servers.
Language servers typically provide syntax highlighting, contextual help, code completion, etc.
Unification could simply be code completion for a partial MMP file, or a special language server command.
An advantage of this approach is that this is an industry standard, and there is a long list of editors which support them.
Just my 2c!
BR,
_
Thierry
The advantage of a client-server architecture compared to a command-line tool is that the server can perform computing intense tasks once (when started, when a file is loaded) and keep that information. A command-line tool does not have any context and might have to reload/re-parse a lot of information at each call.