Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Currently, the Prusti repo has a Nix flake, but this flake does not work because it downloads Viper from the download link. This means that whenever a new version of Viper is released and the SHA256 hash changes, the Prusti flake will fail to build. By introducing a flake in the Viper repository as well, the Prusti flake will be able to refer to a specific version of Viper, and a new release of Viper will not break the Prusti flake.
Notes:
"git+file://$(pwd)?submodules=1"
. For example, instead ofnix build .
, you would runnix build "git+file://$(pwd)?submodules=1"
. In the future, if Viper were to switch to using Nix for all development and CI, the submodules could be removed and instead the Carbon, Silicon, and Silver repositories could be used as flake inputs, removing the need for this.nix develop "git+file://$(pwd)?submodules=1"
opens a development shell with sbt and JDK 11 in the PATH, and the Z3_EXE and BOOGIE_EXE environment variables are set.