## Stream: general

### Topic: Try this: (spac)emacs

#### 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:?

#### Jesse Michael Han (Jan 26 2021 at 15:45):

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

#### 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.

#### Jesse Michael Han (Jan 26 2021 at 16:16):

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

#### Adam Topaz (Jan 26 2021 at 16:27):

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

#### 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.

#### 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

#### 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)


#### 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.

#### 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.

#### 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.

#### 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

#### Johan Commelin (Jan 26 2021 at 18:28):

Thanks, I'll try to look into this asap

#### Johan Commelin (Jan 26 2021 at 18:28):

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

#### Adam Topaz (Jan 26 2021 at 18:38):

Yes, the default in doom emacs is evil-mode

As it should be.

#### 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
'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))))))))


#### Kyle Miller (Jan 26 2021 at 20:09):

As it should be.

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

#### 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.

#### 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...

#### Johan Commelin (Jan 26 2021 at 20:36):

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

#### 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

#### 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).

#### 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.

#### 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.

#### 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

#### Julian Berman (Jan 27 2021 at 00:49):

The vscode implementation has some slightly lengthy heuristic it uses

#### 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

#### 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.

#### Johan Commelin (Jan 29 2021 at 08:41):

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

#### Johan Commelin (Jan 29 2021 at 08:41):

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.

#### 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
)
(global-set-key (kbd "C-return") #'company-complete)
)


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

#### 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