error: interrupted

Stream: general

[Reid Barton]

Does anyone know why this often happens when using jump-to-definition? (I'm in emacs if it matters.)

[Simon Hudon]

I get the same error.

[Simon Hudon]

I thought it might be a problem with company-mode but I wasn't able to find anything. Are you also on a Mac?

[Reid Barton]

Linux here

[Simon Hudon]

@Sebastian Ullrich also I think and I remember he didn't have the same error so I thought it might be because of mac. It must be something else

[Simon Hudon]

Are you well versed in Emacs Lisp?

[Reid Barton]

Not especially, but I would try to debug it if the issue is not already understood.

[Reid Barton]

It's quite irritating

[Simon Hudon]

it is indeed. I just added print statements in lean-find-definition in lean-mode but I can't get it to fail now ... :/

[Simon Hudon]

Do you have:

(global-set-key (kbd "S-SPC") #'company-complete)

in your init file? I found a thread on the github repo (https://github.com/company-mode/company-mode/issues/69) that suggests replacing it with:

(define-key company-mode-map (kbd "S-SPC") #'company-complete)

It seems to help but the bug has been showing up inconsistently. Can you try it and tell me if it helps?

[Reid Barton]

I got Symbol's value as variable is void: company-mode-map

[Reid Barton]

Is that the right issue?

[Reid Barton]

okay, a (require 'company) fixed that

[Simon Hudon]

That's the one that helped me. Do you have (require 'company) before that line?

[Reid Barton]

Well, it's working at the moment, but it usually does after restarting emacs :)

[Reid Barton]

Oh, it already stopped working

[Simon Hudon]

Darn! I was hoping!

[Simon Hudon]

In lean-input.el, in lean-find-definition, can you try adding print statements inside the lambda expression? Like this:

(defun lean-find-definition ()
  "Jump to definition of thing at point"
  (interactive)
  (lean-get-info-record-at-point
   (lambda (info-record)
     (print "begin")
     (-if-let (source-record (plist-get info-record :source))
         (apply #'lean-find-definition-cont source-record)
       (-if-let (id (plist-get info-record :full-id))
           (message "no source location available for %s" id)
         (message "unknown thing at point")))
     (print "end"))))

[Reid Barton]

Well... I tried adding those and it's working again.
Did editing the .el file cause emacs to reload the mode automatically?

[Simon Hudon]

I don't know. I wonder if the printing introduces a delay. Let's try removing the print statements

[Reid Barton]

Unfortunately I finished proving the thing I was trying to prove

[Simon Hudon]

I guess we'll never know

[Sebastian Ullrich]

This is a known issue (to me :) ) where go-to-definition doesn't work while the goal display is open

[Simon Hudon]

That's very good to know! Is this on the emacs side or on the Lean side?

[Sebastian Ullrich]

That requests are interrupted by unrelated requests is an issue with the Lean server. But lean-mode could try to work around that by not sending a goal request directly after a find definition request.

[Simon Hudon]

Do you think if we set a timer for masking requests for half a second after find definition that might be good enough?

[Sebastian Ullrich]

It should be sufficient to suppress the next execution of lean-show-goal--handler after lean-find-definition has run, probably?

[Simon Hudon]

That seems to be enough. Do you want a PR for it?

[Sebastian Ullrich]

Sure, thanks

[Simon Hudon]

Done