Skip to content

Commit

Permalink
chore: add note about lean4lean
Browse files Browse the repository at this point in the history
  • Loading branch information
digama0 committed Nov 4, 2024
1 parent 7bc0a77 commit c7ac956
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,9 @@ This can only be used on a single file.
This is not an external verifier, simply a tool to detect "environment hacking".
-/
unsafe def main (args : List String) : IO UInt32 := do
-- Contributor's note: lean4lean is intended to have a CLI interface matching lean4checker,
-- so if you want to make a change here please either make a sibling PR to
-- https://github.com/digama0/lean4lean or ping @digama0 (Mario Carneiro) to go fix it.
initSearchPath (← findSysroot)
let (flags, args) := args.partition fun s => s.startsWith "-"
let verbose := "-v" ∈ flags || "--verbose" ∈ flags
Expand Down

0 comments on commit c7ac956

Please sign in to comment.