Some background: I am using Dafny through https://github.com/boogie-org/boogie-friends, which requires DafnyLanguageServer version <= 3.9.0, where function syntax 3 is still the default.
Can I change the functionSyntax setting when I am not using the CLI application but DafnyLanguageServer? The documentation is silent on this topic.
The DafnyOptions type, where the functionSyntax option can be found, is used in Source/DafnyLanguageServer, but if I can derive from this how to pass the functionSyntax option to DafnyLanguageServer, then I'm not knowledgeable enough to understand.
Seeing that DafnyLanguageServer takes parameters like --verifier:timelimit=0, I tried to pass --verifier:functionSyntax=4, --functionSyntax=4 and --verifier:functionSytax:4 which didn't work. Since here I found functionSyntax in the "ParserOptions" instead of the "VerificationOptions" I also guessed --parser:functionSyntax=4, but, of course, that didn't work either.
I also found the DafnyLanguageServer.appsettings.json that is mentioned in the documentation, but there I didn't find a functionSyntax setting either.
I would like to avoid adding {:options "-functionSyntax:4"} to all my files. Unless this is considered a best practice?
At the time of writing, Dafny developers recommend using dafny server (instead of DafnyServer), which is a Language Server Protocol implementation.
Section 14.3 "The Dafny Server" of the Dafny documentation explains that DafnyServer was developed before the Language Server implementation. It uses its own protocol to communicate with Emacs.
As of 2024/01/05, the documentation says
The Dafny Server is still supported, but we recommend using the Language Server instead.
but DafnyServer does not support some recent Dafny features.
As a result, the developers clarified the documentation:
While the latest Dafny releases still contain a working DafnyServer binary, this component has been feature frozen since 2022, and it may not support features that were added to Dafny after that time. We do not recommend using it.
So it seems to me that you can't configure the function syntax version with DafnyServer and that it won't be supported in the future either. There may be a way to do it that I haven't discovered, but the more time passes, the more irrelevant DafnyServer becomes.
But actually the question is about "DafnyLanguageServer", not about "DafnyServer". The DafnyLanguageServer executable has been removed from the Dafny releases sometime between 3.9 and 4.4.
14. Dafny VSCode extension and the Dafny Language Server links to the DafnyLanguageServer source, so I assume that the DafnyLanguageServer code is now used by the dafny server command. I was able to confirm that dafny server can be used in place of DafnyLanguageServer in boogie-friends' lsp-dafny.el: https://github.com/boogie-org/boogie-friends/pull/41
To summarize: Probably neither DafnyServer nor DafnyLanguageServer can be configured in the way I hoped. But both are "feature frozen" or already removed from releases, so this part of the question becomes more and more irrelevant as time passes.
More generally I would also like to know whether even more of the options of the dafny CLI (
--manual-lemma-induction,--disable-nonlinear-arithmeticetc.) can be passed to the lsp server
The "forward path" of Dafny Language Protocol Servers, i.e. dafny server, fully supports all of those options, both when passed on the command line and via project files (dfyconfig.yaml).