Kontrol
  • Overview
    • Kontrol
      • The significance
      • Installations
  • Guides
    • Proofcast Episode: Getting Started
    • Kontrol Example
      • Property Verification using Kontrol
      • K Control Flow Graph (KCFG)
      • Proof Management
      • Debugging a Proof
    • Node Refutation
    • Bytecode Verification
    • Advancing Proofs
      • KEVM Lemmas
      • Writing Simplifications
      • Rule Application
      • Symbolic Storage
  • Cheatsheets
    • Kup Cheatsheet
    • Kontrol Cheatsheet
    • Cheatcodes
  • Tips
    • Debugging Failing Proofs
  • Glossary
    • Kontrol Arguments
    • Kontrol Build Options
    • Kontrol Prove Flags
  • Developer Docs
    • Digest File
  • Learn More
    • Resources
    • Example Projects
  • 🔗Links
    • Join our Discord!
    • Kontrol Repo
    • Gitbook Repo
Powered by GitBook
On this page
  • K Framework Installer
  • Install kup
  • kup commands
  • kup packages management
  • Chaining flags
  • Troubleshooting
  • Making changes to nix.conf (manually or through kup) has no effect.

Was this helpful?

Edit on GitHub
  1. Cheatsheets

Kup Cheatsheet

PreviousSymbolic StorageNextKontrol Cheatsheet

Last updated 1 year ago

Was this helpful?

K Framework Installer

All K-related tools are managed through the kup . Below you will find the command to install the K framework, commands available with kup and flags that allow easy switching between different versions.

Install kup

bash <(curl https://kframework.org/install)

kup commands

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., ) may take longer as it needs to fetch all the libraries and compile sources. This process typically takes around 30 mins to 1 hour.

kup packages management

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

Chaining flags

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 to kontrol).

  • Use a haskell-backend branch (for example, some execution improvements have not yet been upstreamed to kontrol).

  • Use the Github release v0.1.461 of pyk, which includes a useful new feature.

The line below will allow us to run a version of kontrol with the above modifications:

kup install kontrol --version ./$path_to_local_kevm --override k-framework/haskell-backend $haskell-branch pyk ./$path_to_local_pyk

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.

Troubleshooting

Making changes to nix.conf (manually or through kup) has no effect.

export NIX_USER_CONF_FILES = "/etc/nix/nix.conf"
kup doctor

configuration files can be stored in many different locations. A full treatment can be found in the . 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.

package manager
kontrol
Nix
Nix manual