Integrate rust repository as a git submodule
#8
Comments
jberthold
added a commit
to runtimeverification/mir-semantics
that referenced
this issue
Sep 8, 2024
This PR adds a set of simple rust programs (from prior art) for a simple parser test: * salvages [old test programs from `run-rs` in the `textual-mir` branch](https://github.com/runtimeverification/mir-semantics/tree/textual-mir/kmir/src/tests/integration/test-data/run-rs) * [sets up `smir_pretty`](https://github.com/runtimeverification/smir_pretty) as a submodule for integration tests * adds `make` targets to manage the submodule build (including a bootstrap of `rustc`, which [should be set up as a recursive submodule](runtimeverification/smir_pretty#8) in the future) * adds a `make` target for a simple integration test: convert each `run-rs` program to Stable-MIR and parse the result. Remarks: * The tests are currently only proving that the parser succeeds. We can add better checks later when the format is stable enough to not cause noise in golden tests. * In order to run `smir_pretty`, information about the rust target architecture is needed. To circumvent this, the related script (within `smir_pretty` repo) is patched (but only the copy in the docker file system). This is a workaround and could be addressed properly by - crafting a github action to set up K and removing the dockerised K, - or preparing `smir_pretty` to run within `nix` and using a nix shell. - or (not recommended) placing the custom `rust` build and `smir_pretty` within the docker image or container. --------- Co-authored-by: devops <devops@runtimeverification.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
and others
The logic to check out
https://github.com/rust-lang/rustand the branch to refer to is currently managed by theMakefileonly.deps/rustinto a git submodule to track the dependency more prominentlygit submodule update --single-branchto avoid checking out too much history, provide a suitable command short-hand for this in the Makefile for convenience.Makefile) if necessary.The text was updated successfully, but these errors were encountered: