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

fix: lowercase error messages

Browse source
This commit is contained in:
Simon Hudon 2020-01-12 13:53:34 -05:00 • committed by Leonardo de Moura
parent 6c9d408799
commit dd6e95c718
2 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -152,16 +152,16 @@ timeExpired
private def downCaseFirst (s : String) : String := s.modify 0 Char.toLower
def fopenErrorToString (gist fn : String) (code : UInt32) : Option String → String
| some details => gist ++ " (error code: " ++ toString code ++ ", " ++ downCaseFirst details ++ ")\n file: " ++ fn
| none => gist ++ " (error code: " ++ toString code ++ ")\n file: " ++ fn
| some details => downCaseFirst gist ++ " (error code: " ++ toString code ++ ", " ++ downCaseFirst details ++ ")\n file: " ++ fn
| none => downCaseFirst gist ++ " (error code: " ++ toString code ++ ")\n file: " ++ fn
def otherErrorToString (gist : String) (code : UInt32) : Option String → String
| some details => gist ++ " (error code: " ++ toString code ++ ", " ++ downCaseFirst details ++ ")"
| none => gist ++ " (error code: " ++ toString code ++ ")"
| some details => downCaseFirst gist ++ " (error code: " ++ toString code ++ ", " ++ downCaseFirst details ++ ")"
| none => downCaseFirst gist ++ " (error code: " ++ toString code ++ ")"
@[export lean_io_error_to_string]
def toString : IO.Error → String
| unexpectedEof => "End of file"
| 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

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

@ -3,7 +3,7 @@ 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_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)