From d303833ddaa3b046cfc506be8c843ec950f26000 Mon Sep 17 00:00:00 2001 From: loganrjmurphy Date: Tue, 28 May 2024 12:00:25 -0400 Subject: [PATCH] minor edits to readmes --- AutoFormalization/README.md | 2 ++ E3/README.md | 2 +- README.md | 2 +- 3 files changed, 4 insertions(+), 2 deletions(-) diff --git a/AutoFormalization/README.md b/AutoFormalization/README.md index f4936d8..e21fbf4 100644 --- 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 index fff3a54..8bf2d91 100644 --- 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 index 365d629..f3b67ea 100644 --- 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`