Build K, KEVM, and Both Backends

[ehildenb]

From a fresh clone of KEVM, we should be able to build it from source. This means these commands work:

git clone 'https://github.com/kframework/evm-semantics'
cd evm-semantics
git submodule update --init --recursive
make deps RELEASE=true -j8
make build RELEASE=true -j8

Following the build instructions above ^^^, you should make sure that you can also run some of the tests:

make test-conformance -j8 # llvm backend
make test-prove -j8 TEST_SYMBOLIC_BACKEND=haskell # haskell backend
make test-prove -j8 TEST_SYMBOLIC_BACKEND=java # java backend

Raoul

• Build dependencies and semantics (make deps and make build).
• Run the concrete tests (make test-conformance)
• Run the symbolic tests (make test-prove).

[ehildenb]

If you're on a Mac #1022

On Windows, use WSL2.

[ehildenb]

We do have a binary cache for the Nix packages, which it would be good to try, to make sure we have a larger bus factor than 1.

@andreiburdusa can you point us to the instructions for setting up the binary cache?

[ehildenb]

We'll leave this one open, for when @RaoulSchaffranek gets his new machine. Then we can try the Nix version of the install again.

[andreiburdusa]

We do have a binary cache for the Nix packages, which it would be good to try, to make sure we have a larger bus factor than 1.

@andreiburdusa can you point us to the instructions for setting up the binary cache?

For kore, we have these instructions linked from Developing with Nix. Is this what you are looking for?

[ehildenb]

Will that same binary cache also work for the K repo Nix build, or just Kore @andreiburdusa ?

[andreiburdusa]

Will that same binary cache also work for the K repo Nix build, or just Kore @andreiburdusa ?

andrei@q:~/k$ nix-build -A k
copying path '/nix/store/k7mnwba0x8bvdh7rplx93wwf4559sg2l-kore-stack-to-nix-pkgs' from 'https://kore.cachix.org'...
building '/nix/store/7r9djpy19zkifqzp286l0m5bj65ysl5n-git-ls-files.drv'...
building '/nix/store/k2xyx7n8fqr0dpql221cv32qz2w0k4f2-git-ls-files.drv'...
...

The first output line makes me think it works for K as well, but I'm not entirely sure

[RaoulSchaffranek]

Thanks, everybody. The binary cache solved my problem, namely that nix-build built everything (including GHC and Cabal) from source. I can confirm, that the binary cache also works for the k frontend.

I think it would be a good idea to mention the binary cache in the Building with Nix section of the K-frontend Readme file. Otherwise building with Nix can take hours. I will prepare a PR.