Consider moving the content of this repository into https://github.com/dafny-lang/dafny

[keyboardDrummer]

Moving the .NET projects in this repository into https://github.com/dafny-lang/dafny will make it easier to refactor Dafny without breaking the language server, and make it easier to make changes to the Dafny compilation pipeline that benefit the language server, such as making compilation more incremental.

If you look at a compiler like the C# one (link) you can see that the compiler and language server are integrated into a single repository (example), and I think that makes sense because a big chunk of the compilation, basically the whole front-end of the compilation: parsing, name binding and type inference, validation, relates to the language server as well.

I don’t see significant downsides to including the language server in the Dafny repo. There will be an increase in load time of the Dafny solution, but I think in practice that shouldn’t be an issue.

[RustanLeino]

If this is helpful, I'm okay with it. I suggest it would mean that language-server-csharp would play a similar role to DafnyServer, which is currently part of dafny-lang/dafny.

Would this make it harder to set up a build environment for the combined repository?

[camrein]

I agree with you that moving the language server into the main repository has its benefits, especially keeping the codebase compatible.
However, the drawback is that the releases of the compiler and language server will most-likely be coupled. I think it's great that we can release an update to the language server without having to do so for the compiler. Although there are so few feature-requests and bug reports so far, it might not be necessary to retain this flexibility.

[keyboardDrummer]

However, the drawback is that the releases of the compiler and language server will most-likely be coupled

Is that a problem? If you make purely language server changes, like adding a refactoring or fixing a language server bug, that can be released as a patch, only incrementing the Z in the version X.Y.Z, indicating that nothing about the language specification has been changed. Changes like better error messages or a faster compilation, which affect both the compiler and language server, would also be patch releases.

One advantage I see of coupling the release of the compiler and language server is that it becomes simpler to know that both are in sync: they should be the same X.Y.Z. version.

Are you bundling the Dafny LSP server with the Dafny VSCode extension? In that case, if a customer gets an update of the extension they'll also get an update of the LSP server, and their LSP server might become out of sync with the Dafny compiler they're using.

I think it would be good to let the Dafny VSCode extension determine the language server by resolving it from $PATH. When a customer wants to use a newer Dafny they'll download the release and put both the new compiler and new language server on their path, so their compilation and editor experience remain consistent.

[camrein]

Not really a problem. Somehow it seems to work for the .NET Compiler Platform too.
I agree that it's definitely easier to see that the installed versions should be compatible when they are meant to have the same version string. So feel free to merge this repository into the main repository. 👍

Not really bundling. When releasing an update to the VS Code extension, I raise the minimum required version string to the one of the latest language server. The extension then checks if the currently installed version is at least this version. If that's not the case, it'll download and install it. Moreover, the compiler is bundled with the language server that is distributed. It'll only become out-of-sync if the user manually specifies a custom installation in the settings (side-note: the compiler version is not enforced the way it is for the language server).

It's surely convenient for the users to place their dafny installation somewhere on the path. But I think the currently provided ability to configure the installation locations manually is sufficient.

Edit: If you wish, I can prepare a PR on the main repo.

[camrein]

Do you have any news on this? I'd like to release a new update - but this would lead to the situation that the language server will then have a different version than the compiler. I could release the current update as a "bug-fix" version (e.g. v3.0.1, even if it includes a new feature), reducing the impact.

[RustanLeino]

It would be great to get the updated VS Code. Besides, it's been over 2 months since the Dafny 3.0.0 release, so releasing an updated Dafny seems a good idea.

I will merge the PRs that are ready to go and will plan to release a Dafny 3.1.0 on Monday or Tuesday. Does that work with you?

[camrein]

That sounds good. Does this mean that we will postpone the merger of this repository into the dafny-lang one? Otherwise, I could file a new PR to include the language server. This would also help solve issue #51 as the Dafny source will no longer be pinned to a certain commit.

[keyboardDrummer]

Otherwise, I could file a new PR to include the language server.

That sounds like a good idea to me. Apart from the ease of development benefits we can think of and concrete issues that this would resolve, this also seems to be the industry standard. Other compilers repositories like TypeScript, Roslyn and Scala 3 also include the language server. Any objections @RustanLeino ?

I'm also guessing that https://github.com/dafny-lang/dafny/tree/master/Source/DafnyServer becomes obsolete once this repository is merged into the Dafny one, right?

[camrein]

Excellent. I have prepared a branch with the repository merger and some relocations of the files. Unfortunately, I cannot push a branch to dafny-lang/dafny. Would you mind giving me access, or should I use another method?

About DafnyServer: The decision is up to you. As far as I know, DafnyServer works similarly to a REPL console. I don't know if there's any need for that (the new VSCode plugin no longer uses it). But DafnyLS makes use of some files from there which would need to be moved somewhere else in case of DafnyServer's removal.

[keyboardDrummer]

Unfortunately, I cannot push a branch to dafny-lang/dafny. Would you mind giving me access, or should I use another method?

Why not make a pull request from a branch in a repository you can commit to, to dafny/master? I'm a bit confused as to why that's not an option.

Would you mind giving me access

I can't, so I'll leave that up to @RustanLeino

[RustanLeino]

@camrein I gave you Write access. Please push your branch and make a PR for it. (Alternatively, I think you should be able to make a PR from wherever that branch is sitting. That's how I do my PRs.)

DafnyServer is still used by the emacs mode. Maybe we can combine them in some way in the future.