Skip to content

Commit 2a4088c

Browse files
committed
fix(Cache): option order in usage & error messages (leanprover-community#33735)
This PR fixes cache's help text to indicate that options must come before the command (in `Usage:`). It also improves the error messages produced when an option or other invalid identifier appears as an argument.
1 parent c627e66 commit 2a4088c

File tree

2 files changed

+7
-1
lines changed

2 files changed

+7
-1
lines changed

Cache/IO.lean

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -472,6 +472,9 @@ Note: An argument like `Archive` is treated as module, not a path.
472472
-/
473473
def leanModulesFromSpec (sp : SearchPath) (argₛ : String) :
474474
IO <| Except String <| Array (Name × FilePath) := do
475+
if argₛ.startsWith "-" then
476+
-- provided option after command
477+
return .error s!"Invalid argument: option must come before command {argₛ}"
475478
-- TODO: This could be just `FilePath.normalize` if the TODO there was addressed
476479
let arg : FilePath := System.mkFilePath <|
477480
(argₛ : FilePath).normalize.components.filter (· != "")
@@ -491,6 +494,9 @@ def leanModulesFromSpec (sp : SearchPath) (argₛ : String) :
491494
else
492495
-- provided a module
493496
let mod := argₛ.toName
497+
if mod.isAnonymous then
498+
-- provided a module name which is not a valid Lean identifier
499+
return .error s!"Invalid argument: expected path or module name, not {argₛ}"
494500
let sourceFile ← Lean.findLean sp mod
495501
if ← sourceFile.pathExists then
496502
-- (1.) provided valid module

Cache/Main.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ Authors: Arthur Paulino, Jon Eugster
77
import Cache.Requests
88

99
def help : String := "Mathlib4 caching CLI
10-
Usage: cache [COMMAND] [OPTIONS]
10+
Usage: cache [OPTIONS] [COMMAND]
1111
1212
Commands:
1313
# No privilege required

0 commit comments

Comments
 (0)