Zulip Chat Archive

Stream: lean4

Topic: emacs


view this post on Zulip Adam Topaz (Jan 05 2021 at 15:18):

Just for future reference, here's the link to the emacs lean4 package
https://github.com/leanprover/lean4/tree/master/lean4-mode

Will this be on melpa at some point soon?

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 15:20):

Probably, when it (and the language server) is more stable

view this post on Zulip Adam Topaz (Jan 05 2021 at 16:53):

Just in case it helps anyone else, the following code in packages.el seems to work for doom emacs

(package! dash)
(package! flycheck)
(package! dash-functional)
(package! f)
(package! s)
(package! lsp-mode)

(package! lean4-mode :recipe
  (:host github
   :repo "leanprover/lean4"
   :files ("lean4-mode/*.el")))

view this post on Zulip Koundinya Vajjha (Jan 05 2021 at 17:32):

@Adam Topaz thank you!

view this post on Zulip Adam Topaz (Jan 05 2021 at 17:34):

Looks like (require 'lean4-mode) is problematic if you have both lean4-mode and lean-mode installed. And without it you have to manually activate lean4-mode with e.g. M-x. Is there a way to have it automatically activate lean4-mode in a lean4 project?

view this post on Zulip Kevin Lacker (Jan 05 2021 at 17:42):

maybe https://www.gnu.org/software/emacs/manual/html_node/emacs/Directory-Variables.html

view this post on Zulip Adam Topaz (Jan 05 2021 at 17:43):

Yeah that's a good workaround.

view this post on Zulip Simon Hudon (Jan 05 2021 at 20:41):

I just (re)installed lean4-mode (I had a version from before it was based on LSP). I have a weird situation where I'm having status: starting for a very long time

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 20:43):

Are you using the Nix setup?

view this post on Zulip Simon Hudon (Jan 05 2021 at 20:47):

To install Lean4 yes but not to install the emacs mode. Does the nix setup help also with emacs?

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 20:50):

There is preliminary integration of the Nix-based build system into editors started as above, which automatically builds dependencies when opening or invalidating a file. There is no progress report yet, and build errors from dependencies will crash the language server; see the stderr logs for the build error in that case.

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 20:51):

The language server starting for a long time can mean Nix compiling dependencies in the background, but that shouldn't happen if you pointed lean4-mode manually at the result of nix build.

view this post on Zulip Simon Hudon (Jan 05 2021 at 20:56):

Do refer to setting lean4-rootdir manually?

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 20:56):

Yes, whatever you did to set it up

view this post on Zulip Simon Hudon (Jan 05 2021 at 20:59):

Ok thanks! I'll need to get back to it a bit later. I'll let you know how it goes

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 21:04):

Btw, given my part of the talk yesterday I probably don't have to mention that I will have only limited patience dealing with manual setups not using Nix (completely) from now on :grinning_face_with_smiling_eyes:

view this post on Zulip Simon Hudon (Jan 06 2021 at 02:21):

That's understandable

view this post on Zulip Simon Hudon (Jan 06 2021 at 02:27):

For emacs, what is the nix way of doing things?

view this post on Zulip Simon Hudon (Jan 06 2021 at 02:33):

I really like what you did with the documentation btw. I especially like the button that copies code snippets. For shell code, it also copies $ however

view this post on Zulip Simon Hudon (Jan 06 2021 at 03:00):

I just saw the following line in the instructions:

nix run .#emacs-dev MyPackage.lean  # arguments can be passed as well, e.g. the file to open

Is this what you refer to as the nix emacs setup? It kind of looks like I'd need a different instance of emacs for each project. That's not very practical

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

@Simon Hudon did you ever get emacs to behave with nix? If so, could you give some hints on how you set it up?

view this post on Zulip Sebastian Ullrich (Jan 08 2021 at 16:19):

Simon Hudon said:

It kind of looks like I'd need a different instance of emacs for each project. That's not very practical

FWIW, I use a separate instance per workspace, so that's not really an issue for me. But if you don't want that, the nix-env-selector solution mentioned in the "using nix" topic sounds like the next-best thing.

view this post on Zulip Simon Hudon (Jan 08 2021 at 16:28):

@Sebastian Ullrich I see. I kind of use emacs as an operating system where I do a whole bunch of stuff until I'm forced to interact with OSX again

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

@Adam Topaz Sorry I haven't made progress yet. I'm going to try again tonight

view this post on Zulip Adam Topaz (Jan 08 2021 at 16:30):

nix-env-selector is a vs-code thing right?

view this post on Zulip Sebastian Ullrich (Jan 08 2021 at 16:33):

Whoops, yeah. I use direnv in Emacs (for things that are not Lean), though that needs one more setup step per project...

view this post on Zulip Adam Topaz (Jan 08 2021 at 16:36):

Isn't there a way to make this nix build .#lean-dev -o ./lean-dev step happen automatically when opening the nix-shell using a shell.nix file? I think it's also possible to ask nix-shell to set up a link + update the path variable so that lean is symlinked to ./lean-dev. I guess what I'm going for is to have it automatically set up the links + path stuff when I run nix-shell so that emacs is happy when I run emacs from within the nix-shell.

view this post on Zulip Adam Topaz (Jan 08 2021 at 16:37):

I'll take a look at direnv. Thanks!

view this post on Zulip Sebastian Ullrich (Jan 08 2021 at 16:37):

If you're running Emacs from within a nix-shell anyway, why not use .#emacs-dev?

view this post on Zulip Adam Topaz (Jan 08 2021 at 16:37):

Does this not create a whole new installation of emacs?

view this post on Zulip Sebastian Ullrich (Jan 08 2021 at 16:39):

Yes, it does download "a bit" of stuff. But it will use your .emacs.d.

view this post on Zulip Adam Topaz (Jan 08 2021 at 16:40):

Oh ok.

view this post on Zulip Adam Topaz (Jan 08 2021 at 16:43):

"a bit" ~= 1G

view this post on Zulip Reid Barton (Jan 08 2021 at 16:45):

If you wish to build a Lean program from scratch, you must first invent the universe. -- Carl Sagan

view this post on Zulip Sebastian Ullrich (Jan 08 2021 at 16:46):

Adam Topaz said:

Isn't there a way to make this nix build .#lean-dev -o ./lean-dev step happen automatically when opening the nix-shell using a shell.nix file?

If you use nix shell .#lean-dev instead, it will put the correct lean binary in your path, which should be sufficient if you've already installed lean4-mode another way.

view this post on Zulip Adam Topaz (Jan 08 2021 at 16:49):

Hmm... what's the actual command?

view this post on Zulip Adam Topaz (Jan 08 2021 at 16:49):

I've been using nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix to start the nix shell with the custom nix

view this post on Zulip Adam Topaz (Jan 08 2021 at 16:54):

Ah I see. You mean run nix shell .#lean-dev in the nix-shell.

view this post on Zulip Adam Topaz (Jan 08 2021 at 16:54):

Yes, this works


Last updated: May 07 2021 at 13:21 UTC