Error when updating settings file (using "advanced" version of the plugin)

viper-admin commented 8 years ago

Created by @alexanderjsummers on 2016-09-19 22:12 Last updated on 2016-09-26 18:33

I tried updating the plugin on my machine, since the version that I had doesn't seem to work with the latest Silicon. I took the "advanced" version from VSCode.

After manually updating the paths to the silicon and carbon jars (as well as the path to Z3) I get the following message at the top:

Viper: Invalid settings: 1 Error: Path to Viper Tools: path not found: "$defaultViperToolsPath$" which expands to "C:\Program Files (x86)\Viper" undefined

I don't see a setting with this name - it's not clear what to do next.

viper-admin commented 8 years ago

@alexanderjsummers commented on 2016-09-19 22:19

If one clicks on the buttons to open the settings, a new message appears:

Viper: Only if a folder is opened, the workspace settings can be accessed.

viper-admin commented 8 years ago

Bitbucket user rukaelin commented on 2016-09-20 09:09

I have changed the structure of the settings quite much, I suggest copying the new default settings and modifying them again. For ease of installation we decided to use one folder containing all Viper files. If you want to use another location for some of the files you can of course also change their paths in the settings. the default path for this folder is "C:\Program Files (x86)\Viper" The reason you don't see the ViperToolsPath setting, is that it's in the default settings.

There are two kinds of settings, userSettings and WorkspaceSettings. The user settings are valid for the user, no matter what directory is open, whereas the workspaceSettings only hold for one folder. If you only opened a file but not a folder, it would be insensible to use workspaceSettings.

viper-admin commented 8 years ago

@aterga commented on 2016-09-20 10:09

@alexanderjsummers I agree with Ruben that the best solution right now is to remove all previously changed User Settings (so that the default ones provided with the current version of the extension would apply). You could do that by just removing all the contents and saving the User Settings file (File > Preferences > User Settings).

Then, just unzip the archive ( https://polybox.ethz.ch/index.php/s/gNSAf2FmWn7kmt3 ) into the following folder: "C:\Program Files (x86)\Viper".

rukaelin I think Alex meant that the complaint about workspace settings appears when one clicks on the button in the ViperIDE pop-up, which is supposed to lead to the right settings file. If that's the case, could we do something about that? Could it be the wrong interface for the button is used at the moment?

viper-admin commented 8 years ago

@alexanderjsummers commented on 2016-09-21 22:09

Thanks for the extra info. With respect to the last comment, indeed, the "Open Workspace Settings" button leads to a message: "Viper: Only if a folder is opened, the workspace settings can be accessed."

I'd like to understand how to point the settings at other versions of the tools (on my machine). It seems that deleting the user settings file would mean that I lose the names of various settings (and I don't know where to find them again).

I tried updating the plugin (via VSCode for now) and had a look at the instructions (which seem clearer than in the last version, so that's good!), but I think the line "You cannot change the default setting, but have to copy the default viperSettings to your own settings." needs some clarification. It's not clear to me from this where (if anywhere) I can read the default settings, or explicitly what to do once I have an empty user settings file and want to change something.

viper-admin commented 8 years ago

Bitbucket user rukaelin commented on 2016-09-22 07:46

deleting the user settings only removes your personal settings. you cannot delete the default settings. For all settings you specify, VS Code is just using yours instead of the default settings. The default settings open up together with your settings. Open the command palette (F1), type settings, and select open user settings from the dropdown menu to open the default settings.

viper-admin commented 8 years ago

@aterga commented on 2016-09-22 11:57

Here is an attempt to a better explanation of how Code's settings work.

Both the default settings for VS Code and the default settings for Viper extension are stored in a read-only JSON text file.
Customizing the settings is done via modifying the User Settings file, in which some of the settings from the default file could be overwritten. The structure should be the same in both files, but one only needs to mention the parameters which are to be changed (not all of them). For example, here is a fragment of the default settings for the Viper extension. You can see them on the left panel if you go to File→Preferences→User Settings.
```
#!json
{
    ...
    "viperSettings.viperToolsPath": "$defaultViperToolsPath$",
    "viperSettings.nailgunSettings": {
        "serverJar": "$viperTools$/nailgun/nailgun.jar",
        "clientExecutable": "$viperTools$/nailgun/ng",
        "port": "7654",
        "timeout": 3000
    }
    ...
}
```
If one would be to change, say, the prefix for Viper's binary dependencies, one would need to copy the relevant settings into the User Settings file (the tab on the right, called just settings.json). The User Settings could then look like this:
```
#!json
{
    "viperSettings.viperToolsPath": "C:\VerificationTools\Viper"
}
```
Another example: if (in addition to the previous customization) one would also like to change the Nailgun port from the default value of 7654 to, say, 8765, here is what the User Settings would look like:
```
#!json
{
    "viperSettings.viperToolsPath": "C:\VerificationTools\Viper",
    "viperSettings.nailgunSettings": {
        "serverJar": "$viperTools$/nailgun/nailgun.jar",
        "clientExecutable": "$viperTools$/nailgun/ng",
        "port": "8765",
        "timeout": 3000
    }
}
```
In this case, one should copy the entire viperSettings.nailgunSettings settings object from the Default Settings into the User Settings, and then change the relevant fields.

The same technique allows to specify any number of verification back-ends. A verification back-end corresponds to a sequence of actions which take place after the verification command (binding to F5) is executed (by-default, this happens automatically while you change the sources). The action might be simple, e.g., running Silicon on the opened file, but it might include other stages, too. A stage corresponds to any command line tool which one might want to run at any order with other stages which together describe a particular back-end.

The list of back-ends is stored under the key viperSettings.verificationBackends in the settings files. Three back-ends are specified in the Default Settings file:
```
#!json
{
    ...
    "viperSettings.verificationBackends": [
        {
            "name": "silicon"
            ...
        },
        {
            "name": "silicon with infer",
            ...
        },
        {
            "name": "carbon_no_nailgun",
            ...
        }
    ]
    ...
}
```
These three back-ends demonstrate how different things could be achieved via customizing the back-end stages.
- The backend named silicon uses Nailgun to call Silicon's main method in viper.silicon.SiliconRunner. It only has one stage, called verify. This is the standard way of using the IDE with Silicon.
- In contrast, the backend named silicon with infer has two stages:
```
#!json
{
    "name": "silicon with infer",
    ...
    "stages": [
        {
            "name": "verify",
            ...
            "onVerificationError": "infer"
        },
        {
            "name": "infer",
            ...
            "onSuccess": "verify"
        }
    ]
    ...
}
...
```
  Note how the stages interaction is encoded via the on[EventName] attributes. This way, infer stage is only called if a verification error happens, and after inference is done we call verify stage again. Of course, the Viper IDE extension makes sure that we don't get an infinite loop between these stages.
- Finally, we include the back-end called carbon_no_nailgun in order to demonstrate how the IDE could be used without Nailgun (which is inadvisable):
```
#!json
{
    "name": "carbon_no_nailgun",
    ...
    "useNailgun": false,
    ...
}
...
```
Finally, there is a third possible location for storing settings, called Workspace Settings. The file is accessible through the menu: File→Preferences→Workspace Settings. These settings are meant to be specific for each project, and in terms of VS Code a project is defined by it's main folder, called Workspace. The structure of this file is exactly the same as the structure of Default Settings and User Settings, but Workspace Settings have top priority.

rukaelin, for our purposes, there is no need to modify the Workspace settings. However, the button in the pop-up (described above by Alex) leads here. We should change this, so that when the extension detects invalid User Settings, the button leads to the right place (which is, User Settings).

@alexanderjsummers I'd like to understand how to point the settings at other versions of the tools (on my machine). It seems that deleting the user settings file would mean that I lose the names of various settings (and I don't know where to find them again).

Does the above answer your question?

viper-admin commented 8 years ago

@aterga commented on 2016-09-22 11:59

Also, please see the simple installation steps in the corresponding section in our documentation: https://bitbucket.org/viperproject/viper-ide/wiki/Home

viper-admin commented 8 years ago

Bitbucket user rukaelin commented on 2016-09-22 13:08

Unfortunately there is no way of telling where the settings come from, I cannot distinguish default from user settings, nor user settings from workspace settings. Therefore, I am showing two buttons, one leading to the user settings and one leading to the workspace settings.

viper-admin commented 8 years ago

Bitbucket user rukaelin commented on 2016-09-26 07:56

In version 0.2.14 the user is warned if he is using old settings.

viper-admin commented 8 years ago

@alexanderjsummers commented on 2016-09-26 11:57

Hi again. Thanks a lot for all of the info. One thing that confused me before was that I never saw the default settings. It turns out that if you click on "User Settings" directly to the right of the related error-message, then only that file is opened - not the default one. This is why I didn't really understand the instructions to copy settings, etc. before. Thanks to a little help from Arshavir this morning, the plugin now works on my new laptop :)

viper-admin commented 8 years ago

@aterga on 2016-09-26 18:33:

changed state from new to resolved

viperproject / viper-ide

Error when updating settings file (using "advanced" version of the plugin) #33

Here is an attempt to a better explanation of how Code's settings work.