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

Configure Prusti arguments and environment variables #139

Merged
merged 6 commits into from
Feb 2, 2022

Conversation

fpoli
Copy link
Member

@fpoli fpoli commented Feb 1, 2022

In this PR:

  • Add configuration options to let the user specify extra arguments and environment variables to be used when running prusti-rustc, cargo-prusti and prusti-server. This mitigates Allow configuring the server #62.
  • Make the prusti-server start in the first folder of the workspace. This way, if the user enables PRUSTI_DUMP_VIPER_PROGRAM, the dump will end up in the workspace and not in some obscure folder of VS Code.

I haven't added a way to test that the new configuration options work as intended. I just tested them locally.

@fpoli fpoli self-assigned this Feb 1, 2022
@fpoli fpoli requested a review from JonasAlaif February 1, 2022 14:17
src/diagnostics.ts Show resolved Hide resolved
src/server.ts Outdated
util.log(`Prusti server will be executed in '${prustiServerCwd}'`);
}

const prustiServerArgs = ["--port", "0"].concat(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Again, we could move the --port setting to extraPrustiServerArgs instead of hardcoding it?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you see a use case for letting the user choose the port?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not really, but I don't see much of a reason for the --port setting in the first place aha

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah :D We could at least make 0 the default.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Makes sense, in that case we can merge as is

@fpoli
Copy link
Member Author

fpoli commented Feb 1, 2022

Mmm, for some reason the prusti-server keeps failing on Windows.

@JonasAlaif
Copy link
Contributor

When I run the test on Windows I get:

Prusti server will be executed in '/C:/Users/Jonas/AppData/Local/Temp/tmp-8312-lLQef3cvi7GF'
[Prusti server] Start "c:\Users\Jonas\AppData\Roaming\Code\User\globalStorage\viper-admin.prusti-assistant\prustiTools\LatestDev\prusti\prusti-server.exe --port 0"
[Prusti server] Mark server as "Running".
[Prusti server] Server process error: Error: spawn c:\Users\Jonas\AppData\Roaming\Code\User\globalStorage\viper-admin.prusti-assistant\prustiTools\LatestDev\prusti\prusti-server.exe ENOENT

As the output in Prusti Assistant Trace. It would be nice to display this output in the CI

@JonasAlaif
Copy link
Contributor

I think that the error is caused by the leading / in /C:/Users/Jonas/AppData/Local/Temp/tmp-8312-lLQef3cvi7GF

@fpoli fpoli force-pushed the extra-env-and-args branch from 9c3ad25 to 0b6212c Compare February 2, 2022 10:41
@fpoli
Copy link
Member Author

fpoli commented Feb 2, 2022

I think that the error is caused by the leading / in /C:/Users/Jonas/AppData/Local/Temp/tmp-8312-lLQef3cvi7GF

Thanks! Apparently, for disk operations one must use Uri::fsPath instead of Uri::path.

I added plenty of log to the console. Debugging should be easier.

@JonasAlaif
Copy link
Contributor

Hahaha, this github CI on all 3 platforms is invaluable

@fpoli fpoli merged commit 15e4353 into master Feb 2, 2022
@fpoli fpoli deleted the extra-env-and-args branch February 2, 2022 14:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants