From 8f29824d1313e50734e732a84d668aef169c116f Mon Sep 17 00:00:00 2001 From: Vitor Enes Date: Thu, 28 Jan 2021 15:31:05 +0000 Subject: [PATCH] Improve light-client README (#790) The light client README files improved wrt. the testing instructions --- light-client/README.md | 16 ++++------------ light-client/tests/model_based.rs | 6 +++++- light-client/tests/support/model_based/README.md | 8 +++++++- 3 files changed, 16 insertions(+), 14 deletions(-) diff --git a/light-client/README.md b/light-client/README.md index ce552ca73..d3d92264b 100644 --- a/light-client/README.md +++ b/light-client/README.md @@ -66,22 +66,14 @@ The Tendermint Light Client is primarily tested through unit tests. ### Core Verification The logic for the core verification of light blocks is entirely self-contained in -the [`predicates`](./src/predicates.rs) module. This code is exercised in a family -of tests called `single_step` via a set of [JSON fixtures](./tests/support/single_step) -which encode an initial trusted state, a target block to verify, and the -expected result of the core verification algorithm. - -These tests come in two flavours: - -- `skipping` tests, where there is a gap between the initial trusted state and the target block. -- `sequential` tests, where there the initial trusted state and the target block are adjacent. +the [`predicates`](./src/predicates.rs) module. +This code is exercised through unit tests which test each predicate in isolation +by giving it a set of data along with the expected outcome of each check. The following command can be used to run only these tests: -TODO: the following runs 0 tests - ```bash -$ cargo test -p tendermint-light-client --test light_client single_step +cargo test -p tendermint-light-client predicates ``` #### Model-based tests diff --git a/light-client/tests/model_based.rs b/light-client/tests/model_based.rs index 5f3e3cf29..16e125ea3 100644 --- a/light-client/tests/model_based.rs +++ b/light-client/tests/model_based.rs @@ -662,7 +662,11 @@ fn model_based_test( } true }; - if !check_program("apalache-mc") || !check_program("jsonatr") || !check_program("timeout") { + if !check_program("tendermint-testgen") + || !check_program("apalache-mc") + || !check_program("jsonatr") + || !check_program("timeout") + { output_env.logln(" failed to find necessary programs; consider adding them to your PATH. skipping the test"); return; } diff --git a/light-client/tests/support/model_based/README.md b/light-client/tests/support/model_based/README.md index 8ed4a24e0..5f1cf73d5 100644 --- a/light-client/tests/support/model_based/README.md +++ b/light-client/tests/support/model_based/README.md @@ -23,7 +23,7 @@ When you run `cargo test` some machinery will run under the hood, namely: takes care of translating abstract values from the model into the concrete implementation values. * `timeout` command is used to limit the test execution time. -So, for the model-based test to run, the programs `apalache-mc`, `jsonatr`, +So, for the model-based test to run, the programs `apalache-mc`, `jsonatr`, `tendermint-testgen` and `timeout` should be present in your `PATH`. If any of the programs is not found, execution of a model-based test will be skipped. @@ -48,6 +48,12 @@ $ cd jsonatr/ $ cargo install --path . ``` +#### Installing `tendermint-testgen` + +```bash +$ cargo install tendermint-testgen +``` + #### Installing `timeout` `timeout` should be present by default on all Linux distributions, but may be absent on Macs. In that case it can be installed using `brew install coreutils`.