From 64ef03d73693611c1e0d775d241da62a7ad6bcf4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 12 Jan 2020 08:21:26 -0800 Subject: [PATCH] chore: lowercase error messages @cipher1024 We use lowercase error messages in Lean. I know other systems capitalize, but we need consistency. --- src/Init/System/IOError.lean | 38 ++++++++++---------- tests/lean/eval_except.lean.expected.out | 2 +- tests/lean/file_not_found.lean.expected.out | 4 +-- tests/lean/run/print_error.lean.expected.out | 2 +- 4 files changed, 23 insertions(+), 23 deletions(-) diff --git a/src/Init/System/IOError.lean b/src/Init/System/IOError.lean index 4facdfbd18..3f87126dd7 100644 --- a/src/Init/System/IOError.lean +++ b/src/Init/System/IOError.lean @@ -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 ⟩ diff --git a/tests/lean/eval_except.lean.expected.out b/tests/lean/eval_except.lean.expected.out index cfc1a5e905..4d8c822d0f 100644 --- a/tests/lean/eval_except.lean.expected.out +++ b/tests/lean/eval_except.lean.expected.out @@ -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 diff --git a/tests/lean/file_not_found.lean.expected.out b/tests/lean/file_not_found.lean.expected.out index d770a6fd80..d90ee82c42 100644 --- a/tests/lean/file_not_found.lean.expected.out +++ b/tests/lean/file_not_found.lean.expected.out @@ -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) diff --git a/tests/lean/run/print_error.lean.expected.out b/tests/lean/run/print_error.lean.expected.out index 3aee74080e..5b8659dd96 100644 --- a/tests/lean/run/print_error.lean.expected.out +++ b/tests/lean/run/print_error.lean.expected.out @@ -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