mortberg / cubicaltt

Experimental implementation of Cubical Type Theory
https://arxiv.org/abs/1611.02108
MIT License
572 stars 76 forks source link

Parser error messages are truncated too much #95

Closed necrosovereign closed 6 years ago

necrosovereign commented 6 years ago

In the file Main.hs at the lines 93-94 there is an expression

    (\e -> do putStrLn ("Exception: " ++ takeWhile (/='\n')
                                 (show (e :: SomeException)))

Which, as I understand, is used to catch exception arising from parsing files.

The presence of takeWhile (/='\n') in the expression causes the parser error message to be truncated to Exception: Parse failed in "filename". I am not sure if this is the intended behaviour

mortberg commented 6 years ago

Interesting. Can you post an example of what the errors look like without this truncation?

necrosovereign commented 6 years ago

For example, the following code:

module m where

T (A : U) : U = A = A

causes error message with the following text:

Exception: Parse failed in "m.ctt"
"syntax error at line 3 before = A }"
CallStack (from HasCallStack):
  error, called at Main.hs:188:16 in main:Main
mortberg commented 6 years ago

Ah right, so with the truncation you don't get the line number? That's what I was suspecting...

I suspect that we wanted to remove the CallStack part but ended up removing too much. How about using lines and then takeWhile (/= "CallStack (from HasCallStack):") ?

necrosovereign commented 6 years ago

I really don't know what is the best solution in this case. Removing the truncation completely works for me

mortberg commented 6 years ago

I finally found some free time and pushed: https://github.com/mortberg/cubicaltt/commit/452d973fae544861090fbdea51f4f5da653fb394

This should solve this issue so I'm closing.