refactor: port shell option processing to Lean (v2) (#11434)
This PR moves the processing of options passed to the CLI from `shell.cpp` to `Shell.lean`. As with previous ports, this attempts to mirror as much of the original behavior as possible, Benefits to be gained from the ported code can come in later PRs. There should be no significant behavioral changes from this port. Nonetheless, error reporting has changed some, hopefully for the better. For instance, errors for improper argument configurations has been made more consistent (e.g., Lean will now error if numeric arguments fall outside the expected range for an option). (Redo of #11345 to fix Windows issue.)
This commit is contained in:
Mac Malone
GitHub
parent
edf804c70f
commit
79838834c1
9 changed files with 442 additions and 387 deletions
|
|
@ -300,6 +300,28 @@ structure SetupImportsResult where
|
|||
/-- Lean plugins to load as part of the environment setup. -/
|
||||
plugins : Array System.FilePath := #[]
|
||||
|
||||
/--
|
||||
Parses an option value from a string and inserts it into `opts`.
|
||||
The type of the option is determined from `decl`.
|
||||
-/
|
||||
def setOption (opts : Options) (decl : OptionDecl) (name : Name) (val : String) : IO Options := do
|
||||
match decl.defValue with
|
||||
| .ofBool _ =>
|
||||
match val with
|
||||
| "true" => return opts.insert name true
|
||||
| "false" => return opts.insert name false
|
||||
| _ =>
|
||||
throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
|
||||
it must be true/false"
|
||||
| .ofNat _ =>
|
||||
let some val := val.toNat?
|
||||
| throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
|
||||
it must be a natural number"
|
||||
return opts.insert name val
|
||||
| .ofString _ => return opts.insert name val
|
||||
| _ => throw <| .userError s!"invalid -D parameter, configuration option '{name}' \
|
||||
cannot be set in the command line, use set_option command"
|
||||
|
||||
/--
|
||||
Parses values of options registered during import and left by the C++ frontend as strings.
|
||||
Removes `weak` prefixes from both parsed and unparsed options and fails if any option names remain
|
||||
|
|
@ -322,22 +344,7 @@ If the option is defined in a library, use '-D{`weak ++ name}' to set it conditi
|
|||
let .ofString val := val
|
||||
| opts' := opts'.insert name val -- Already parsed
|
||||
|
||||
match decl.defValue with
|
||||
| .ofBool _ =>
|
||||
match val with
|
||||
| "true" => opts' := opts'.insert name true
|
||||
| "false" => opts' := opts'.insert name false
|
||||
| _ =>
|
||||
throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
|
||||
it must be true/false"
|
||||
| .ofNat _ =>
|
||||
let some val := val.toNat?
|
||||
| throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
|
||||
it must be a natural number"
|
||||
opts' := opts'.insert name val
|
||||
| .ofString _ => opts' := opts'.insert name val
|
||||
| _ => throw <| .userError s!"invalid -D parameter, configuration option '{name}' \
|
||||
cannot be set in the command line, use set_option command"
|
||||
opts' ← setOption opts' decl name val
|
||||
|
||||
return opts'
|
||||
|
||||
|
|
|
|||
|
|
@ -55,15 +55,15 @@ opaque displayCumulativeProfilingTimes : BaseIO Unit
|
|||
@[extern "lean_internal_has_address_sanitizer"]
|
||||
opaque Internal.hasAddressSanitizer (_ : Unit) : Bool
|
||||
|
||||
/-- Whether Lean was built with multithread support. -/
|
||||
/-- Whether Lean was built with multithread support (i.e., `LEAN_MULTI_THREAD`). -/
|
||||
@[extern "lean_internal_is_multi_thread"]
|
||||
opaque Internal.isMultiThread (_ : Unit) : Bool
|
||||
|
||||
/-- Whether Lean was built in debug mode. -/
|
||||
/-- Whether Lean was built in debug mode (i.e., `LEAN_DEBUG`). -/
|
||||
@[extern "lean_internal_is_debug"]
|
||||
opaque Internal.isDebug (_ : Unit) : Bool
|
||||
|
||||
/-- Returns the mode Lean was built in. -/
|
||||
/-- Returns the mode Lean was built in (i.e., `LEAN_BUILD_TYPE`). -/
|
||||
@[extern "lean_internal_get_build_type"]
|
||||
opaque Internal.getBuildType (_ : Unit) : String
|
||||
|
||||
|
|
@ -89,7 +89,27 @@ opaque Internal.getDefaultMaxHeartbeat (_ : Unit) : Nat
|
|||
@[extern "lean_internal_set_max_heartbeat"]
|
||||
opaque Internal.setMaxHeartbeat (max : USize) : BaseIO Unit
|
||||
|
||||
/-- Lean equivalent of `LEAN_VERSION_STRING` / `g_short_version_string` -/
|
||||
/-- Returns whether Lean was built as verbose by default (i.e., `LEAN_DEFAULT_VERBOSE`). -/
|
||||
@[extern "lean_internal_get_default_verbose"]
|
||||
opaque Internal.getDefaultVerbose (_ : Unit) : Bool
|
||||
|
||||
/-- Sets whether Lean aborts when a panic occurs. -/
|
||||
@[extern "lean_internal_set_exit_on_panic"]
|
||||
opaque Internal.setExitOnPanic (exit : Bool) : BaseIO Unit
|
||||
|
||||
/-- Sets the stack size (in bytes) of a Lean thread. -/
|
||||
@[extern "lean_internal_set_thread_stack_size"]
|
||||
opaque Internal.setThreadStackSize (sz : USize) : BaseIO Unit
|
||||
|
||||
/-- Enables debug assertions with the given tag. -/
|
||||
@[extern "lean_internal_enable_debug"]
|
||||
opaque Internal.enableDebug (tag : @& String) : BaseIO Unit
|
||||
|
||||
/--
|
||||
Lean's short version string (i.e., what is printed by `lean --short-version`).
|
||||
|
||||
This is the Lean equivalent of of the C++ `LEAN_VERSION_STRING` / `g_short_version_string`.
|
||||
-/
|
||||
def shortVersionString : String :=
|
||||
if version.specialDesc ≠ "" then
|
||||
s!"{versionStringCore}-{version.specialDesc}"
|
||||
|
|
@ -107,13 +127,17 @@ def versionHeader : String := Id.run do
|
|||
ver := s!"{ver}, commit {githash}"
|
||||
s!"Lean (version {ver}, {Internal.getBuildType ()})"
|
||||
|
||||
/-- Print the Lean version header. -/
|
||||
@[export lean_display_header]
|
||||
def displayHeader : IO Unit := do
|
||||
IO.println versionHeader
|
||||
/--
|
||||
A string containing the list of additional features Lean was built with.
|
||||
|
||||
This is printed by `lean --features`.
|
||||
-/
|
||||
def featuresString :=
|
||||
if Internal.hasLLVMBackend () then
|
||||
"[LLVM]"
|
||||
else "[]"
|
||||
|
||||
/-- Print the Lean CLI help message. -/
|
||||
@[export lean_display_help]
|
||||
def displayHelp (useStderr : Bool) : IO Unit := do
|
||||
let out ← if useStderr then IO.getStderr else IO.getStdout
|
||||
out.putStrLn versionHeader
|
||||
|
|
@ -129,7 +153,7 @@ def displayHelp (useStderr : Bool) : IO Unit := do
|
|||
out.putStrLn " -c, --c=fname name of the C output file"
|
||||
out.putStrLn " -b, --bc=fname name of the LLVM bitcode file"
|
||||
out.putStrLn " --stdin take input from stdin"
|
||||
out.putStrLn " --root=dir set package root directory from which the module name\n"
|
||||
out.putStrLn " -R, --root=dir set package root directory from which the module name\n"
|
||||
out.putStrLn " of the input file is calculated\n"
|
||||
out.putStrLn " (default: current working directory)\n";
|
||||
out.putStrLn " -t, --trust=num trust level (default: max) 0 means do not trust any macro,\n"
|
||||
|
|
@ -148,7 +172,7 @@ def displayHelp (useStderr : Bool) : IO Unit := do
|
|||
out.putStrLn " --load-dynlib=file load shared library to make its symbols available to the interpreter"
|
||||
out.putStrLn " --setup=file JSON file with module setup data (supersedes the file's header)"
|
||||
out.putStrLn " --json report Lean output (e.g., messages) as JSON (one per line)"
|
||||
out.putStrLn " -E --error=kind report Lean messages of kind as errors"
|
||||
out.putStrLn " -E, --error=kind report Lean messages of kind as errors"
|
||||
out.putStrLn " --deps just print dependencies of a Lean input"
|
||||
out.putStrLn " --src-deps just print dependency sources of a Lean input"
|
||||
out.putStrLn " --print-prefix print the installation prefix for Lean and exit"
|
||||
|
|
@ -170,52 +194,285 @@ private builtin_initialize maxMemory : Lean.Option Nat ←
|
|||
private builtin_initialize timeout : Lean.Option Nat ←
|
||||
Lean.Option.register `timeout {defValue := Internal.getDefaultMaxHeartbeat ()}
|
||||
|
||||
private builtin_initialize verbose : Lean.Option Bool ←
|
||||
Lean.Option.register `verbose {defValue := Internal.getDefaultVerbose ()}
|
||||
|
||||
/--
|
||||
Returns the default options Lean was built with
|
||||
(i.e., those set in `stdlib_flags.h`).
|
||||
-/
|
||||
@[extern "lean_internal_get_default_options"]
|
||||
opaque Internal.getDefaultOptions (_ : Unit) : Options
|
||||
|
||||
/--
|
||||
Returns the believer trust level of the Lean environment (i.e., `LEAN_BELIEVER_TRUST_LEVEL`).
|
||||
|
||||
If an environment is created with a trust level greater than this, then we can add declarations
|
||||
to it without type checking them.
|
||||
-/
|
||||
@[extern "lean_internal_get_believer_trust_level"]
|
||||
opaque Internal.getBelieverTrustLevel (_ : Unit) : UInt32
|
||||
|
||||
/-- Returns the shell's default trust level. -/
|
||||
def defaultTrustLevel : UInt32 :=
|
||||
Internal.getBelieverTrustLevel () + 1
|
||||
|
||||
/-- Returns the platform's native concurrency limit. -/
|
||||
@[extern "lean_internal_get_hardware_concurrency"]
|
||||
opaque Internal.getHardwareCurrency (_ : Unit) : UInt32
|
||||
|
||||
/-- Returns the default number of threads for the shell's task manager. -/
|
||||
def defaultNumThreads : UInt32 :=
|
||||
if Internal.isMultiThread () then
|
||||
Internal.getHardwareCurrency ()
|
||||
else 0
|
||||
|
||||
structure ShellOptions where
|
||||
leanOpts : Options := Internal.getDefaultOptions ()
|
||||
forwardedArgs : Array String := #[]
|
||||
component : ShellComponent := .frontend
|
||||
printPrefix : Bool := false
|
||||
printLibDir : Bool := false
|
||||
useStdin : Bool := false
|
||||
onlyDeps : Bool := false
|
||||
onlySrcDeps : Bool := false
|
||||
depsJson : Bool := false
|
||||
opts : Options := {}
|
||||
trustLevel : UInt32 := defaultTrustLevel
|
||||
numThreads : UInt32 := defaultNumThreads
|
||||
rootDir? : Option System.FilePath := none
|
||||
setupFileName? : Option System.FilePath := none
|
||||
oleanFileName? : Option System.FilePath := none
|
||||
ileanFileName? : Option System.FilePath := none
|
||||
cFileName? : Option System.FilePath := none
|
||||
bcFileName? : Option System.FilePath := none
|
||||
jsonOutput : Bool := false
|
||||
errorOnKinds : Array Name := #[]
|
||||
printStats : Bool := false
|
||||
run : Bool := false
|
||||
|
||||
@[export lean_shell_options_mk]
|
||||
def mkShellOptions (_ : Unit) : ShellOptions := {}
|
||||
|
||||
@[export lean_shell_options_get_run]
|
||||
def ShellOptions.getRun (opts : ShellOptions) : Bool :=
|
||||
opts.run
|
||||
|
||||
@[export lean_shell_options_get_profiler]
|
||||
def ShellOptions.getProfiler (opts : ShellOptions) : Bool :=
|
||||
profiler.get opts.leanOpts
|
||||
|
||||
@[export lean_shell_options_get_num_threads]
|
||||
def ShellOptions.getNumThreads (opts : ShellOptions) : UInt32 :=
|
||||
opts.numThreads
|
||||
|
||||
def checkOptArg (optName : String) (optArg? : Option String) : IO String := do
|
||||
if let some arg := optArg? then
|
||||
return arg
|
||||
else
|
||||
throw <| .userError s!"argument missing for option '-{optName}'"
|
||||
|
||||
def setConfigOption (opts : Options) (arg : String) : IO Options := do
|
||||
let pos := arg.find '='
|
||||
if h : pos.IsAtEnd then
|
||||
throw <| .userError "invalid -D parameter, argument must contain '='"
|
||||
else
|
||||
let name := arg.sliceTo pos |>.toName
|
||||
let val := arg.sliceFrom (pos.next h) |>.copy
|
||||
if let some decl := (← getOptionDecls).find? name then
|
||||
Language.Lean.setOption opts decl name val
|
||||
else
|
||||
-- More options may be registered by imports, so we leave validating them to the elaborator.
|
||||
-- This (minor) duplication may be resolved later.
|
||||
return opts.insert name val
|
||||
|
||||
/--
|
||||
Process a command-line option parsed by the C++ shell.
|
||||
|
||||
Runs under `IO.initializing` and without a task manager.
|
||||
-/
|
||||
@[export lean_shell_options_process]
|
||||
def ShellOptions.process (opts : ShellOptions)
|
||||
(opt : Char) (optArg? : Option String) : EIO UInt32 ShellOptions := do
|
||||
have : MonadLift IO (EIO UInt32) := ⟨liftIO⟩
|
||||
match opt with
|
||||
| 'e' => -- undocumented
|
||||
Internal.setExitOnPanic true
|
||||
return opts
|
||||
| 'j' => -- `-j, --threads=num`
|
||||
let arg ← checkOptArg "j" optArg?
|
||||
let some numThreads := arg.toNat?
|
||||
| throwExpectedNumeric "j"
|
||||
if h : numThreads < UInt32.size then
|
||||
let numThreads := UInt32.ofNatLT numThreads h
|
||||
let forwardedArgs := opts.forwardedArgs.push s!"-j{arg}";
|
||||
return {opts with forwardedArgs, numThreads}
|
||||
else
|
||||
throwTooLarge "j"
|
||||
| 'v' => --- `-v, --version`
|
||||
IO.println Lean.versionHeader
|
||||
throw 0
|
||||
| 'V' => --- `-V, --short-version`
|
||||
IO.println Lean.shortVersionString
|
||||
throw 0
|
||||
| 'g' => -- `-g, --githash`
|
||||
IO.println Lean.githash
|
||||
throw 0
|
||||
| 'h' => -- `-h, --help`
|
||||
displayHelp (useStderr := false)
|
||||
throw 0
|
||||
| 'f' => -- `--features`
|
||||
IO.println Lean.featuresString
|
||||
throw 0
|
||||
| 'c' => -- `-c, --c=fname`
|
||||
return {opts with cFileName? := ← checkOptArg "c" optArg?}
|
||||
| 'b' => -- `-b, --bc=fname`
|
||||
return {opts with bcFileName? := ← checkOptArg "b" optArg?}
|
||||
| 's' => -- `-s, --tstack=num`
|
||||
let arg ← checkOptArg "s" optArg?
|
||||
let some stackSize := arg.toNat?
|
||||
| throwExpectedNumeric "s"
|
||||
let stackSize := stackSize / 4 * 4 * 1024
|
||||
if h : stackSize < USize.size then
|
||||
let stackSize := USize.ofNatLT stackSize h
|
||||
Internal.setThreadStackSize stackSize
|
||||
let forwardedArgs := opts.forwardedArgs.push s!"-s{arg}"
|
||||
return {opts with forwardedArgs}
|
||||
else
|
||||
throwTooLarge "s"
|
||||
| 'I' => -- `-I, --stdin`
|
||||
return {opts with useStdin := true}
|
||||
| 'r' => -- `--run`
|
||||
return {opts with run := true}
|
||||
| 'o' => -- `--o, olean=fname`
|
||||
return {opts with oleanFileName? := ← checkOptArg "o" optArg?}
|
||||
| 'i' => -- `--i, ilean=fname`
|
||||
return {opts with ileanFileName? := ← checkOptArg "i" optArg?}
|
||||
| 'R' => -- `-R, --root=dir`
|
||||
let arg ← checkOptArg "R" optArg?
|
||||
let forwardedArgs := opts.forwardedArgs.push s!"-R{arg}"
|
||||
return {opts with forwardedArgs, rootDir? := arg}
|
||||
| 'M' => -- `-M, --memory=num`
|
||||
let arg ← checkOptArg "M" optArg?
|
||||
let some val := arg.toNat?
|
||||
| throwExpectedNumeric "M"
|
||||
let leanOpts := maxMemory.set opts.leanOpts val
|
||||
let forwardedArgs := opts.forwardedArgs.push s!"-M{arg}"
|
||||
return {opts with forwardedArgs, leanOpts}
|
||||
| 'T' => -- `-T, --timeout=num`
|
||||
let arg ← checkOptArg "T" optArg?
|
||||
let some val := arg.toNat?
|
||||
| throwExpectedNumeric "T"
|
||||
let leanOpts := timeout.set opts.leanOpts val
|
||||
let forwardedArgs := opts.forwardedArgs.push s!"-T{arg}"
|
||||
return {opts with forwardedArgs, leanOpts}
|
||||
| 't' => -- `--trust=num`
|
||||
let arg ← checkOptArg "t" optArg?
|
||||
let some trustLevel := arg.toNat?
|
||||
| throwExpectedNumeric "t"
|
||||
if h : trustLevel < UInt32.size then
|
||||
let trustLevel := UInt32.ofNatLT trustLevel h
|
||||
let forwardedArgs := opts.forwardedArgs.push s!"-t{arg}";
|
||||
return {opts with forwardedArgs, trustLevel}
|
||||
else
|
||||
throwTooLarge "t"
|
||||
| 'q' =>
|
||||
return {opts with leanOpts := verbose.set opts.leanOpts false}
|
||||
| 'd' => -- `--deps`
|
||||
return {opts with onlyDeps := true}
|
||||
| 'O' => -- `--src-deps`
|
||||
return {opts with onlySrcDeps := true}
|
||||
| 'N' => -- `--deps-json`
|
||||
return {opts with onlyDeps := true, depsJson := true}
|
||||
| 'J' => -- `--json`
|
||||
return {opts with jsonOutput := true}
|
||||
| 'a' => -- `--stats`
|
||||
return {opts with printStats := true}
|
||||
| 'x' => -- `--print-prefix`
|
||||
return {opts with printPrefix := true}
|
||||
| 'L' => -- `--print-libdir`
|
||||
return {opts with printLibDir := true}
|
||||
| 'D' => -- `-D name=value`
|
||||
let arg ← checkOptArg "D" optArg?
|
||||
let leanOpts ← setConfigOption opts.leanOpts arg
|
||||
let forwardedArgs := opts.forwardedArgs.push s!"-D{arg}"
|
||||
return {opts with forwardedArgs, leanOpts}
|
||||
| 'S' => -- `--server`
|
||||
return {opts with component := .watchdog}
|
||||
| 'W' => -- `--worker`
|
||||
return {opts with component := .worker}
|
||||
| 'P' => -- `--profile`
|
||||
return {opts with leanOpts := profiler.set opts.leanOpts true}
|
||||
| 'B' => -- `--debug=tag`
|
||||
if Internal.isDebug () then
|
||||
let arg ← checkOptArg "B" optArg?
|
||||
Internal.enableDebug arg
|
||||
return opts
|
||||
-- if not `LEAN_DEBUG`, fall through to unknown option
|
||||
| 'p' => -- `--plugin=file`
|
||||
let arg ← checkOptArg "p" optArg?
|
||||
Lean.loadPlugin arg
|
||||
let forwardedArgs := opts.forwardedArgs.push s!"-p{arg}"
|
||||
return {opts with forwardedArgs}
|
||||
| 'l' => -- `--load-dynlib=file`
|
||||
let arg ← checkOptArg "l" optArg?
|
||||
Lean.loadDynlib arg
|
||||
let forwardedArgs := opts.forwardedArgs.push s!"-l{arg}"
|
||||
return {opts with forwardedArgs}
|
||||
| 'u' => -- `--setup=file`
|
||||
return {opts with setupFileName? := ← checkOptArg "u" optArg?}
|
||||
| 'E' => -- `-E, --error=kind`
|
||||
let arg ← checkOptArg "E" optArg?
|
||||
let errorOnKinds := opts.errorOnKinds.push arg.toName
|
||||
return {opts with errorOnKinds}
|
||||
| _ =>
|
||||
pure ()
|
||||
eprint "Unknown command line option\n"
|
||||
displayHelp (useStderr := true)
|
||||
throw 1
|
||||
where
|
||||
@[inline] eprint msg := do
|
||||
IO.eprint msg |>.catchExceptions fun _ => pure ()
|
||||
@[inline] liftIO {α} (x : IO α) := do
|
||||
match (← x.toBaseIO) with
|
||||
| .ok a =>
|
||||
return a
|
||||
| .error e =>
|
||||
eprint s!"error: "
|
||||
eprint (toString e)
|
||||
eprint "\n"
|
||||
throw 1
|
||||
@[inline] throwExpectedNumeric opt := do
|
||||
eprint s!"error: expected numeric argument for option '-{opt}'\n"
|
||||
throw 1
|
||||
@[inline] throwTooLarge opt := do
|
||||
eprint s!"error: argument value for '-{opt}' is too large\n"
|
||||
throw 1
|
||||
|
||||
@[export lean_shell_main]
|
||||
def shellMain
|
||||
(args : List String)
|
||||
(forwardedArgs : List String)
|
||||
(component : ShellComponent := .frontend)
|
||||
(printPrefix : Bool := false)
|
||||
(printLibDir : Bool := false)
|
||||
(useStdin : Bool := false)
|
||||
(onlyDeps : Bool := false)
|
||||
(onlySrcDeps : Bool := false)
|
||||
(depsJson : Bool := false)
|
||||
(opts : Options := {})
|
||||
(trustLevel : UInt32 := 0)
|
||||
(rootDir? : Option System.FilePath := none)
|
||||
(setupFileName? : Option System.FilePath := none)
|
||||
(oleanFileName? : Option System.FilePath := none)
|
||||
(ileanFileName? : Option System.FilePath := none)
|
||||
(cFileName? : Option System.FilePath := none)
|
||||
(bcFileName? : Option System.FilePath := none)
|
||||
(jsonOutput : Bool := false)
|
||||
(errorOnKinds : Array Name := #[])
|
||||
(printStats : Bool := false)
|
||||
(run : Bool := false)
|
||||
: IO UInt32 := do
|
||||
if printPrefix then
|
||||
def shellMain (args : List String) (opts : ShellOptions) : IO UInt32 := do
|
||||
if opts.printPrefix then
|
||||
IO.println (← getBuildDir)
|
||||
return 0
|
||||
if printLibDir then
|
||||
if opts.printLibDir then
|
||||
IO.println (← getLibDir (← getBuildDir))
|
||||
return 0
|
||||
let maxMemory := maxMemory.get opts
|
||||
let maxMemory := maxMemory.get opts.leanOpts
|
||||
if maxMemory != 0 then
|
||||
Internal.setMaxMemory (maxMemory.toUSize * 1024 * 1024)
|
||||
let timeout := timeout.get opts
|
||||
let timeout := timeout.get opts.leanOpts
|
||||
if timeout != 0 then
|
||||
Internal.setMaxHeartbeat (timeout.toUSize * 1000)
|
||||
match component with
|
||||
match opts.component with
|
||||
| .frontend =>
|
||||
pure ()
|
||||
| .watchdog =>
|
||||
return ← Server.Watchdog.watchdogMain forwardedArgs
|
||||
return ← Server.Watchdog.watchdogMain opts.forwardedArgs.toList
|
||||
| .worker =>
|
||||
return ← Server.FileWorker.workerMain opts
|
||||
if onlyDeps && depsJson then
|
||||
return ← Server.FileWorker.workerMain opts.leanOpts
|
||||
if opts.onlyDeps && opts.depsJson then
|
||||
let fns ←
|
||||
if useStdin then
|
||||
if opts.useStdin then
|
||||
(← IO.getStdin).lines
|
||||
else
|
||||
pure args.toArray
|
||||
|
|
@ -225,72 +482,73 @@ def shellMain
|
|||
match args with
|
||||
| fileName :: args => (some fileName, args)
|
||||
| [] => (none, args)
|
||||
if !run && !args.isEmpty then
|
||||
if !opts.run && !args.isEmpty then
|
||||
IO.eprintln "Expected exactly one file name"
|
||||
displayHelp (useStderr := true)
|
||||
return 1
|
||||
let fileName ←
|
||||
if let some fileName := fileName? then
|
||||
pure fileName
|
||||
else if useStdin then
|
||||
else if opts.useStdin then
|
||||
pure "<stdin>"
|
||||
else
|
||||
IO.eprintln "Expected exactly one file name"
|
||||
displayHelp (useStderr := true)
|
||||
return 1
|
||||
let contents ← decodeLossyUTF8 <$> do
|
||||
if useStdin then
|
||||
if opts.useStdin then
|
||||
(← IO.getStdin).readBinToEnd
|
||||
else
|
||||
IO.FS.readBinFile fileName
|
||||
if onlyDeps then
|
||||
if opts.onlyDeps then
|
||||
Elab.printImports contents fileName
|
||||
return 0
|
||||
if onlySrcDeps then
|
||||
if opts.onlySrcDeps then
|
||||
Elab.printImportSrcs contents fileName
|
||||
return 0
|
||||
-- Quick and dirty `#lang` support
|
||||
---TODO: make it extensible, and add `lean4md`
|
||||
let contents ←
|
||||
if contents.startsWith "#lang" then
|
||||
if let some contents := contents.dropPrefix? "#lang" then
|
||||
let endLinePos := contents.find '\n'
|
||||
let langId := String.Pos.Raw.extract contents ⟨6⟩ endLinePos.offset |>.trimAscii
|
||||
let langId := contents.sliceTo endLinePos |>.trimAscii
|
||||
if langId == "lean4" then
|
||||
pure () -- do nothing for now
|
||||
else
|
||||
IO.eprintln s!"unknown language '{langId}'\n";
|
||||
return 1
|
||||
-- Remove up to `\n`
|
||||
pure <| String.Pos.Raw.extract contents endLinePos.offset contents.rawEndPos
|
||||
pure (contents.sliceFrom endLinePos).copy
|
||||
else
|
||||
pure contents
|
||||
let setup? ← setupFileName?.mapM ModuleSetup.load
|
||||
let setup? ← opts.setupFileName?.mapM ModuleSetup.load
|
||||
let mainModuleName ←
|
||||
if let some setup := setup? then
|
||||
pure setup.name
|
||||
else if let some fileName := fileName? then
|
||||
try moduleNameOfFileName fileName rootDir? catch e =>
|
||||
if oleanFileName?.isNone && cFileName?.isNone then
|
||||
try moduleNameOfFileName fileName opts.rootDir? catch e =>
|
||||
if opts.oleanFileName?.isNone && opts.cFileName?.isNone then
|
||||
pure `_stdin
|
||||
else
|
||||
throw e
|
||||
else
|
||||
pure `_stdin
|
||||
let env? ← Elab.runFrontend contents opts fileName mainModuleName trustLevel
|
||||
oleanFileName? ileanFileName? jsonOutput errorOnKinds #[] printStats setup?
|
||||
let env? ← Elab.runFrontend contents opts.leanOpts fileName mainModuleName
|
||||
opts.trustLevel opts.oleanFileName? opts.ileanFileName? opts.jsonOutput opts.errorOnKinds
|
||||
#[] opts.printStats setup?
|
||||
if let some env := env? then
|
||||
if run then
|
||||
return ← runMain env opts args
|
||||
if let some c := cFileName? then
|
||||
if opts.run then
|
||||
return ← runMain env opts.leanOpts args
|
||||
if let some c := opts.cFileName? then
|
||||
let .ok out ← IO.FS.Handle.mk c .write |>.toBaseIO
|
||||
| IO.eprintln s!"failed to create '{c}'"
|
||||
return 1
|
||||
profileitIO "C code generation" opts do
|
||||
profileitIO "C code generation" opts.leanOpts do
|
||||
let data ← IO.ofExcept <| IR.emitC env mainModuleName
|
||||
out.write data.toUTF8
|
||||
if let some bc := bcFileName? then
|
||||
if let some bc := opts.bcFileName? then
|
||||
initLLVM
|
||||
profileitIO "LLVM code generation" opts do
|
||||
profileitIO "LLVM code generation" opts.leanOpts do
|
||||
emitLLVM env mainModuleName bc
|
||||
displayCumulativeProfilingTimes
|
||||
if Internal.hasAddressSanitizer () then
|
||||
|
|
|
|||
|
|
@ -64,4 +64,9 @@ extern "C" LEAN_EXPORT lean_object * lean_kernel_check(lean_object * obj_env, le
|
|||
return type_checker(env.to_kernel_env(), local_ctx(lctx)).check(expr(a)).steal();
|
||||
});
|
||||
}
|
||||
|
||||
/* getBelieverTrustLevel (_ : Unit) : UInt32 */
|
||||
extern "C" LEAN_EXPORT uint32 lean_internal_get_believer_trust_level(obj_arg) {
|
||||
return LEAN_BELIEVER_TRUST_LEVEL;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -59,6 +59,12 @@ void enable_debug(char const * tag) {
|
|||
g_enabled_debug_tags->insert(tag);
|
||||
}
|
||||
|
||||
/* enableDebug (tag : @& String) : BaseIO Unit */
|
||||
extern "C" LEAN_EXPORT lean_obj_res lean_internal_enable_debug(b_lean_obj_arg tag) {
|
||||
enable_debug(lean_string_cstr(tag));
|
||||
return lean_box(0);
|
||||
}
|
||||
|
||||
void disable_debug(char const * tag) {
|
||||
if (g_enabled_debug_tags)
|
||||
g_enabled_debug_tags->erase(tag);
|
||||
|
|
|
|||
|
|
@ -106,6 +106,12 @@ extern "C" LEAN_EXPORT void lean_set_exit_on_panic(bool flag) {
|
|||
g_exit_on_panic = flag;
|
||||
}
|
||||
|
||||
/* setExitOnPanic (exit : Bool) : BaseIO Unit */
|
||||
extern "C" LEAN_EXPORT obj_res lean_internal_set_exit_on_panic(uint8 exit) {
|
||||
g_exit_on_panic = exit;
|
||||
return box(0);
|
||||
}
|
||||
|
||||
extern "C" LEAN_EXPORT void lean_set_panic_messages(bool flag) {
|
||||
g_panic_messages = flag;
|
||||
}
|
||||
|
|
@ -1014,6 +1020,11 @@ static unsigned get_lean_num_threads() {
|
|||
return hardware_concurrency();
|
||||
}
|
||||
|
||||
/* getHardwareConcurrency (_ : Unit) : UInt32 */
|
||||
extern "C" LEAN_EXPORT uint32 lean_internal_get_hardware_concurrency(obj_arg) {
|
||||
return hardware_concurrency();
|
||||
}
|
||||
|
||||
extern "C" LEAN_EXPORT void lean_init_task_manager() {
|
||||
lean_init_task_manager_using(get_lean_num_threads());
|
||||
}
|
||||
|
|
|
|||
|
|
@ -157,6 +157,12 @@ lthread::~lthread() {}
|
|||
void lthread::join() { m_imp->join(); }
|
||||
#endif
|
||||
|
||||
/* setThreadStackSize (sz : USize) : BaseIO Unit */
|
||||
extern "C" LEAN_EXPORT lean_obj_res lean_internal_set_thread_stack_size(size_t sz) {
|
||||
lthread::set_thread_stack_size(sz);
|
||||
return lean_box(0);
|
||||
}
|
||||
|
||||
LEAN_THREAD_VALUE(bool, g_finalizing, false);
|
||||
|
||||
bool in_thread_finalization() {
|
||||
|
|
|
|||
|
|
@ -9,6 +9,7 @@ Author: Leonardo de Moura
|
|||
#include "runtime/sstream.h"
|
||||
#include "util/options.h"
|
||||
#include "util/option_declarations.h"
|
||||
#include "stdlib_flags.h"
|
||||
|
||||
#ifndef LEAN_DEFAULT_VERBOSE
|
||||
#define LEAN_DEFAULT_VERBOSE true
|
||||
|
|
@ -50,6 +51,16 @@ bool get_verbose(options const & opts) {
|
|||
return opts.get_bool(*g_verbose, LEAN_DEFAULT_VERBOSE);
|
||||
}
|
||||
|
||||
/* getDefaultVerbose (_ : Unit) : Bool */
|
||||
extern "C" LEAN_EXPORT uint8 lean_internal_get_default_verbose(obj_arg) {
|
||||
return LEAN_DEFAULT_VERBOSE;
|
||||
}
|
||||
|
||||
/* getDefaultOptions (_ : Unit) : Options */
|
||||
extern "C" LEAN_EXPORT obj_res lean_internal_get_default_options(obj_arg) {
|
||||
return get_default_options().steal();
|
||||
}
|
||||
|
||||
options join(options const & opts1, options const & opts2) {
|
||||
kvmap r = opts2.m_value;
|
||||
for (kvmap_entry const & e : opts1.m_value) {
|
||||
|
|
|
|||
|
|
@ -68,6 +68,7 @@ public:
|
|||
*/
|
||||
friend options join(options const & opts1, options const & opts2);
|
||||
|
||||
object * steal() { return m_value.steal(); }
|
||||
object * to_obj_arg() const { return m_value.to_obj_arg(); }
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -40,7 +40,6 @@ Author: Leonardo de Moura
|
|||
#include "initialize/init.h"
|
||||
#include "library/ir_interpreter.h"
|
||||
#include "util/path.h"
|
||||
#include "stdlib_flags.h"
|
||||
#ifdef _MSC_VER
|
||||
#include <io.h>
|
||||
#define STDOUT_FILENO 1
|
||||
|
|
@ -157,33 +156,6 @@ int getopt_long(int argc, char *in_argv[], const char *optstring, const option *
|
|||
|
||||
using namespace lean; // NOLINT
|
||||
|
||||
extern "C" obj_res lean_display_header();
|
||||
static void display_header() {
|
||||
consume_io_result(lean_display_header());
|
||||
}
|
||||
|
||||
static void display_version(std::ostream & out) {
|
||||
out << get_short_version_string() << "\n";
|
||||
}
|
||||
|
||||
static void display_features(std::ostream & out) {
|
||||
out << "[";
|
||||
#if defined(LEAN_LLVM)
|
||||
out << "LLVM";
|
||||
#endif
|
||||
out << "]\n";
|
||||
}
|
||||
|
||||
extern "C" obj_res lean_display_help(uint8 use_stderr);
|
||||
static void display_help(bool use_stderr) {
|
||||
consume_io_result(lean_display_help(use_stderr));
|
||||
}
|
||||
|
||||
static int only_src_deps = 0;
|
||||
static int print_prefix = 0;
|
||||
static int print_libdir = 0;
|
||||
static int json_output = 0;
|
||||
|
||||
static struct option g_long_options[] = {
|
||||
{"version", no_argument, 0, 'v'},
|
||||
{"help", no_argument, 0, 'h'},
|
||||
|
|
@ -200,12 +172,12 @@ static struct option g_long_options[] = {
|
|||
{"stats", no_argument, 0, 'a'},
|
||||
{"quiet", no_argument, 0, 'q'},
|
||||
{"deps", no_argument, 0, 'd'},
|
||||
{"src-deps", no_argument, &only_src_deps, 1},
|
||||
{"deps-json", no_argument, 0, 'J'},
|
||||
{"src-deps", no_argument, 0, 'O'},
|
||||
{"deps-json", no_argument, 0, 'N'},
|
||||
{"timeout", optional_argument, 0, 'T'},
|
||||
{"c", optional_argument, 0, 'c'},
|
||||
{"bc", optional_argument, 0, 'b'},
|
||||
{"features", optional_argument, 0, 'f'},
|
||||
{"features", no_argument, 0, 'f'},
|
||||
{"exitOnPanic", no_argument, 0, 'e'},
|
||||
#if defined(LEAN_MULTI_THREAD)
|
||||
{"threads", required_argument, 0, 'j'},
|
||||
|
|
@ -217,9 +189,9 @@ static struct option g_long_options[] = {
|
|||
{"load-dynlib", required_argument, 0, 'l'},
|
||||
{"setup", required_argument, 0, 'u'},
|
||||
{"error", required_argument, 0, 'E'},
|
||||
{"json", no_argument, &json_output, 1},
|
||||
{"print-prefix", no_argument, &print_prefix, 1},
|
||||
{"print-libdir", no_argument, &print_libdir, 1},
|
||||
{"json", no_argument, 0, 'J'},
|
||||
{"print-prefix", no_argument, 0, 'x'},
|
||||
{"print-libdir", no_argument, 0, 'L'},
|
||||
#ifdef LEAN_DEBUG
|
||||
{"debug", required_argument, 0, 'B'},
|
||||
#endif
|
||||
|
|
@ -233,90 +205,9 @@ static char const * g_opt_str =
|
|||
#endif
|
||||
; // NOLINT
|
||||
|
||||
options set_config_option(options const & opts, char const * in) {
|
||||
if (!in) return opts;
|
||||
while (*in && std::isspace(*in))
|
||||
++in;
|
||||
std::string in_str(in);
|
||||
auto pos = in_str.find('=');
|
||||
if (pos == std::string::npos)
|
||||
throw lean::exception("invalid -D parameter, argument must contain '='");
|
||||
lean::name opt = lean::string_to_name(in_str.substr(0, pos));
|
||||
std::string val = in_str.substr(pos+1);
|
||||
auto decls = lean::get_option_declarations();
|
||||
auto it = decls.find(opt);
|
||||
if (it) {
|
||||
switch (it->kind()) {
|
||||
case lean::data_value_kind::Bool:
|
||||
if (val == "true")
|
||||
return opts.update(opt, true);
|
||||
else if (val == "false")
|
||||
return opts.update(opt, false);
|
||||
else
|
||||
throw lean::exception(lean::sstream() << "invalid -D parameter, invalid configuration option '" << opt
|
||||
<< "' value, it must be true/false");
|
||||
case lean::data_value_kind::Nat:
|
||||
return opts.update(opt, static_cast<unsigned>(atoi(val.c_str())));
|
||||
case lean::data_value_kind::String:
|
||||
return opts.update(opt, val.c_str());
|
||||
default:
|
||||
throw lean::exception(lean::sstream() << "invalid -D parameter, configuration option '" << opt
|
||||
<< "' cannot be set in the command line, use set_option command");
|
||||
}
|
||||
} else {
|
||||
// More options may be registered by imports, so we leave validating them to the Lean side.
|
||||
// This (minor) duplication will be resolved when this file is rewritten in Lean.
|
||||
return opts.update(opt, val.c_str());
|
||||
}
|
||||
}
|
||||
|
||||
namespace lean {
|
||||
extern "C" obj_res lean_shell_main(
|
||||
obj_arg args,
|
||||
obj_arg forwarded_args,
|
||||
uint8 component,
|
||||
uint8 print_prefix,
|
||||
uint8 print_libdir,
|
||||
uint8 use_stdin,
|
||||
uint8 only_deps,
|
||||
uint8 only_src_deps,
|
||||
uint8 deps_json,
|
||||
obj_arg opts,
|
||||
uint32_t trust_level,
|
||||
obj_arg root_dir,
|
||||
obj_arg setup_file_name,
|
||||
obj_arg olean_filename,
|
||||
obj_arg ilean_filename,
|
||||
obj_arg c_filename,
|
||||
obj_arg bc_filename,
|
||||
uint8 json_output,
|
||||
obj_arg error_kinds,
|
||||
uint8 print_stats,
|
||||
uint8 run
|
||||
);
|
||||
uint32 run_shell_main(
|
||||
int argc, char* argv[],
|
||||
buffer<string_ref> forwarded_args,
|
||||
int run_server,
|
||||
bool print_prefix,
|
||||
bool print_libdir,
|
||||
bool use_stdin,
|
||||
bool only_deps,
|
||||
bool only_src_deps,
|
||||
bool deps_json,
|
||||
options const & opts,
|
||||
uint32_t trust_level,
|
||||
optional<std::string> const & root_dir,
|
||||
optional<std::string> const & setup_file_name,
|
||||
optional<std::string> const & olean_file_name,
|
||||
optional<std::string> const & ilean_file_name,
|
||||
optional<std::string> const & c_file_name,
|
||||
optional<std::string> const & bc_file_name,
|
||||
bool json_output,
|
||||
array_ref<name> const & error_kinds,
|
||||
bool print_stats,
|
||||
bool run
|
||||
) {
|
||||
extern "C" obj_res lean_shell_main(obj_arg args, obj_arg shell_opts);
|
||||
int run_shell_main(int argc, char* argv[], object_ref const & shell_opts) {
|
||||
list_ref<string_ref> args;
|
||||
while (argc > 0) {
|
||||
argc--;
|
||||
|
|
@ -324,45 +215,51 @@ uint32 run_shell_main(
|
|||
}
|
||||
return get_io_scalar_result<uint32>(lean_shell_main(
|
||||
args.steal(),
|
||||
to_list_ref(forwarded_args).to_obj_arg(),
|
||||
run_server,
|
||||
print_prefix,
|
||||
print_libdir,
|
||||
use_stdin,
|
||||
only_deps, only_src_deps, deps_json,
|
||||
opts.to_obj_arg(),
|
||||
trust_level,
|
||||
root_dir ? mk_option_some(mk_string(*root_dir)) : mk_option_none(),
|
||||
setup_file_name ? mk_option_some(mk_string(*setup_file_name)) : mk_option_none(),
|
||||
olean_file_name ? mk_option_some(mk_string(*olean_file_name)) : mk_option_none(),
|
||||
ilean_file_name ? mk_option_some(mk_string(*ilean_file_name)) : mk_option_none(),
|
||||
c_file_name ? mk_option_some(mk_string(*c_file_name)) : mk_option_none(),
|
||||
bc_file_name ? mk_option_some(mk_string(*bc_file_name)) : mk_option_none(),
|
||||
json_output,
|
||||
error_kinds.to_obj_arg(),
|
||||
print_stats,
|
||||
run
|
||||
shell_opts.to_obj_arg()
|
||||
));
|
||||
}
|
||||
|
||||
extern "C" object* lean_init_search_path();
|
||||
void init_search_path() {
|
||||
get_io_scalar_result<unsigned>(lean_init_search_path());
|
||||
consume_io_result(lean_init_search_path());
|
||||
}
|
||||
|
||||
extern "C" object* lean_environment_free_regions(object * env);
|
||||
void environment_free_regions(elab_environment && env) {
|
||||
consume_io_result(lean_environment_free_regions(env.steal()));
|
||||
}
|
||||
extern "C" obj_res lean_shell_options_mk(obj_arg);
|
||||
object_ref mk_shell_options() {
|
||||
return object_ref(lean_shell_options_mk(box(0)));
|
||||
}
|
||||
|
||||
void check_optarg(char const * option_name) {
|
||||
if (!optarg) {
|
||||
std::cerr << "error: argument missing for option '-" << option_name << "'" << std::endl;
|
||||
std::exit(1);
|
||||
extern "C" obj_res lean_shell_options_process(obj_arg shell_opts, uint32 opt, obj_arg opt_arg);
|
||||
bool process_shell_option(object_ref & shell_opts, int opt, char const * optarg, int & rc) {
|
||||
auto optarg_ref = optarg ? mk_option_some(mk_string(optarg)) : mk_option_none();
|
||||
auto r = lean_shell_options_process(shell_opts.steal(), opt, optarg_ref);
|
||||
if (io_result_is_ok(r)) {
|
||||
shell_opts = object_ref(io_result_get_value(r), true);
|
||||
dec_ref(r);
|
||||
return false;
|
||||
} else {
|
||||
rc = unbox(io_result_get_error(r));
|
||||
dec_ref(r);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
extern "C" uint8 lean_shell_options_get_run(obj_arg shell_opts);
|
||||
bool get_shell_run(object_ref const & shell_opts) {
|
||||
return lean_shell_options_get_run(shell_opts.to_obj_arg());
|
||||
}
|
||||
|
||||
extern "C" uint8 lean_shell_options_get_profiler(obj_arg shell_opts);
|
||||
bool get_shell_profiler(object_ref const & shell_opts) {
|
||||
return lean_shell_options_get_profiler(shell_opts.to_obj_arg());
|
||||
}
|
||||
|
||||
extern "C" uint32 lean_shell_options_get_num_threads(obj_arg shell_opts);
|
||||
unsigned get_shell_num_threads(object_ref const & shell_opts) {
|
||||
return lean_shell_options_get_num_threads(shell_opts.to_obj_arg());
|
||||
}
|
||||
}
|
||||
|
||||
extern "C" object * lean_enable_initializer_execution();
|
||||
|
||||
namespace lean {
|
||||
|
|
@ -412,21 +309,6 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
|
|||
auto init_start = std::chrono::steady_clock::now();
|
||||
lean::initializer init;
|
||||
second_duration init_time = std::chrono::steady_clock::now() - init_start;
|
||||
bool run = false;
|
||||
optional<std::string> olean_fn;
|
||||
optional<std::string> ilean_fn;
|
||||
optional<std::string> setup_fn;
|
||||
bool use_stdin = false;
|
||||
unsigned trust_lvl = LEAN_BELIEVER_TRUST_LEVEL + 1;
|
||||
bool only_deps = false;
|
||||
bool deps_json = false;
|
||||
bool stats = false;
|
||||
// 0 = don't run server, 1 = watchdog, 2 = worker
|
||||
int run_server = 0;
|
||||
unsigned num_threads = 0;
|
||||
#if defined(LEAN_MULTI_THREAD)
|
||||
num_threads = hardware_concurrency();
|
||||
#endif
|
||||
|
||||
try {
|
||||
// Remark: This currently runs under `IO.initializing = true`.
|
||||
|
|
@ -437,167 +319,35 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
|
|||
}
|
||||
consume_io_result(lean_enable_initializer_execution());
|
||||
|
||||
options opts = get_default_options();
|
||||
optional<std::string> c_output;
|
||||
optional<std::string> llvm_output;
|
||||
optional<std::string> root_dir;
|
||||
buffer<string_ref> forwarded_args;
|
||||
buffer<name> error_kinds;
|
||||
|
||||
while (!run) { // stop consuming arguments after `--run`
|
||||
int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL);
|
||||
if (c == -1)
|
||||
break; // end of command line
|
||||
if (c == 0)
|
||||
continue; // long-only option
|
||||
switch (c) {
|
||||
case 'e':
|
||||
lean_set_exit_on_panic(true);
|
||||
break;
|
||||
case 'j':
|
||||
num_threads = static_cast<unsigned>(atoi(optarg));
|
||||
forwarded_args.push_back(string_ref("-j" + std::string(optarg)));
|
||||
break;
|
||||
case 'v':
|
||||
display_header();
|
||||
return 0;
|
||||
case 'V':
|
||||
display_version(std::cout);
|
||||
return 0;
|
||||
case 'g':
|
||||
std::cout << LEAN_GITHASH << "\n";
|
||||
return 0;
|
||||
case 'h':
|
||||
display_help(/* useStderr */ false);
|
||||
return 0;
|
||||
case 'f':
|
||||
display_features(std::cout);
|
||||
return 0;
|
||||
case 'c':
|
||||
check_optarg("c");
|
||||
c_output = optarg;
|
||||
break;
|
||||
case 'b':
|
||||
check_optarg("bc");
|
||||
llvm_output = optarg;
|
||||
break;
|
||||
case 's':
|
||||
lean::lthread::set_thread_stack_size(
|
||||
static_cast<size_t>((atoi(optarg) / 4) * 4) * static_cast<size_t>(1024));
|
||||
forwarded_args.push_back(string_ref("-s" + std::string(optarg)));
|
||||
break;
|
||||
case 'I':
|
||||
use_stdin = true;
|
||||
break;
|
||||
case 'r':
|
||||
run = true;
|
||||
break;
|
||||
case 'o':
|
||||
olean_fn = optarg;
|
||||
break;
|
||||
case 'i':
|
||||
ilean_fn = optarg;
|
||||
break;
|
||||
case 'R':
|
||||
root_dir = optarg;
|
||||
forwarded_args.push_back(string_ref("-R" + std::string(optarg)));
|
||||
break;
|
||||
case 'M':
|
||||
check_optarg("M");
|
||||
opts = opts.update(get_max_memory_opt_name(), static_cast<unsigned>(atoi(optarg)));
|
||||
forwarded_args.push_back(string_ref("-M" + std::string(optarg)));
|
||||
break;
|
||||
case 'T':
|
||||
check_optarg("T");
|
||||
opts = opts.update(get_timeout_opt_name(), static_cast<unsigned>(atoi(optarg)));
|
||||
forwarded_args.push_back(string_ref("-T" + std::string(optarg)));
|
||||
break;
|
||||
case 't':
|
||||
check_optarg("t");
|
||||
trust_lvl = atoi(optarg);
|
||||
forwarded_args.push_back(string_ref("-t" + std::string(optarg)));
|
||||
break;
|
||||
case 'q':
|
||||
opts = opts.update(lean::get_verbose_opt_name(), false);
|
||||
break;
|
||||
case 'd':
|
||||
only_deps = true;
|
||||
break;
|
||||
case 'J':
|
||||
only_deps = true;
|
||||
deps_json = true;
|
||||
break;
|
||||
case 'a':
|
||||
stats = true;
|
||||
break;
|
||||
case 'D':
|
||||
try {
|
||||
check_optarg("D");
|
||||
opts = set_config_option(opts, optarg);
|
||||
forwarded_args.push_back(string_ref("-D" + std::string(optarg)));
|
||||
} catch (lean::exception & ex) {
|
||||
std::cerr << ex.what() << std::endl;
|
||||
return 1;
|
||||
}
|
||||
break;
|
||||
case 'S':
|
||||
run_server = 1;
|
||||
break;
|
||||
case 'W':
|
||||
run_server = 2;
|
||||
break;
|
||||
case 'P':
|
||||
opts = opts.update("profiler", true);
|
||||
break;
|
||||
#if defined(LEAN_DEBUG)
|
||||
case 'B':
|
||||
check_optarg("B");
|
||||
lean::enable_debug(optarg);
|
||||
break;
|
||||
#endif
|
||||
case 'p':
|
||||
check_optarg("p");
|
||||
lean::load_plugin(optarg);
|
||||
forwarded_args.push_back(string_ref("--plugin=" + std::string(optarg)));
|
||||
break;
|
||||
case 'l':
|
||||
check_optarg("l");
|
||||
lean::load_dynlib(optarg);
|
||||
forwarded_args.push_back(string_ref("--load-dynlib=" + std::string(optarg)));
|
||||
break;
|
||||
case 'u':
|
||||
check_optarg("u");
|
||||
setup_fn = optarg;
|
||||
break;
|
||||
case 'E':
|
||||
check_optarg("E");
|
||||
error_kinds.push_back(string_to_name(std::string(optarg)));
|
||||
break;
|
||||
default:
|
||||
std::cerr << "Unknown command line option\n";
|
||||
display_help(/* useStderr */ true);
|
||||
return 1;
|
||||
int rc;
|
||||
object_ref shell_opts;
|
||||
try {
|
||||
shell_opts = mk_shell_options();
|
||||
for (;;) {
|
||||
int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL);
|
||||
if (c == -1)
|
||||
break; // end of command line
|
||||
if (process_shell_option(shell_opts, c, optarg, rc))
|
||||
return rc; // option processing triggered an early exit
|
||||
if (get_shell_run(shell_opts))
|
||||
break; // stop consuming arguments after `--run`
|
||||
}
|
||||
} catch (lean::throwable & ex) {
|
||||
std::cerr << "error: " << ex.what() << std::endl;
|
||||
return 1;
|
||||
}
|
||||
|
||||
lean::io_mark_end_initialization();
|
||||
|
||||
if (get_profiler(opts)) {
|
||||
if (get_shell_profiler(shell_opts)) {
|
||||
g_lean_report_task_get_blocked_time = report_task_get_blocked_time;
|
||||
report_profiling_time("initialization", init_time);
|
||||
}
|
||||
|
||||
scoped_task_manager scope_task_man(num_threads);
|
||||
scoped_task_manager scope_task_man(get_shell_num_threads(shell_opts));
|
||||
|
||||
try {
|
||||
return run_shell_main(
|
||||
argc - optind, argv + optind,
|
||||
forwarded_args, run_server, print_prefix, print_libdir,
|
||||
use_stdin, only_deps, only_src_deps, deps_json,
|
||||
opts, trust_lvl, root_dir, setup_fn,
|
||||
olean_fn, ilean_fn, c_output, llvm_output,
|
||||
json_output, error_kinds, stats, run
|
||||
);
|
||||
return run_shell_main(argc - optind, argv + optind, shell_opts);
|
||||
} catch (lean::throwable & ex) {
|
||||
std::cerr << ex.what() << "\n";
|
||||
} catch (std::bad_alloc & ex) {
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue