All K-related tools are managed through the kup package manager. Below you will find the command to install the K framework, commands available with kup and flags that allow easy switching between different versions.
bash <(curl https://kframework.org/install)| Command | Description | Example |
|---|---|---|
kup list | List all available packages and their status | kup list |
kup install $package | Install or update a $package | kup install kontrol |
kup uninstall $package | Uninstall $package | kup uninstall kontrol |
kup shell $package | Add $package to the current shell (this is temporary) | kup shell kevm |
kup doctor | Check if kup is installed correctly | kup doctor |
kup add $package | Add a private package to kup | |
kup publish | Push a package to a cachix cache (RV developer use) | |
kup $option --help | Output the description of $option | kup list --help |
Installation time: The initial installation of certain packages (e.g., kontrol) may take longer as it needs to fetch all the libraries and compile sources. This process typically takes around 30 mins to 1 hour.
The following flags allow for the installation of different package versions and/or different dependencies versions.
| Flag | Usage | Description | Parameters | Example |
|---|---|---|---|---|
--version | kup install $package --version $version | Install/update $package with a particular $version | $version: Commit/branch/local checkout/release tag of $package | kup install kontrol --version ~/kontrol |
--override | kup install $package --override $dependency $version | Install/update $package with a particular $version of $dependency | $dependency: a dependency of $package$version: commit/branch/local checkout/release tag of $dependency | kup install kontrol --override kevm/k-framework/haskell-backend ~/haskell-backend |
As an example, let's assume we want to use kontrol with the following modifications:
- Use a local checkout of
kontrol(for example, after adding a new feature tokontrol). - Use a
haskell-backendbranch (for example, some execution improvements have not yet been upstreamed tokontrol). - Use the Github release
v0.1.461ofpyk, which includes a useful new feature.
The line below will allow us to run a version of kontrol with the above modifications:
{% code overflow="wrap" %}
kup install kontrol --version ./$path_to_local_kevm --override k-framework/haskell-backend $haskell-branch pyk ./$path_to_local_pyk{% endcode %}
As you can see, release tags, local checkouts and branches can be used to build a fine tuned version of any of our tools, kontrol being the example here. To know the exact naming of the dependencies that a package has one can use kup list $package --inputs.
Nix configuration files can be stored in many different locations. A full treatment can be found in the Nix manual. Check if you have additional Nix config files, for example in $HOME/.config/nix. If $HOME/.config/nix specifies a trusted-users option, this will override whichever trusted-users were set in /etc/nix/nix.conf. Changing the config variable from trusted-users to extra-trusted-users means it will only be appended, not overwritten. You can also explicitly set which files Nix should use as config files using the NIX_USER_CONF_FILES environment variable.
export NIX_USER_CONF_FILES = "/etc/nix/nix.conf"
kup doctor