Skip to content

Commit 3772bb8

Browse files
authored
chore: revert "refactor: port shell option processing to Lean" (#11378)
Needs a fix to unbreak the Windows build first. Reverts #11345
1 parent 5a5f8c4 commit 3772bb8

File tree

9 files changed

+387
-442
lines changed

9 files changed

+387
-442
lines changed

src/Lean/Language/Lean.lean

Lines changed: 16 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -300,28 +300,6 @@ structure SetupImportsResult where
300300
/-- Lean plugins to load as part of the environment setup. -/
301301
plugins : Array System.FilePath := #[]
302302

303-
/--
304-
Parses an option value from a string and inserts it into `opts`.
305-
The type of the option is determined from `decl`.
306-
-/
307-
def setOption (opts : Options) (decl : OptionDecl) (name : Name) (val : String) : IO Options := do
308-
match decl.defValue with
309-
| .ofBool _ =>
310-
match val with
311-
| "true" => return opts.insert name true
312-
| "false" => return opts.insert name false
313-
| _ =>
314-
throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
315-
it must be true/false"
316-
| .ofNat _ =>
317-
let some val := val.toNat?
318-
| throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
319-
it must be a natural number"
320-
return opts.insert name val
321-
| .ofString _ => return opts.insert name val
322-
| _ => throw <| .userError s!"invalid -D parameter, configuration option '{name}' \
323-
cannot be set in the command line, use set_option command"
324-
325303
/--
326304
Parses values of options registered during import and left by the C++ frontend as strings.
327305
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
344322
let .ofString val := val
345323
| opts' := opts'.insert name val -- Already parsed
346324

347-
opts' ← setOption opts' decl name val
325+
match decl.defValue with
326+
| .ofBool _ =>
327+
match val with
328+
| "true" => opts' := opts'.insert name true
329+
| "false" => opts' := opts'.insert name false
330+
| _ =>
331+
throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
332+
it must be true/false"
333+
| .ofNat _ =>
334+
let some val := val.toNat?
335+
| throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
336+
it must be a natural number"
337+
opts' := opts'.insert name val
338+
| .ofString _ => opts' := opts'.insert name val
339+
| _ => throw <| .userError s!"invalid -D parameter, configuration option '{name}' \
340+
cannot be set in the command line, use set_option command"
348341

349342
return opts'
350343

0 commit comments

Comments
 (0)