Nix devshell

[Asqiir]

I created a nix devshell for the project.

Features/what is this for?

For anybody who uses the nix (or lix) package manager (with the nix3-commands and flakes features enabled) and wishes to use verus without installing all the programs (z3 and its settings, rustup and its settings, vargo, ...) system wide.

How to use it

You need to install that package manager beforehand.

• a dev shell is an environment that contains all the dependencies for the project. It is an environment for developing the project. Enter it with nix develop. This is especially useful for collaborative coding, since everybody gets the same setup very easily.
• I packaged vargo. The package can be installed or made accessible in a nix shell. Known drawback: it only works when rustup is installed on the system.

Known limitations:

• vargo calls rustup, therefore directories ~/.cargo and ~/.rustup will be modified. Yes, that are the folders in the users home.
• the hash check during cargo build is removed. This might lead to harder-to-find errors later on
• the z3 version is hardcoded. If it's updated in the project, it also needs to be updated here.

Open questions

• The flake.nix is usually in the project root, but I can move the other files that I added. Where should they go?
• What is up with pub const EXPECTED_CVC5_VERSION: &str = "1.1.2";? As far as I can see, this does not reference any program that is installed in the background (according to the install guide).

[parno]

What is up with pub const EXPECTED_CVC5_VERSION: &str = "1.1.2";?

We recently added experimental support for using cvc5 as a backend. It's not needed to use Z3, nor do we expect most Verus users to use this support (or install cvc5) at present.

[Asqiir]

Ok. What is the variable called where verus expects the executable to be? (I can't see it in the installation docs.)

[parno]

It follows the same procedure as for Z3 (i.e., it will look in the same directory as the verus executable, check the VERUS_CVC5_PATH environment variable, etc.). But this feature isn't stable and might never be (which is why it isn't in the installation docs), so I think you might want to hold off on adding it to the devshell for now.

[Asqiir]

So, normally, the devshell would be intended for developping verus, so it would make sense.
But since it's currently kind of impossible to just package verus for just using it, the devshell picks up the additional task here.
I could create two different devshells for the task, or I can just add cvc5 to the main one, just in case someone uses it.

[parno]

Ah, okay, sounds good.