search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.89k stars 258 forks source link

Language Server: Relocate prover options #1453

Open camrein opened 3 years ago

camrein commented 3 years ago

Currently, the prover options of the language server are tied to the setting --document:proveroptions (DocumentOptions class). For me, it sounds like settings that are relevant for the verification, especially because it's an option coming from boogie. Therefore, I wonder if it's more suitable to relocate this option to --verifier:proveroptions (VerifierOptions class). Currently, we have the option to set the verification time limit and the number of virtual cores there. Since this feature is not yet part of a Dafny release, I think we're safe to rename this option.

@Dargones If I remember right, you have integrated this feature. What is your opinion about this?

keyboardDrummer commented 3 years ago

Can you refresh my memory: why do the Dafny language server and CLI not share many of the same options, and style of configuring those options?

camrein commented 3 years ago

In contrast to the CLI, the language server uses .NET Cores options style for configurations: https://github.com/dafny-lang/dafny/blob/90eb1084d9862384accd03fb5a1c8af500212a05/Source/DafnyLanguageServer/Program.cs#L33-L38 This allows injecting settings through the IOptions interface where needed. It drastically improves the testability over the statically configured DafnyOptions class the CLI uses. Unfortunately, some options are relevant to the compiler so the CLI options have to be configured through the DafnyOptions class as well. We could straightforwardly apply the compiler-relevant settings just as the CLI. But there are some settings that must not be changed (or have to be reset after applying the user settings). For example ModelViewFile has to be -. Moreover, we start mixing different options: Compiler options and language server-only options (e.g., the automatic verification).

keyboardDrummer commented 3 years ago

I'd like to have an interface ILanguageServerOptions that makes it clear what options the language server can except, and that could inherit from similar Options interfaces defined by the Dafny compiler. The AddCommandLine and AddJsonFile of ConfigurationBuilder are nice but I think there's value in keeping the format of arguments the same as in the Dafny CLI. We could create our own DafnyCommandLineArguments implementation of IConfigurationSource.

Anyways, none of the above is urgent, we can think more about it later.

Dargones commented 3 years ago

I think these could be moved to VerifierOptions provided that these additional proverOptions are injected by default whenever the server tries to verify something. The reason for this difference with CLI is that the Language Server needs a full uncompressed Z3 model to extract a counterexample out of it. Speaking of which, I have also added a CounterExampleDepth option to the CounterExampleParams class but I am not sure how to specify this argument when running the language server.

camrein commented 3 years ago

Thanks for the confirmation, that we could move this setting to VerifierOptions.

Speaking of which, I have also added a CounterExampleDepth option to the CounterExampleParams class but I am not sure how to specify this argument when running the language server.

These Params classes are requests the language client sends. At this time, this is mostly Dafny VSCode. With the re-design of the extension, I ensured that we have a clean counterpart to the language server interfaces. For example, for CounterExampleParams that would be ICounterExampleParams. The API is provided by DafnyLanguageClient and used by CounterExamplesView. Speaking of this I'm wondering now: Did you intend to expose the capability to change the CounterExampleDepth for every requested counterexample? Or did you want to make it configurable as you did with proveroptions? If it's the latter, I could refactor it accordingly or guide you on how to do it.

Dargones commented 3 years ago

My apologies for the slow response, @camrein ! The intention was to make this option configurable for any requested counterexample. Should I do any refactoring in this case? I know that right know CounterExampleDepth is essentially a constant since it cannot changed from within Visual Studio Code but I thought defining this variable in the CounterExampleParams class would make it easier to make it configurable, if necessary.

camrein commented 3 years ago

If you think it's useful to enable users to configure the counterexample depth per document, then you can leave it there. I can add a prompt to VSCode asking to enter the desired depth when displaying the counterexamples. If, on the other hand, it's more reasonable to configure it once for all, it makes sense to change it to a language server option. Then you can set it similarly to the options as described in the language server's README.

Dargones commented 3 years ago

I think it makes more sense to make the setting configurable per counterexample. This way, if you have several files open, you don't have to restart the server to change the depth in one particular case. That said, this setting might become obsolete if a new way of displaying nested counterexample is introduced.