From 3772bb8685f2fdf414e8aa4af6f1d2964b2f64af Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 26 Nov 2025 10:28:48 +0100 Subject: [PATCH] chore: revert "refactor: port shell option processing to Lean" (#11378) Needs a fix to unbreak the Windows build first. Reverts leanprover/lean4#11345 --- src/Lean/Language/Lean.lean | 39 ++-- src/Lean/Shell.lean | 382 +++++-------------------------- src/library/elab_environment.cpp | 5 - src/runtime/debug.cpp | 6 - src/runtime/object.cpp | 11 - src/runtime/thread.cpp | 6 - src/util/options.cpp | 11 - src/util/options.h | 1 - src/util/shell.cpp | 368 ++++++++++++++++++++++++----- 9 files changed, 387 insertions(+), 442 deletions(-) diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean index b8af3376f0..a981d0a749 100644 --- a/src/Lean/Language/Lean.lean +++ b/src/Lean/Language/Lean.lean @@ -300,28 +300,6 @@ 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 @@ -344,7 +322,22 @@ 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 - opts' ← setOption opts' decl name val + 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" return opts' diff --git a/src/Lean/Shell.lean b/src/Lean/Shell.lean index cd59774d99..af3c89ffdb 100644 --- a/src/Lean/Shell.lean +++ b/src/Lean/Shell.lean @@ -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 (i.e., `LEAN_MULTI_THREAd`). -/ +/-- Whether Lean was built with multithread support. -/ @[extern "lean_internal_is_multi_thread"] opaque Internal.isMultiThread (_ : Unit) : Bool -/-- Whether Lean was built in debug mode (i.e., `LEAN_DEBUG`). -/ +/-- Whether Lean was built in debug mode. -/ @[extern "lean_internal_is_debug"] opaque Internal.isDebug (_ : Unit) : Bool -/-- Returns the mode Lean was built in (i.e., `LEAN_BUILD_TYPE`). -/ +/-- Returns the mode Lean was built in. -/ @[extern "lean_internal_get_build_type"] opaque Internal.getBuildType (_ : Unit) : String @@ -89,27 +89,7 @@ opaque Internal.getDefaultMaxHeartbeat (_ : Unit) : Nat @[extern "lean_internal_set_max_heartbeat"] opaque Internal.setMaxHeartbeat (max : USize) : BaseIO Unit -/-- 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`. --/ +/-- Lean equivalent of `LEAN_VERSION_STRING` / `g_short_version_string` -/ def shortVersionString : String := if version.specialDesc ≠ "" then s!"{versionStringCore}-{version.specialDesc}" @@ -127,17 +107,13 @@ def versionHeader : String := Id.run do ver := s!"{ver}, commit {githash}" s!"Lean (version {ver}, {Internal.getBuildType ()})" -/-- -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 version header. -/ +@[export lean_display_header] +def displayHeader : IO Unit := do + IO.println versionHeader /-- 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 @@ -153,7 +129,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 " -R, --root=dir set package root directory from which the module name\n" + out.putStrLn " --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" @@ -172,7 +148,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" @@ -194,285 +170,52 @@ 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) (opts : ShellOptions) : IO UInt32 := do - if opts.printPrefix then +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 IO.println (← getBuildDir) return 0 - if opts.printLibDir then + if printLibDir then IO.println (← getLibDir (← getBuildDir)) return 0 - let maxMemory := maxMemory.get opts.leanOpts + let maxMemory := maxMemory.get opts if maxMemory != 0 then Internal.setMaxMemory (maxMemory.toUSize * 1024 * 1024) - let timeout := timeout.get opts.leanOpts + let timeout := timeout.get opts if timeout != 0 then Internal.setMaxHeartbeat (timeout.toUSize * 1000) - match opts.component with + match component with | .frontend => pure () | .watchdog => - return ← Server.Watchdog.watchdogMain opts.forwardedArgs.toList + return ← Server.Watchdog.watchdogMain forwardedArgs | .worker => - return ← Server.FileWorker.workerMain opts.leanOpts - if opts.onlyDeps && opts.depsJson then + return ← Server.FileWorker.workerMain opts + if onlyDeps && depsJson then let fns ← - if opts.useStdin then + if useStdin then (← IO.getStdin).lines else pure args.toArray @@ -482,73 +225,72 @@ def shellMain (args : List String) (opts : ShellOptions) : IO UInt32 := do match args with | fileName :: args => (some fileName, args) | [] => (none, args) - if !opts.run && !args.isEmpty then + if !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 opts.useStdin then + else if useStdin then pure "" else IO.eprintln "Expected exactly one file name" displayHelp (useStderr := true) return 1 let contents ← decodeLossyUTF8 <$> do - if opts.useStdin then + if useStdin then (← IO.getStdin).readBinToEnd else IO.FS.readBinFile fileName - if opts.onlyDeps then + if onlyDeps then Elab.printImports contents fileName return 0 - if opts.onlySrcDeps then + if onlySrcDeps then Elab.printImportSrcs contents fileName return 0 -- Quick and dirty `#lang` support ---TODO: make it extensible, and add `lean4md` let contents ← - if let some contents := contents.dropPrefix? "#lang" then + if contents.startsWith "#lang" then let endLinePos := contents.find '\n' - let langId := contents.sliceTo endLinePos |>.trimAscii + let langId := String.Pos.Raw.extract contents ⟨6⟩ endLinePos.offset |>.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 (contents.sliceFrom endLinePos).copy + pure <| String.Pos.Raw.extract contents endLinePos.offset contents.rawEndPos else pure contents - let setup? ← opts.setupFileName?.mapM ModuleSetup.load + let setup? ← 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 opts.rootDir? catch e => - if opts.oleanFileName?.isNone && opts.cFileName?.isNone then + try moduleNameOfFileName fileName rootDir? catch e => + if oleanFileName?.isNone && cFileName?.isNone then pure `_stdin else throw e else pure `_stdin - let env? ← Elab.runFrontend contents opts.leanOpts fileName mainModuleName - opts.trustLevel opts.oleanFileName? opts.ileanFileName? opts.jsonOutput opts.errorOnKinds - #[] opts.printStats setup? + let env? ← Elab.runFrontend contents opts fileName mainModuleName trustLevel + oleanFileName? ileanFileName? jsonOutput errorOnKinds #[] printStats setup? if let some env := env? then - if opts.run then - return ← runMain env opts.leanOpts args - if let some c := opts.cFileName? then + if run then + return ← runMain env opts args + if let some c := 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.leanOpts do + profileitIO "C code generation" opts do let data ← IO.ofExcept <| IR.emitC env mainModuleName out.write data.toUTF8 - if let some bc := opts.bcFileName? then + if let some bc := bcFileName? then initLLVM - profileitIO "LLVM code generation" opts.leanOpts do + profileitIO "LLVM code generation" opts do emitLLVM env mainModuleName bc displayCumulativeProfilingTimes if Internal.hasAddressSanitizer () then diff --git a/src/library/elab_environment.cpp b/src/library/elab_environment.cpp index 95d3680254..49ef3e6fe0 100644 --- a/src/library/elab_environment.cpp +++ b/src/library/elab_environment.cpp @@ -64,9 +64,4 @@ 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; -} } diff --git a/src/runtime/debug.cpp b/src/runtime/debug.cpp index ecd5da1bfc..ee4f917100 100644 --- a/src/runtime/debug.cpp +++ b/src/runtime/debug.cpp @@ -59,12 +59,6 @@ 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); diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index c03af87615..bee8738d62 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -106,12 +106,6 @@ 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; } @@ -1020,11 +1014,6 @@ 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()); } diff --git a/src/runtime/thread.cpp b/src/runtime/thread.cpp index ba06b37d13..7df3d8f2f7 100644 --- a/src/runtime/thread.cpp +++ b/src/runtime/thread.cpp @@ -157,12 +157,6 @@ 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() { diff --git a/src/util/options.cpp b/src/util/options.cpp index 0c01fb54c0..365448881a 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -9,7 +9,6 @@ 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 @@ -51,16 +50,6 @@ bool get_verbose(options const & opts) { return opts.get_bool(*g_verbose, LEAN_DEFAULT_VERBOSE); } -/* getDefaultVerbose (_ : Unit) : Bool */ -extern "C" uint8 lean_internal_get_default_verbose(obj_arg) { - return LEAN_DEFAULT_VERBOSE; -} - -/* getDefaultOptions (_ : Unit) : Options */ -extern "C" 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) { diff --git a/src/util/options.h b/src/util/options.h index f1908f8b55..75c9ea1f47 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -68,7 +68,6 @@ 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(); } }; diff --git a/src/util/shell.cpp b/src/util/shell.cpp index bcf7eaf74a..7ef4c515ad 100644 --- a/src/util/shell.cpp +++ b/src/util/shell.cpp @@ -40,6 +40,7 @@ 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 #define STDOUT_FILENO 1 @@ -156,6 +157,33 @@ 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'}, @@ -172,12 +200,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, 0, 'O'}, - {"deps-json", no_argument, 0, 'N'}, + {"src-deps", no_argument, &only_src_deps, 1}, + {"deps-json", no_argument, 0, 'J'}, {"timeout", optional_argument, 0, 'T'}, {"c", optional_argument, 0, 'c'}, {"bc", optional_argument, 0, 'b'}, - {"features", no_argument, 0, 'f'}, + {"features", optional_argument, 0, 'f'}, {"exitOnPanic", no_argument, 0, 'e'}, #if defined(LEAN_MULTI_THREAD) {"threads", required_argument, 0, 'j'}, @@ -189,9 +217,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, 0, 'J'}, - {"print-prefix", no_argument, 0, 'x'}, - {"print-libdir", no_argument, 0, 'L'}, + {"json", no_argument, &json_output, 1}, + {"print-prefix", no_argument, &print_prefix, 1}, + {"print-libdir", no_argument, &print_libdir, 1}, #ifdef LEAN_DEBUG {"debug", required_argument, 0, 'B'}, #endif @@ -205,9 +233,90 @@ 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(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 shell_opts); -int run_shell_main(int argc, char* argv[], object_ref const & shell_opts) { +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 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 const & root_dir, + optional const & setup_file_name, + optional const & olean_file_name, + optional const & ilean_file_name, + optional const & c_file_name, + optional const & bc_file_name, + bool json_output, + array_ref const & error_kinds, + bool print_stats, + bool run +) { list_ref args; while (argc > 0) { argc--; @@ -215,51 +324,45 @@ int run_shell_main(int argc, char* argv[], object_ref const & shell_opts) { } return get_io_scalar_result(lean_shell_main( args.steal(), - shell_opts.to_obj_arg() + 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 )); } extern "C" object* lean_init_search_path(); void init_search_path() { - consume_io_result(lean_init_search_path()); + get_io_scalar_result(lean_init_search_path()); } -extern "C" obj_res lean_shell_options_mk(obj_arg); -object_ref mk_shell_options() { - return object_ref(lean_shell_options_mk(box(0))); +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_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; +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" 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 { @@ -309,6 +412,21 @@ 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 olean_fn; + optional ilean_fn; + optional 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`. @@ -319,35 +437,167 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) { } consume_io_result(lean_enable_initializer_execution()); - 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` + options opts = get_default_options(); + optional c_output; + optional llvm_output; + optional root_dir; + buffer forwarded_args; + buffer 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(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((atoi(optarg) / 4) * 4) * static_cast(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(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(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; } - } catch (lean::throwable & ex) { - std::cerr << "error: " << ex.what() << std::endl; - return 1; } lean::io_mark_end_initialization(); - if (get_shell_profiler(shell_opts)) { + if (get_profiler(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(get_shell_num_threads(shell_opts)); + scoped_task_manager scope_task_man(num_threads); try { - return run_shell_main(argc - optind, argv + optind, shell_opts); + 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 + ); } catch (lean::throwable & ex) { std::cerr << ex.what() << "\n"; } catch (std::bad_alloc & ex) {