max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: lowercase error messages

Browse source 
@cipher1024 We use lowercase error messages in Lean. I know other
systems capitalize, but we need consistency.
This commit is contained in:
Leonardo de Moura 2020-01-12 08:21:26 -08:00
parent 07edbd395e
commit 64ef03d736
4 changed files with 23 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/Init/System/IOError.lean
View file

@ -162,28 +162,28 @@ def otherErrorToString (gist : String) (code : UInt32) : Option String → Strin
@[export lean_io_error_to_string]
def toString : IO.Error → String
| unexpectedEof => "End of file"
| inappropriateType (some fn) code details => fopenErrorToString "Inappropriate type" fn code details
| inappropriateType none code details => otherErrorToString "Inappropriate type" code details
| interrupted fn code details => fopenErrorToString "Interrupted system call" fn code details
| invalidArgument (some fn) code details => fopenErrorToString "Invalid argument" fn code details
| invalidArgument none code details => otherErrorToString "Invalid argument" code details
| noFileOrDirectory fn code _ => fopenErrorToString "No such file or directory" fn code none
| noSuchThing (some fn) code details => fopenErrorToString "No such thing" fn code details
| noSuchThing none code details => otherErrorToString "No such thing" code details
| inappropriateType (some fn) code details => fopenErrorToString "inappropriate type" fn code details
| inappropriateType none code details => otherErrorToString "inappropriate type" code details
| interrupted fn code details => fopenErrorToString "interrupted system call" fn code details
| invalidArgument (some fn) code details => fopenErrorToString "invalid argument" fn code details
| invalidArgument none code details => otherErrorToString "invalid argument" code details
| noFileOrDirectory fn code _ => fopenErrorToString "no such file or directory" fn code none
| noSuchThing (some fn) code details => fopenErrorToString "no such thing" fn code details
| noSuchThing none code details => otherErrorToString "no such thing" code details
| permissionDenied (some fn) code details => fopenErrorToString details fn code none
| permissionDenied none code details => otherErrorToString details code none
| resourceExhausted (some fn) code details => fopenErrorToString "Resource exhausted" fn code details
| resourceExhausted none code details => otherErrorToString "Resource exhausted" code details
| alreadyExists code details => otherErrorToString "Already exists" code details
| resourceExhausted (some fn) code details => fopenErrorToString "resource exhausted" fn code details
| resourceExhausted none code details => otherErrorToString "resource exhausted" code details
| alreadyExists code details => otherErrorToString "already exists" code details
| otherError code details => otherErrorToString details code none
| resourceBusy code details => otherErrorToString "Resource busy" code details
| resourceVanished code details => otherErrorToString "Resource vanished" code details
| hardwareFault code _ => otherErrorToString "Hardware fault" code none
| illegalOperation code details => otherErrorToString "Illegal operation" code details
| protocolError code details => otherErrorToString "Protocol error" code details
| timeExpired code details => otherErrorToString "Time expired" code details
| unsatisfiedConstraints code _ => otherErrorToString "Directory not empty" code none
| unsupportedOperation code details => otherErrorToString "Unsupported operation" code details
| resourceBusy code details => otherErrorToString "resource busy" code details
| resourceVanished code details => otherErrorToString "resource vanished" code details
| hardwareFault code _ => otherErrorToString "hardware fault" code none
| illegalOperation code details => otherErrorToString "illegal operation" code details
| protocolError code details => otherErrorToString "protocol error" code details
| timeExpired code details => otherErrorToString "time expired" code details
| unsatisfiedConstraints code _ => otherErrorToString "directory not empty" code none
| unsupportedOperation code details => otherErrorToString "unsupported operation" code details
| userError msg => msg
instance : HasToString IO.Error := ⟨ IO.Error.toString ⟩

2
tests/lean/eval_except.lean.expected.out
View file

@ -1,5 +1,5 @@
eval_except.lean:4:0: error: this is my error
eval_except.lean:5:0: error: No such file or directory (error code: 31)
eval_except.lean:5:0: error: no such file or directory (error code: 31)
file: file.ext

4
tests/lean/file_not_found.lean.expected.out
View file

@ -1,9 +1,9 @@
file_not_found.lean:6:0: error: No such file or directory (error code: 2)
file_not_found.lean:6:0: error: no such file or directory (error code: 2)
file: non-existent-file.txt
file_not_found.lean:12:0: error: Permission denied (error code: 13)
file: readonly.txt
file_not_found.lean:13:0: error: Invalid argument (error code: 9, bad file descriptor)
file_not_found.lean:13:0: error: invalid argument (error code: 9, bad file descriptor)

2
tests/lean/run/print_error.lean.expected.out
View file

@ -1,2 +1,2 @@
uncaught exception: No such file or directory (error code: 13)
uncaught exception: no such file or directory (error code: 13)
file: file.ext