m-fleury / isabelle-emacs

Clone of isabelle, with LSP extensions in seperate branches
Other
25 stars 5 forks source link

infinite looping? #15

Closed gh-salt closed 4 years ago

gh-salt commented 4 years ago

When I select a section of text and press tabulation, emacs gets stuck and I have to kill the process with kill -9

gh-salt commented 4 years ago

This also happens when I attempt to paste anything into the main .thy buffer (this is new, it didn't happen before last week-end, contrarily to what I report in the previous message about tabulation)

m-fleury commented 4 years ago

That is bad.

Are you really using the indentation mode? (check for "activating experimental feature is lsp-isar. Set lsp-isar-experimental to nil to avoid it" in Message)

EDIT: If this forbids you to work, set lsp-isar-experimental to nil.

gh-salt commented 4 years ago

I don't have this message about the experimental feature in Message and I have nothing (uncommented) about lsp-isar-experimental in my dotfile. If I add (setq lsp-isar-experimental nil) in the user-init section of my dotfile, it appears to fix the issue

gh-salt commented 4 years ago

I find it a bit strange that the experimental mode would be enabled by default.

gh-salt commented 4 years ago

Forget my forelast comment, the looping still happens when I do a copy-paste...

gh-salt commented 4 years ago

I'll try to rollback to the last commit before the week-end to see if the issue is still there.

m-fleury commented 4 years ago

Try pressing C-g to interrupt whatever is currently running.

gh-salt commented 4 years ago

C-g does the job! :)

It appear the paste loop happens only once lsp has started. Before that, I can paste as much as I want without looping.

EDIT: the tab loop also still happens by the way, and it can also be stopped by C-g

m-fleury commented 4 years ago

I cannot reproduce it (even in spacemacs). So, I would need additional information

M-x toggle-debug-on-quit < reproduce the bug > send me the trace.

If no trace appears, I would be interested in the profiling information: M-x profiler-start <To the question what should be profiles> cpu < reproduce the bug, wait a bit, press C-g > M-x profiler-report

and send me the trace.

gh-salt commented 4 years ago

Here comes the debug-on-quit trace:

Debugger entered--Lisp error: (quit)

  accept-process-output(nil 0.001)

  lsp-request("textDocument/rangeFormatting" (:textDocument (:uri "file:///home/<my_home>/<path_to_thy_file>...") :options (:tabSize 2 :insertSpaces t) :range (:start (:line 781 :character 6) :end (:line 781 :character 82))))

  lsp-format-region(48781 48857)

  indent-region(48781 48857 nil)

  (if (<= (- end beg) spacemacs-yank-indent-threshold) (indent-region beg end nil))

  spacemacs/yank-advised-indent-function(48781 48857)

  (let ((transient-mark-mode nil) (save-undo buffer-undo-list)) (spacemacs/yank-advised-indent-function (region-beginning) (region-end)))

  (progn (let ((transient-mark-mode nil) (save-undo buffer-undo-list)) (spacemacs/yank-advised-indent-function (region-beginning) (region-end))))

  (if (and enable (not (equal '(4) prefix))) (progn (let ((transient-mark-mode nil) (save-undo buffer-undo-list)) (spacemacs/yank-advised-indent-function (region-beginning) (region-end)))))

  (prog1 (apply yank-func args) (if (and enable (not (equal '(4) prefix))) (progn (let ((transient-mark-mode nil) (save-undo buffer-undo-list)) (spacemacs/yank-advised-indent-function (region-beginning) (region-end))))))

  (let ((prefix (car args)) (enable (and (not (member major-mode spacemacs-indent-sensitive-modes)) (or (derived-mode-p 'prog-mode) (member major-mode spacemacs-yank-indent-modes))))) (if (and enable (equal '(4) prefix)) (progn (setq args (cdr args)))) (prog1 (apply yank-func args) (if (and enable (not (equal '(4) prefix))) (progn (let ((transient-mark-mode nil) (save-undo buffer-undo-list)) (spacemacs/yank-advised-indent-function (region-beginning) (region-end)))))))

  (prog1 (let ((prefix (car args)) (enable (and (not (member major-mode spacemacs-indent-sensitive-modes)) (or (derived-mode-p 'prog-mode) (member major-mode spacemacs-yank-indent-modes))))) (if (and enable (equal '(4) prefix)) (progn (setq args (cdr args)))) (prog1 (apply yank-func args) (if (and enable (not (equal '... prefix))) (progn (let ((transient-mark-mode nil) (save-undo buffer-undo-list)) (spacemacs/yank-advised-indent-function (region-beginning) (region-end))))))) (evil-end-undo-step))

  spacemacs//yank-indent-region(#f(compiled-function (count &optional register yank-handler) "Pastes the latest yanked text behind point.\nThe return value is the yanked text." (interactive #f(compiled-function () #<bytecode 0x1581c390e991>)) #<bytecode 0x1581c3f41a2d>) 1 nil)
  apply(spacemacs//yank-indent-region #f(compiled-function (count &optional register yank-handler) "Pastes the latest yanked text behind point.\nThe return value is the yanked text." 

(interactive #f(compiled-function () #<bytecode 0x1581c3da79d1>)) #<bytecode 0x1581c3f41a2d>) (1 nil))

  evil-paste-after(1 nil)

  funcall-interactively(evil-paste-after 1 nil)

  call-interactively(evil-paste-after nil nil)

  command-execute(evil-paste-after)
m-fleury commented 4 years ago

This is weird. As far as I remember, the request "textDocument/rangeFormatting" is not supported by isabelle-lsp. I have no idea where this is coming from (and why I cannot reproduce is).

I even get a warning when I try to call the function by hand. helm-M-x-execute-command: The connected server(s) does not support method textDocument/rangeFormatting To find out what capabilities support your server use ‘M-x lsp-describe-session’ and expand the capabilities section.

I will investigate that (but not now).

gh-salt commented 4 years ago

No problem. Now that I know how to kill the loop without restarting emacs, I can still work despite this.

Thanks for taking the time to get to this point!

m-fleury commented 4 years ago

Okay, I still have no idea what happened, so I have done the only thing I can do: mark the formatting as non-supported explicitly.

In case you still have the bug with the fix, I would be interested in the content of "Capabilities" on the output of lsp-describe-session, both right after startup and after the bug is triggered. It should look like:

    -[-] Capabilities
       |-[X] documentSymbolProvider: t
       |-[X] textDocumentSync: 2
       |-[X] documentHighlightProvider: t
       |-[-] completionProvider:
       |  |-[X] triggerCharacters: []
       |  `-[X] resolveProvider: nil
       |-[X] hoverProvider: t
       |-[X] definitionProvider: t
       -[X] rangeFormatter: nil
gh-salt commented 4 years ago

The bug still happens.

Here is the status after startup:

    `-[-] Capabilities
       |-[X] documentSymbolProvider: t
       |-[X] textDocumentSync: 2
       |-[X] documentHighlightProvider: t
       |-[-] completionProvider:
       |  |-[X] triggerCharacters: []
       |  `-[X] resolveProvider: nil
       |-[X] hoverProvider: t
       |-[X] definitionProvider: t
       `-[X] rangeFormatter: nil

and here is the status after the bug has happened (several times) (spoiler: they are identical ^^ ) :

    `-[-] Capabilities
       |-[X] documentSymbolProvider: t
       |-[X] textDocumentSync: 2
       |-[X] documentHighlightProvider: t
       |-[-] completionProvider:
       |  |-[X] triggerCharacters: []
       |  `-[X] resolveProvider: nil
       |-[X] hoverProvider: t
       |-[X] definitionProvider: t
       `-[X] rangeFormatter: nil
m-fleury commented 4 years ago
  1. select a region and call M-x: lsp-format-region (IIRC: ",=r"). -> Expected behaviour: an informative error message that the server does not support that.
  2. Which spacemacs version are you using (commit-id please)? (Current guess is bad interaction in some spacemacs version with some emacs-lsp version)
  3. What is the value of M-: indent-region-function
  4. C-h m (or M-x describe-mode) and the content of "Enabled minor modes:" (just the list of minor modes, not the documentation after it).
gh-salt commented 4 years ago
  1. This also triggers the loop, I can't get a message, I have to kill it using C-g
  2. The following commit of the devel branch: f578e618a570d91f9312a2c7c65711a5211f40de (I pulled this morning)
  3. lsp-format-region
  4. Enabled minor modes: Anzu Auto-Composition Auto-Compression Auto-Encryption
    Clean-Aindent Column-Number Company Editorconfig Eldoc Electric-Indent Evil
    Evil-Escape Evil-Local Evil-Surround Eyebrowse File-Name-Shadow Flycheck
    Flycheck-Pos-Tip Font-Lock Global-Anzu Global-Auto-Revert Global-Eldoc
    Global-Evil-Surround Global-Font-Lock Global-Hl-Line Global-Hl-Todo
    Global-Page-Break-Lines Global-Spacemacs-Leader-Override Global-Undo-Tree
    Global-Vi-Tilde-Fringe Helm Helm--Remap-Mouse Helm-Descbinds Helm-Flx Hl-Todo
    Ido-Vertical Line-Number Lsp Lsp-Managed Lsp-Ui Lsp-Ui-Doc Lsp-Ui-Sideline
    Mouse-Wheel Override-Global Persp Projectile Pupo Purpose Recentf Save-Place
    Savehist Shell-Dirtrack Show-Smartparens Show-Smartparens-Global Spaceline-Helm
    Spaceline-Info Spacemacs-Leader-Override Transient-Mark Undo-Tree Unicode-Tokens
    Vi-Tilde-Fringe Which-Key Winner Winum Xterm-Mouse Yas Yas-Global
m-fleury commented 4 years ago

When you have updated spacemacs, have you also updated the plugins?

gh-salt commented 4 years ago

I have updated the packages, the bug has not reoccurred since then. I will work some more like this and see if it comes back

m-fleury commented 4 years ago

I will close this issue. Feel free to reopen it if the bug reoccurs.