Skip to content

Commit

Permalink
update README
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Nov 6, 2023
1 parent b0d67ea commit 13087b3
Showing 1 changed file with 1 addition and 7 deletions.
8 changes: 1 addition & 7 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ file on the search path (note that this include Lean 4 and all dependencies of y

You can also use `lake exe lean4checker --fresh Mathlib.Data.Nat.Basic` to replay all the constants
(both imported and defined in that file) into a fresh environment.
This is single threaded, and may be much slower.

This is not an external verifier, as it uses the Lean kernel itself.
However it is useful as a tool to detect "environment hacking",
Expand All @@ -33,10 +34,3 @@ Despite `.olean` files being "fairly cross-platform",
`lean4checker` will reject `.olean`s that were compiled on a system
that does not use the same bignum library as your system,
so it advisable to not rely on cached `.olean`s.

## Variants

It would be easy to adapt this code to replay the entire environment up to some set of declarations,
starting from an empty environment
(rather than the current implementation, which starts from the environment provided by the imports).
If this would be useful to you, please ask.

0 comments on commit 13087b3

Please sign in to comment.