| /- | |
| Copyright (c) 2025 Lean FRO, LLC. All rights reserved. | |
| Released under Apache 2.0 license as described in the file LICENSE. | |
| Authors: Henrik Böving | |
| -/ | |
| import LeanExport.Basic | |
| import LeanExport.Parse | |
| open Lean LeanExport | |
| def main (args : List String) : IO Unit := do | |
| initSearchPath (← findSysroot) | |
| let (opts, args) := args.partition (fun s => s.startsWith "--" && s.length ≥ 3) | |
| let (imports, constants) := args.span (· != "--") | |
| let imports := imports.toArray.map fun mod => { module := Syntax.decodeNameLit ("`" ++ mod) |>.get! } | |
| let env ← importModules imports {} | |
| let constants? := constants.tail?.map fun cs => | |
| cs.map fun c => Syntax.decodeNameLit ("`" ++ c) |>.get! | |
| dumpEnv env constants? opts |