Use relative paths in demo/example Cargo.toml files

[gww-parity]

Example :

diff --git a/compatibility-test/Cargo.toml b/compatibility-test/Cargo.toml
index 7a18f73..2b31ff5 100644
--- a/compatibility-test/Cargo.toml
+++ b/compatibility-test/Cargo.toml
@@ -11,7 +11,7 @@ description = "Tests for both the propverify and the proptest crates - to check
 [dependencies]
 
 [target.'cfg(verify)'.dependencies]
-propverify = { path="/home/rust-verification-tools/propverify" }
+propverify = { path="../propverify" }
 
 [target.'cfg(not(verify))'.dependencies]
 proptest = { version = "*" }
diff --git a/demos/simple/klee/Cargo.toml b/demos/simple/klee/Cargo.toml
index 11fe766..fa1e6f4 100644
--- a/demos/simple/klee/Cargo.toml
+++ b/demos/simple/klee/Cargo.toml
@@ -5,7 +5,8 @@ authors = [""]
 edition = "2018"
 
 [dependencies]
-verification-annotations = { path="/home/rust-verification-tools/verification-annotations" }
+#verification-annotations = { path="/home/rust-verification-tools/verification-annotations" }
+verification-annotations = { path="../../../verification-annotations" }
 

btw. also maybe consider +nightly in scripts as it seems that some nightly features are required, example:

 cargo clean
-cargo build --features=verifier-klee
+cargo  +nightly build --features=verifier-klee

[alastairreid]

Your comment crossed paths with a PR that just landed that improves the docker/build system.
In particular, we now use +nightly in the docker/init script that rebuilds all the tools.
(The docker build process is also much faster than before: 15-20 minutes instead of 3 hours)

We deliberately do not use +nightly in the verify.sh scripts, the cargo-verify script or the Cargo.toml files in regression tests (demos///Cargo.toml, compatibility-test/Cargo.toml) because those need to be built with an LLVM-10 compatible version of Rust. (Our docker build uses the last LLVM-10 version of rustc (nightly-2020-08-03) and makes that the default Rust compiler. Support for LLVM11-based rustc is partially done - but many of our regression tests break.)

[alastairreid]

wrt this change

[target.'cfg(verify)'.dependencies]
-propverify = { path="/home/rust-verification-tools/propverify" }
+propverify = { path="../propverify" }

What we really want to do here is to use path="$RVT_DIR/propverify" but, unfortunately, Cargo does not support environment variables in toml files.

We chose to use an absolute path because then it is easy to use the same dependency information in any toml file, examples, etc. But this only works if you are using docker (where we mount $RVT_DIR) as /home/rust-verification-tools.

Until now, we have been assuming that building directly (not using docker) was too painful for people to do - so this seemed like a good choice. But

1. It sounds as if you are not using docker
2. The PR that I just merged dramatically simplified the build process (you no longer have to build a custom version of rustc/libstd/libcore) and we are wondering whether we could further simplify our use of docker.

I need to think about this a bit more...

[gww-parity]

or maybe just make package propverify and put it on crates.io ?

[alastairreid]

We have held off on doing that because the code is still all experimental, changes in a tool often needs matching changes in a crate (and vice versa) so building them all within docker with a single compiler, from a single source tree avoids problems. (Of course, long-term, they should be on crates.io - but we don't feel ready for that yet.) But I am puzzled about why you were seeing any problems here. If you build a docker image and you only verify within that image (and you use 'cargo clean' or 'cargo verify --clean ...' to remove code compiled with other rustc versions), then it should all be consistent. If you are building as I described in #138 and seeing problems (except for the need for sudo), can you give us some details so that we can reproduce and fix.

…

On Fri, May 21, 2021 at 1:17 PM Grzegorz Wierzowiecki (parity) < ***@***.***> wrote: or maybe just make package propverify and put it on crates.io ? — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#137 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACXRJSKTEQBN72MI36P6RYTTOZFPNANCNFSM45HARZ2Q> .