Zulip Chat Archive

Stream: general

Topic: error: interrupted


Reid Barton (Jun 02 2018 at 00:20):

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

Simon Hudon (Jun 02 2018 at 00:21):

I get the same error.

Simon Hudon (Jun 02 2018 at 00:22):

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 (Jun 02 2018 at 00:23):

Linux here

Simon Hudon (Jun 02 2018 at 00:25):

@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 (Jun 02 2018 at 00:25):

Are you well versed in Emacs Lisp?

Reid Barton (Jun 02 2018 at 00:28):

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

Reid Barton (Jun 02 2018 at 00:28):

It's quite irritating

Simon Hudon (Jun 02 2018 at 00:51):

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 (Jun 02 2018 at 01:05):

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 (Jun 02 2018 at 01:09):

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

Reid Barton (Jun 02 2018 at 01:09):

Is that the right issue?

Reid Barton (Jun 02 2018 at 01:11):

okay, a (require 'company) fixed that

Simon Hudon (Jun 02 2018 at 01:11):

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

Reid Barton (Jun 02 2018 at 01:11):

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

Reid Barton (Jun 02 2018 at 01:14):

Oh, it already stopped working

Simon Hudon (Jun 02 2018 at 01:14):

Darn! I was hoping!

Simon Hudon (Jun 02 2018 at 01:41):

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 (Jun 02 2018 at 01:48):

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

Simon Hudon (Jun 02 2018 at 01:55):

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

Reid Barton (Jun 02 2018 at 01:56):

Unfortunately I finished proving the thing I was trying to prove

Simon Hudon (Jun 02 2018 at 02:00):

I guess we'll never know

Sebastian Ullrich (Jun 02 2018 at 07:08):

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

Simon Hudon (Jun 02 2018 at 11:16):

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

Sebastian Ullrich (Jun 03 2018 at 18:09):

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 (Jun 03 2018 at 18:42):

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 (Jun 03 2018 at 18:51):

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

Simon Hudon (Jun 03 2018 at 20:50):

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

Sebastian Ullrich (Jun 03 2018 at 20:54):

Sure, thanks

Simon Hudon (Jun 03 2018 at 21:00):

Done


Last updated: Dec 20 2023 at 11:08 UTC