logiccomp / lsl

4 stars 2 forks source link

No more blame highlighting #4

Closed dbp closed 10 months ago

dbp commented 10 months ago

I think with the switch to making check-contract report to rackunit, we lost error highlighting (or maybe it happened earlier?). With this example:

(: f (-> Integer Integer))
(define (f x)
  #f)
(check-contract f)

I get this in the interactions window:

Screenshot 2023-12-18 at 1 24 05 PM

But nothing highlighted in the definitions window.

(also, the location of the test seems off too: seems to be definition site for check-contract, rather than use site).

Especially since the blame only is at the level of the file, seems important to have the highlighting!

dbp commented 10 months ago

As a followup, this is even worse when there is indirection, e.g.,:

(: q (-> Integer Integer))
(define (q x)
  (g x))

(: g (-> Integer Integer))
(define (g x)
  (h x))

(: h (-> Integer Integer))
(define (h x)
  #f)

(check-contract q)

Produces the following error:

--------------------
unit tests > Unnamed test
. ../../../../code/lsl/lsl-lib/main.rkt:361:19: FAILURE
name:       check-contract
location:   /Users/dbp/code/lsl/lsl-lib/main.rkt:361:19
params:     '(#<procedure:...sl/lsl-lib/main.rkt:361:35>)

h: contract violation
  expected: Integer
  given: #f
  blaming: /Users/dbp/teaching/logics24/website/lectures/7.rkt
--------------------
0 success(es) 1 failure(s) 0 error(s) 1 test(s) run

Which has nothing about where the test that failed exists in code! I mean, it's correct that h is to blame, but the (check-contract q) seems important to include as well.

camoy commented 10 months ago

I did notice this, it happened when I removed syntax-spec. There's two things going on here:

  1. I figured out why the REPL wasn't working before and it was because errortrace disables the REPL. There was a fix for it (https://github.com/racket/errortrace/commit/574fd7ec038357a4475561df15e67f7594926f6a) and then that fix was reverted (https://github.com/racket/errortrace/commit/6fb1bd2a1c2de8af52d2bc85d096347381d17fee) so I'll have to see what to do here.
  2. The second thing is that the source location information is not getting propagated properly during expansion with ee-lib. I know how to fix this in a bad way, but I'll also see if there's a better solution.
camoy commented 10 months ago

With 87fb544 the error looks like this in DrRacket:

2023-12-19_21-45

However, using check-contract will not show this. In general you can have more than one check-contract failing so Rackunit suppresses any debugging information that would be displayed for each test. But that seems ok, yes?

dbp commented 10 months ago

@camoy I think not having error highlighting with tests makes sense, but the blame locations need to be in the error (which of course you know!).