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

Install Prusti offline #213

Open
champignoom opened this issue Feb 15, 2023 · 2 comments
Open

Install Prusti offline #213

champignoom opened this issue Feb 15, 2023 · 2 comments
Labels
enhancement New feature or request

Comments

@champignoom
Copy link

champignoom commented Feb 15, 2023

Steps to reprodce:

  1. open some rust file in vscode
  2. vscode shows "Installing Prusti"
  3. and it never finishes

The problem is partly my network and proxy settings, which does not work very well the default installation script.

It would be nice if one can download and install prusti manually and then configure it in vscode offline.

I tried building prusti and putting path/to/prusti-dev/target/release in "Local Prusti Path" but it seems to be simply ignored without any diagnostics.

@fpoli fpoli added the enhancement New feature or request label Mar 1, 2023
@fpoli fpoli changed the title manually install prusti Install Prusti offline Mar 1, 2023
@fpoli
Copy link
Member

fpoli commented Mar 1, 2023

When setting prusti-assistant.localPrustiPath, did you also set prusti-assistant.buildChannel to Local?

The prusti-assistant.localPrustiPath cannot just point to prusti-dev/target/release; it should point to some folder /path/to/foobar that has been populated with prusti-dev/x.py package release /path/to/foobar to properly include all the Z3 and Viper dependiencies.

@fpoli
Copy link
Member

fpoli commented Mar 1, 2023

  • We should make sure that it's possible to switch to the Local build channel even when the first activation happens offline or with a slow connection.
  • The readme should describe the localPrustiPath setting and its requirements.

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

No branches or pull requests

2 participants