search

m-fleury / isabelle-emacs

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

Add doom emacs install instructions #54

Closed halbGefressen closed 3 years ago

halbGefressen commented 3 years ago

Hi, I can't figure out how I am going to install this in doom emacs. Is there a way to add a separate installation guide for us doom users?

halbGefressen commented 3 years ago

Nvm, found another issue for it.

m-fleury commented 3 years ago

For documentation purpose: I have posted my config in #45.

halbGefressen commented 3 years ago

I found and tried it, with no success. Emacs cannot find lsp-isar-parse-args, because it doesn't know the location.

What other steps do I have to follow except copying the configuration?

m-fleury commented 3 years ago

In your packages.el, also add:

(package! isar-mode
   :recipe (:local-repo "~/Documents/repos/simp-isar-mode"))

(package! isar-goal-mode
   :recipe (:local-repo "~/Documents/repos/simp-isar-mode"))

(package! lsp-isar
   :recipe (:local-repo "~/Documents/isabelle/isabelle-release/src/Tools/emacs-lsp/lsp-isar/"))

(package! lsp-isar-parse-args
   :recipe (:local-repo "~/Documents/isabelle/isabelle-release/src/Tools/emacs-lsp/lsp-isar/"))

(package! session-async)

(with the correct paths!)

halbGefressen commented 3 years ago

Thank you for your time! Now my packages are loading correctly (I guess), but when I'm opening a .thy file, I have no syntax highlighting, linting whatsoever. I can execute the command isar-mode to bring me highlighting manually, but apart from that, nothing else seems to work. I can open the interfaces, but they do nothing.

Edit: And also, when executing almost any command, I get the error "Symbol's value as variable is void: thing-at-point-provider-alist

Edit2: The Isabelle modes are now opening up and everything shows up like it probably should. But I still get the error above when trying to use any of the C-c commands, like lsp-isar-insert-sledgehammer-and-call

m-fleury commented 3 years ago

what emacs version are you using?

halbGefressen commented 3 years ago

27.2.1

m-fleury commented 3 years ago

Fixed now.

Long version: thing-at-point-provider-alist is new in emacs28... where a performance regression means that I have to 'fix' a core function. And I forgot to add a if (>= emacs-major-version 28) before the code.

halbGefressen commented 3 years ago

Thank you. I'm going to rebuild the package and see if it works. After that, I'll summarize everything and create instructions.

Edit: Yup, works now. :+1: