diff --git a/rocq-tools/README.md b/rocq-tools/README.md index 9d445d0f..71e11415 100644 --- a/rocq-tools/README.md +++ b/rocq-tools/README.md @@ -6,7 +6,7 @@ and performance data while compiling Coq projects efficiently with dune. As it is not currently possible to teach `dune` about custom data files (or any form of additional file generated by compilation), we embed the generated data into `.glob` files. With this approach, we both get: -1. fast CI using the dune cache to only recompiling files that need to be, +1. fast CI using the dune cache to only recompile files that need to be, 2. additional data for all files, including those that hit the cache. Data Gathering @@ -48,7 +48,7 @@ several pieces of data, which are all embedded into `.glob` files: the performance numbers for the whole file is also included. - A JSON log produced by our custom logger library if it was used (either from a plugin, or from our corresponding Ltac2 library). If the logger library is - not in use, no lot is included. + not in use, no log is included. - A copy of what the wrapped invocation of `coqc` printed on its `stderr`, and (separately) on its `stdout`. This is useful for, e.g., listing the warnings produced by the compilation of a given file, in case the cache hits.