Merge the LSP server into Lambdapi.

[rlepigre]

What do you think about that @fblanqui & @ejgallego?

[fblanqui]

Don't forget the doc: structure.md and ui.md.

[fblanqui]

As all LSP files are prefixed by lsp_, why not putting every thing in src/ and remove src/lsp/?

[rlepigre]

That's what I wanted to do at first, but for some reason there already is a pure directory. So why not split the files among several directories? We are starting to get many files in there anyway.

[fblanqui]

It is not very convenient... pure.ml could be moved in src/ too... I feel that it is still manageable but I would be happy to hear other opinions.

[rlepigre]

Let's see what @ejgallego has to say on that. Personally I don't mind flattening the directories and removing all the library stuff we build using dune to only produce the main executable. But in that case, what should we do with Emilio's change log and README?

[fblanqui]

We could postfix them by LSP.

[rlepigre]

I would rather move the contents to the doc, and extend the main README with minimal information on how to use the LSP server. For the change log, I would simply remove it, or turn it into a change log for the whole project.

[fblanqui]

I am fine with this PR. @ejgallego is it fine for you too?

[ejgallego]

I am not sure this is a good idea. If the main motivation is to avoid the Marshall problem then IMHO that's the wrong solution for that particular problem.

My main worry is that LSP is designed to handle whole projects and the next iteration will bring many external dependencies such as Lwt and other OCaml libraries [1]; I tend to think that it is useful to still have a simpler command line interface to the core proof engine. Also, there is little that can be shared among a full-fledged LSP server and a command-line serial checker.

[1] Dune supports very well the scenario where you have a single common tree but many different packages.

[rlepigre]

Sure, this definitely is not the right solution for the Marshall problem. However I think it is not a bad idea to only have one binary anyway. Ideally, things like the LSP server, the legacy parser or the external termination checker interface would be made into plugins.

[ejgallego]

However I think it is not a bad idea to only have one binary anyway. Ideally, things like the LSP server, the legacy parser or the external termination checker interface would be made into plugins.

I dunno; do you think we gain something from plugins? What is the problem of having more than one binary? In Coq we did move in the opposite direction and made the IDE servers standalone binaries as the plugin architecture was getting more complex and it also has some other problems, [i.e. ocamldebug] tho you have Fl_dynload to alleviate some of the pains, such as locating the plugins themselves.

We found that language servers don't usually share, for example, the same command line parameters, and other questions as for example process management tend to be different [for example keep in mind that a single LSP server has to manage a set of .lp files, spawning multiple processes, etc...]

Another issue is that having two binaries allows for a tad more of independence in terms of release schedule / compatibility, but indeed overall what to do boils down to almost personal preference.

[rlepigre]

I don't know about plugins, it is hard to say what is the right way to do things. Anyway, that's not our most pressing problem. So I still think that merging this PR is a good, short-term way to solve the current issues. But I let you decide where you want to go with this @fblanqui and @ejgallego. Feel free to merge or to close.

[ejgallego]

I'd say let's hold the merge for now:

• as outlined above, the next iteration of the server using Lwt will likely undo this PR due to a really different architecture
• i'd like to process [lsp] Add vscode plugin with goal display support #240 first and this will conflict.

[fblanqui]

A simple temporary alternative would be to add an option to LP, for instance --ignore-obj (or --force) so that it ignores existing .lpo files and recompile everything. What do you think @rlepigre and @ejgallego ?

[rlepigre]

A simple temporary alternative would be to add an option to LP, for instance --ignore-obj (or --force) so that it ignores existing .lpo files and recompile everything. What do you think @rlepigre and @ejgallego ?

I'm not a big fan of overwriting the user's files without their explicit consent. If you don't want object files you can already decide not to opt-in for them (by not giving --gen-obj in the first place).

[fblanqui]

I am not saying that we should overwrite lpo files but just that we could ignore them and reparse everything instead. This is not a definitive solution of course but should allow the use of vscode with multiple files before finding a better solution.

[rlepigre]

I am not saying that we should overwrite lpo files but just that we could ignore them and reparse everything instead. This is not a definitive solution of course but should allow the use of vscode with multiple files before finding a better solution.

If we are going for a short term solution, why not use mine then? I think it makes most sense. That would solve the problem, and also solve another minor problem: lp-lsp is not a great name since it is hard to link to Lambdapi.

[ejgallego]

Indeed I think we could have lp-lsp to set a flag so object files are ignored [for now].

About the name, I tend to use very short names, if you like lambdapi-lsp better please go for it.