Add %used directive for idris_crash
Without it, it might fail to compile if there's a more complicated
message than just a string
commit6d8bfbc9fdbb2fb17ad8b9b403587b5a516d923c
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateFri 9 Dec 2016, 13:57 (10 years ago)
parent4a5c677
libs/base/Debug/Error.idr+3−5
@@ -12,8 +12,6 @@ error : {default (%runElab sourceLocation) loc : SourceLocation} ->
1212 (message : String) ->
1313 a
1414error {loc = FileLoc filename (line, col) _} message =
15− unsafePerformIO $
16− do let place = filename ++ " line " ++ show line ++ " column " ++ show col
17− let message' = place ++ ": " ++ message
18− putStrLn message'
19− exit 1
15+ let place = filename ++ " line " ++ show line ++ " column " ++ show col
16+ message' = place ++ ": " ++ message in
17+ idris_crash message'
libs/prelude/Builtins.idr+3−1
@@ -179,9 +179,11 @@ assert_unreachable : a
179179-- compiled as primitive
180180
181181||| Abort immediately with an error message
182−idris_crash : String -> a
182+idris_crash : (msg : String) -> a
183183-- compiled as primitive
184184
185+%used idris_crash msg
186+
185187||| Subvert the type checker. This function is abstract, so it will not reduce in
186188||| the type checker. Use it with care - it can result in segfaults or worse!
187189export