Try this: (spac)emacs

Stream: general

[Johan Commelin]

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]

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

[Johan Commelin]

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]

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

[Adam Topaz]

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

[Simon Hudon]

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

[Johan Commelin]

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]

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

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

[Adam Topaz]

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]

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

[Adam Topaz]

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]

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]

Thanks, I'll try to look into this asap

[Johan Commelin]

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

[Adam Topaz]

Yes, the default in doom emacs is evil-mode

[Adam Topaz]

As it should be.

[Kyle Miller]

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

[Kyle Miller]

Adam Topaz said:

As it should be.

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

[Kyle Miller]

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]

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]

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

[Johan Commelin]

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]

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]

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]

@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]

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]

The vscode implementation has some slightly lengthy heuristic it uses

[Kyle Miller]

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]

@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]

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

[Johan Commelin]

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.

[Johan Commelin]

(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

[Kyle Miller]

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