## Stream: lean4

### Topic: emacs

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

#### Sebastian Ullrich (Jan 05 2021 at 15:20):

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

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


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

#### Adam Topaz (Jan 05 2021 at 17:43):

Yeah that's a good workaround.

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

#### Sebastian Ullrich (Jan 05 2021 at 20:43):

Are you using the Nix setup?

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

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

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

#### Simon Hudon (Jan 05 2021 at 20:56):

Do refer to setting lean4-rootdir manually?

#### Sebastian Ullrich (Jan 05 2021 at 20:56):

Yes, whatever you did to set it up

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

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

#### Simon Hudon (Jan 06 2021 at 02:21):

That's understandable

#### Simon Hudon (Jan 06 2021 at 02:27):

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

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

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

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

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

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

#### Simon Hudon (Jan 08 2021 at 16:29):

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

#### Adam Topaz (Jan 08 2021 at 16:30):

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

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

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

#### Adam Topaz (Jan 08 2021 at 16:37):

I'll take a look at direnv. Thanks!

#### Sebastian Ullrich (Jan 08 2021 at 16:37):

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

#### Adam Topaz (Jan 08 2021 at 16:37):

Does this not create a whole new installation of emacs?

#### Sebastian Ullrich (Jan 08 2021 at 16:39):

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

Oh ok.

"a bit" ~= 1G

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

#### Sebastian Ullrich (Jan 08 2021 at 16:46):

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.

#### Adam Topaz (Jan 08 2021 at 16:49):

Hmm... what's the actual command?

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

#### Adam Topaz (Jan 08 2021 at 16:54):

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

#### Adam Topaz (Jan 08 2021 at 16:54):

Yes, this works

Last updated: May 07 2021 at 13:21 UTC