search

runtimeverification / wasm-semantics

A Prototype Formal Semantics of WebAssembly in K
Other
74 stars 18 forks source link

Migrate build to `kdist` #605

Closed tothtamas28 closed 3 months ago

tothtamas28 commented 3 months ago
tothtamas28 commented 3 months ago
  1. How do I kompile a semantics from the command line?

Using the kdist build command (through poetry run), e.g:

kdist build wasm-semantics.llvm
kdist build -j2 wasm-semantics.kwasm-lemmas wasm-semantics.wrc20
kdist -v build -j4 wasm-semantics.*
  1. How do I kompile a semantics from python?

The simplest way is through the kdist object:

from pyk.kdist import kdist

kdist.build(['wasm-semantics.llvm'])
kdist.get('wasm-semantics.llvm')
  1. If I am developing the mx-backend, and I need to quickly test a change in the wasm-semantics, I can currently just go to the submodule, change it, and recompile. Is it the same with kdist?

Right now, the submodule-based solution should still work. Eventually though, I'd like to eliminate the submodule and replace it with a Python dependency.

In that case, you'd clone this repository, and replace the dependency in mx-semantics/.../pyproject.toml with a path dependency:

wasm-semantics = { path = "<path-to-wasm-semantics>/pykwasm", develop = true }

and work with it as if it were a submodule.

  1. Does kdist recompile the semantics only if it changed? I assume this is so, but it is safer to ask.

Right now, it is set up so that a change in any of the K files, as well as a change in K version triggers build. This can be further customized though.