Yes, a language server does sound like the best approach. I'm trying to
aim for the simplest.
Glauco - thank you very much for your help with that - sorry, I meant to
say sooner - I got that working OK, but haven't got much further. Am
planning on working on that this weekend.
Best regards,
Antony
On Fri, Oct 10, 2025 at 3:49 PM Thierry Arnoux <[email protected]>
wrote:
> 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/CAJ48g%2BAtLSg1bLOr20RqUr8P-bdG31QsLKWXZkYk_EzqfsGEKg%40mail.gmail.com.
