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:
Nix does not work well with submodules. In order to copy the submodules to the Nix store, you have to explicity specify the target as "git+file://$(pwd)?submodules=1". For example, instead of nix build ., you would run nix 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.
Currently, the flake only builds the fat jar, since that is all Prusti needs. An additional package could be added in the future to the flake to build the skinny jars instead.
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.