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
<https://microsoft.github.io/language-server-protocol/implementors/tools/>
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.
On 30/09/2025 09:17, Antony Bartlett wrote:
Sorry to anyone I confused by saying .uue when I meant .mmp, or misled
by referring to yamma's platform (JavaScript) rather than its
programming language (TypeScript).
Glauco made the excellent suggestion that I code a spec for this, and
I am in the process of writing it. We first discussed the possibility
of spinning off a unifier component from yamma at the end of 2022, I
believe, so I don't have any sense of urgency at all about wanting
this api if you are busy.
Best regards,
Antony
--
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/7812b244-aec8-432b-ba1c-3c972e21f74a%40gmx.net.
