Zulip Chat Archive

Stream: general

Topic: Try this: (spac)emacs


view this post on Zulip Johan Commelin (Jan 26 2021 at 15:36):

Is there an easy way to get a key combo in (spac)emacs that will replace tidy? or squeeze_simp or library_search by the output of Try this:?

view this post on Zulip Jesse Michael Han (Jan 26 2021 at 15:45):

my hack is to just record an ad-hoc keyboard macro

view this post on Zulip Johan Commelin (Jan 26 2021 at 15:53):

It would be nice to push something to the spacemacs layer for lean. But I've only been using spacemacs for ~6 days... so I'm not really an expert yet.

view this post on Zulip Jesse Michael Han (Jan 26 2021 at 16:16):

pinging our guru @Simon Hudon, who has definitely thought about this at some point

view this post on Zulip Adam Topaz (Jan 26 2021 at 16:27):

@Johan Commelin Are you moving over to the dark side?

view this post on Zulip Simon Hudon (Jan 26 2021 at 16:29):

I have a script that does that in my init file. I can move it to the lean-mode community contributions.

view this post on Zulip Johan Commelin (Jan 26 2021 at 16:58):

Other things I need to figure out: currently I need to leave insert mode and push 3 buttons to get an autocomplete popup. I would like to just have it show up automatically and filter results as I type. Like in VScode

view this post on Zulip Sebastian Ullrich (Jan 26 2021 at 17:05):

That definitely worked for me in Lean 3 without leaving insert mode using

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

view this post on Zulip Adam Topaz (Jan 26 2021 at 17:09):

Johan Commelin said:

Other things I need to figure out: currently I need to leave insert mode and push 3 buttons to get an autocomplete popup. I would like to just have it show up automatically and filter results as I type. Like in VScode

@Johan Commelin I was using vanilla emacs with company-complete, etc. for a while. I recently switched to doom-emacs and my life has been much easier. I've never seriously used spacemacs, but as far as I understand, doom-emacs is more minimal than spacemacs, hence much faster in many respects.

view this post on Zulip Adam Topaz (Jan 26 2021 at 17:09):

In particular the automatic lean setup in doom emacs has an automatic popup that you're looking for.

view this post on Zulip Adam Topaz (Jan 26 2021 at 17:11):

I guess I can dig a bit and try to find what package doom emacs uses for this, but if you don't actually care about spacemacs you might want to check out doom emacs as well.

view this post on Zulip Adam Topaz (Jan 26 2021 at 17:16):

Hmmm... looks like it's company lean with some nonstandard configuration. See e.g.
https://github.com/hlissner/doom-emacs/blob/develop/modules/lang/lean/config.el
https://github.com/hlissner/doom-emacs/blob/develop/modules/completion/company/config.el

view this post on Zulip Johan Commelin (Jan 26 2021 at 18:28):

Thanks, I'll try to look into this asap

view this post on Zulip Johan Commelin (Jan 26 2021 at 18:28):

Is doom emacs also vim-like? I kind of like spacemacs so far.

view this post on Zulip Adam Topaz (Jan 26 2021 at 18:38):

Yes, the default in doom emacs is evil-mode

view this post on Zulip Adam Topaz (Jan 26 2021 at 18:38):

As it should be.

view this post on Zulip Kyle Miller (Jan 26 2021 at 20:08):

I just hacked together something for the Lean Next Error window that turns "Try this:" into a link that you can click/press enter on to copy the suggestion into the buffer. (Disclaimer: very lightly tested.)

This replaces a function in lean-flycheck.el and gives a couple extra definitions:

(define-button-type 'lean-suggestion-button
  'follow-link t
  'action 'lean-copy-try-this
  'help-echo "mouse-1: copy suggestion into buffer")

(defun lean-copy-try-this (event)
  (interactive "e")
  (let ((window (posn-window (event-end event)))
        (pos (posn-point (event-end event))))
    (with-current-buffer (window-buffer window)
      (let ((sugg (or (get-pos-property pos 'lean-suggestion)
                      ; don't understand why this is needed:
                      (get-pos-property (1+ pos) 'lean-suggestion))))
        (let ((buff (get-file-buffer (alist-get 'filename sugg))))
          (when buff
            (message (buffer-name buff))
            (with-current-buffer buff
              (goto-char (alist-get 'pos sugg))
              (princ (alist-get 'suggest sugg) buff)
              (insert ","))))))))

(defun lean-next-error--handler ()
  (when (lean-info-buffer-active lean-next-error-buffer-name)
    (let ((deactivate-mark) ; keep transient mark
          (errors (or
                   ;; prefer error of current position, if any
                   (flycheck-overlay-errors-at (point))
                   ;; try errors in current line next
                   (sort (flycheck-overlay-errors-in (line-beginning-position) (line-end-position))
                         #'flycheck-error-<)
                   ;; fall back to next error position
                   (-if-let* ((pos (flycheck-next-error-pos 1)))
                       (flycheck-overlay-errors-at pos)))))
      (lean-with-info-output-to-buffer lean-next-error-buffer-name
       (dolist (e errors)
         (princ (format "%d:%d: " (flycheck-error-line e) (flycheck-error-column e)))
         (let ((i (point)))
           (princ (flycheck-error-message e))
           (when (string-prefix-p "Try this:" (flycheck-error-message e))
             (make-button i (+ i (length "Try this:"))
                          :type 'lean-suggestion-button
                          'lean-suggestion
                          (list (cons 'filename (flycheck-error-filename e))
                                (cons 'pos (flycheck-error-pos e))
                                (cons 'suggest
                                      (string-trim
                                       (substring (flycheck-error-message e)
                                                  (length "Try this: "))))))))
         (princ "\n\n"))
       (when flycheck-current-errors
         (princ (format "(%d more messages above...)" (length flycheck-current-errors))))))))

view this post on Zulip Kyle Miller (Jan 26 2021 at 20:09):

Adam Topaz said:

As it should be.

Are you using a constructive modal logic here? :wink:

view this post on Zulip Kyle Miller (Jan 26 2021 at 20:21):

The code just inserts the suggestion (with comma) right before the tactic that generated the suggestion, and it doesn't try to remove that tactic -- I wasn't sure of a reliable way to do this.

view this post on Zulip Johan Commelin (Jan 26 2021 at 20:35):

Ooh, another problem with spacemacs is that I have no idea where I should paste such blobs of code into my config file...

view this post on Zulip Johan Commelin (Jan 26 2021 at 20:36):

Same for the 1-liner that Sebastian share upstairs...

view this post on Zulip Johan Commelin (Jan 26 2021 at 20:36):

But once Kyle's code is tested ϵ\epsilon more, I wouldn't mind if such stuff were added to the default lean packages

view this post on Zulip Kyle Miller (Jan 26 2021 at 20:41):

You can test things out by creating a new .el file anywhere and then C-x C-e at the ends of expressions to evaluate them (or C-M-x to evaluate a whole defun when your cursor is somewhere within it).

view this post on Zulip Kyle Miller (Jan 26 2021 at 20:45):

But for the config file, I think this suggestion code would just need to be after (require 'lean-mode) and (require 'flycheck), but I'm not completely sure. Sebastian's code probably can go anywhere.

view this post on Zulip Adam Topaz (Jan 26 2021 at 20:59):

@Johan Commelin
I don't really know how spacemacs configs work. In doom-emacs, I put configuration for packages in a (use-package foo ...) declaration similar to the examples in the readme here: https://github.com/jwiegley/use-package
(This all takes place in a config.el file in a specific folder)

This might be how spacemacs does things too... not sure.

view this post on Zulip Julian Berman (Jan 27 2021 at 00:49):

Kyle Miller said:

The code just inserts the suggestion (with comma) right before the tactic that generated the suggestion, and it doesn't try to remove that tactic -- I wasn't sure of a reliable way to do this.

I just implemented my own hacky version of this a few weeks ago and what I did was just go with delete the word under the cursor and nothing fancier

view this post on Zulip Julian Berman (Jan 27 2021 at 00:49):

The vscode implementation has some slightly lengthy heuristic it uses

view this post on Zulip Kyle Miller (Jan 27 2021 at 01:17):

I considered that, but I frequently do squeeze_simp [foo1, foo2] and it wouldn't be good to have it automatically introduce a syntax error

view this post on Zulip Jannis Limperg (Jan 27 2021 at 17:07):

@Johan Commelin Configuration usually goes into your .spacemacs, specifically into the body of the function dotspacemacs/user-config there. This function is executed after Spacemacs has done its thing and loaded everything it wants to load.

view this post on Zulip Johan Commelin (Jan 29 2021 at 08:41):

@Kyle Miller would you mind pushing your functions to the lean mode repo?

view this post on Zulip Johan Commelin (Jan 29 2021 at 08:41):

Adam Topaz said:

Hmmm... looks like it's company lean with some nonstandard configuration. See e.g.
https://github.com/hlissner/doom-emacs/blob/develop/modules/lang/lean/config.el
https://github.com/hlissner/doom-emacs/blob/develop/modules/completion/company/config.el

Also, whoever effectively maintains the spacemaces layer... :up: seems like cool-to-have.

view this post on Zulip Johan Commelin (Jan 29 2021 at 09:02):

(defun dotspacemacs/user-config ()
  "Configuration for user code:
This function is called at the very end of Spacemacs startup, after layer
configuration.
Put your configuration code here, except for variables that should be set
before packages are loaded."
  ;; make treemacs hide .gitignore files
  (with-eval-after-load 'treemacs
    (add-to-list 'treemacs-pre-file-insert-predicates #'treemacs-is-file-git-ignored?)
    )
  ;; easy access to completion
  (global-set-key (kbd "C-return") #'company-complete)
  )

The treemacs blob has the intended effect, but <C-return> is undefined

view this post on Zulip Kyle Miller (Jan 29 2021 at 10:25):

Johan Commelin said:

Kyle Miller would you mind pushing your functions to the lean mode repo?

I'll make a PR sometime soon, but in the meantime here's my branch: https://github.com/kmill/lean-mode/tree/try-this


Last updated: May 08 2021 at 19:11 UTC