From 87d5a08f44b46657026a99c154bcec4a733f221d Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 29 May 2024 10:37:17 +0200
Subject: Improve the tests README

---
 tests/Makefile  |  6 +++---
 tests/README.md | 30 +++++++++++++++++++-----------
 2 files changed, 22 insertions(+), 14 deletions(-)

diff --git a/tests/Makefile b/tests/Makefile
index ff4baaba..a911e037 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -1,6 +1,6 @@
 .PHONY: all
-all: test-fstar test-coq test-lean test-hol4
+all: verify-fstar verify-coq verify-lean verify-hol4
 
-.PHONY: test-%
-test-%:
+.PHONY: verify-%
+verify-%:
 	cd $* && $(MAKE) all
diff --git a/tests/README.md b/tests/README.md
index f68b509f..c9ca0047 100644
--- a/tests/README.md
+++ b/tests/README.md
@@ -8,23 +8,26 @@ This folder contains the test suite for Aeneas. It is organized as follows:
    - Files generated by Aeneas from our test inputs;
    - Handwritten proof files.
 
-# Running the test suite
+## Running the test suite
 
 Running the test suite has two parts:
-- The generation of files from rust to each backend. This is done by running `make test` in the
+- We generate files from rust to each backend. This is done by running `make test` in the
   project root. This will call the test runner on each file or crate in `tests/src`, which will call
   `charon` and `aeneas` to generate the backend-specific outputs.
-- The verification of proofs for each backend. This is done by running `make verify` in the project
-  root. It will run each verifier (`fstar`, `lean` etc) on the files in the corresponding folder to
-  verify the correctness of proofs.
+- We check that the generated output is valid code by parsing it and type-checking it with the
+  relevant verifier (Lean, Coq, F*, etc.), and replay the hand-written proofs which use it as
+  a dependency. This is done by running `make verify` in the project root. 
 
-CI does both of these things; in particular it checks that we correctly committed the generated
-files.
+To generate the output of a single test, run `make test-<file_name>`, e.g. `make test-loops.rs` or
+`make test-betree`. To verify the output for a single backend, run `make verify-<backend>` inside the
+`tests/` folder, e.g. `make verify-coq`.
 
-Important note: at the moment we don't regenerate the `hol4` outputs. We do still check them with
+CI does both of these things; it also checks that we committed all the generated files.
+
+Important note: at the moment we don't regenerate the HOL4 outputs. We do still check them with
 hol4. This is tracked in https://github.com/AeneasVerif/aeneas/issues/62.
 
-# Adding a new test
+## Adding a new test
 
 Adding a new test is easy: just add a `foo.rs` file or a `foo_crate` folder in `tests/src`. `make
 test` will find the new file and call the test runner on it.
@@ -35,7 +38,7 @@ Ideally, any non-trivial change to Aeneas should have an accompanying test that
 code. The goal of this test suite is to cover a large portion of what Aeneas can do, so we can work
 on it confidently.
 
-# Passing options to `Aeneas` and `Charon`
+## Passing options to `Aeneas` and `Charon`
 
 The test runner supports setting several options for each test.
 - For single files, it will read comments at the top of the file that start with `//@`;
@@ -52,13 +55,18 @@ In both cases it supports the same options. Typical options are:
 
 For an up-to-date list of options, see comments in `tests/test_runner/Input.ml`.
 
-# `known-failure` tests
+## `known-failure` tests
 
 There's a special kind of test that doesn't generate backend code: `//@ known-failure` tests. These
 are meant to record:
 - Cases that produce an error so we don't forget and can fix them later;
 - Cases that _should_ error, to ensure we correctly raise an error and that the error output is nice.
 
+We record the output of the `aeneas` call in `test-file.out` alongside the original `test-file.rs`.
+This file must be committed like the rest of the test outputs. (Note: sometimes the output will be
+different between your local machine and CI, e.g. because release build changed a stacktrace. In
+that case we don't record the output, which is done with `//@ no-check-output`).
+
 It is useful to add tests there whenever you find an interesting failure case.
 
 Note however that this is for failures of Aeneas. Tests that cause Charon errors should be submitted
-- 
cgit v1.2.3