Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Viper IDE refactoring: Settings #115

Closed
WissenIstNacht opened this issue Oct 22, 2020 · 0 comments · Fixed by #113
Closed

Viper IDE refactoring: Settings #115

WissenIstNacht opened this issue Oct 22, 2020 · 0 comments · Fixed by #113
Labels

Comments

@WissenIstNacht
Copy link

WissenIstNacht commented Oct 22, 2020

This issue pertains to the ongoing refactoring process #113.

Viper IDE had a nubmer of settings describing various parameters (paths to tools used by the extension, which verification engine to use, timeouts, backend options, etc.). With the current refactoring of Viper IDE, the responsible code will be removed. It should therefore be reimplemented in the refactored version of this codebase.

A description of the settings' structure can currently be found here:

export interface ViperSettings {

However, with the refactoring of Viper IDE, this structure of settings is outdated. For example, there is no more need to set a verification engine. The refactored version of Viper IDE uses exactly one engine (namely, ViperServer running in language server mode). Another example related to this is that the use of stages is no longer necessary.

We therefore want to propose a restructuring of the settings. These restructured settings should then be synced with the refactored language server (i.e., ViperServer running in language server mode). This should allow the backend to be run with user-specified options (e.g. backend-specific cache, # of active jobs, timeouts, options for Silicon/Carbon, etc.), instead of the hard-coded parameters currently used.

Note that the counterpart of ViperProtocol.ts in ViperServer is called DataProtocol.scala. The structures of the settings in both files should be kept in sync. This will allow the communication of the setting between client and server using LSP.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants