minor edits to readmes

loganrjmurphy · May 28, 2024 · d303833 · d303833
1 parent 51a7efd
commit d303833
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 2 deletions.
diff --git a/AutoFormalization/README.md b/AutoFormalization/README.md
@@ -32,6 +32,8 @@ The results can be found from the root directory under `results`, under the subd
 
 ### Evaluating Autoformalized Theorem Statements 
 
+Before you run any evaluation scripts for theorem statements, make sure you run `lake build E3` to build the equivalence checker.
+
 #### Standard Equivalence Checking
 Once you've formalized a set of theoerem statements, you can use our equivalence checker `E3` to logically evaluate them in batch against the ground truth theorems in LeanEuclid. 
 

diff --git a/E3/README.md b/E3/README.md
@@ -6,7 +6,7 @@ While `E3` can be used in an *ad hoc* manner, we also provide a Python wrapper f
 
 ### Setup
 
-From the root directory of LeanEuclid, run `lake build E3`
+From the root directory of LeanEuclid, run `lake build E3`.
 
 ### Overview 
 

diff --git a/README.md b/README.md
@@ -64,7 +64,7 @@ Take the following steps to build the Lean project:
 
 Optionally, you can:
 
-1. Run `lake build Book` to build all proofs in the first book of Euclid's *Elements* (takes a few minutes)
+// 1. Run `lake build Book` to build all proofs in the first book of Euclid's *Elements* (takes a few minutes)
 1. Run `lake -R -Kenv=dev build SystemE:docs` to build the documentation
 1. View the auto-generated documentation locally at ./lake/build/doc, e.g., using `python -mhttp.server`