lean4-mode with nix-doom-emacs

Stream: lean4

[ohhaimark]

I'm using NixOS with flakes, a NixOS home-manager module, and nix-doom-emacs via the home-manager module.
I have the following in my home-manager setup:

programs.doom-emacs = {
  enable = true;
  doomPrivateDir = ../doom;
  emacsPackage = pkgs.emacs;
  emacsPackagesOverlay = eself: esuper:
    {
      lean4-mode = eself.trivialBuild rec {
        pname = "lean4-mode";
        version = "v4.0.0-m2";
        src = pkgs.fetchFromGitHub {
          owner = "leanprover";
          repo = "lean4";
          rev = version;
        };
        sourceRoot = "source/lean4-mode";
      };
    };
};

and in my .doom.d/packages.el

(package! lean4-mode)

and (require 'lean4-mode) fails

My NixOS build succeeds, but doesn't create a lean4-mode package that I can find in the store. The NixOS build fails if I don't include the overlay.

[ohhaimark]

What can I do?

[Sebastian Ullrich]

I use doom-emacs with lean4-mode, but the boring way unfortunately

(package! lean4-mode :recipe
  (:local-repo "~/lean/lean"
   :files ("lean4-mode/*.el")
   :build (:not compile)))

[Adam Topaz]

Did something happen with lean4-mode recently? I used to use

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

and it worked just fine for a while, but now lean4-mode is not found at all (after running doom upgrade)

[Adam Topaz]

Ah I see, lean4-mode has been moved to its own repo in github.com/leanprover/lean4-mode. The following seems to work for me:

(package! lean4-mode :recipe
  (:host github
   :repo "leanprover/lean4-mode"))

Is this reasonable, or does anyone have any other recommended configuration options?

[Sebastian Ullrich]

Looks pretty much equivalent to the use-package call in the readme. Feel free to add as Doom instructions.

[Adam Topaz]

https://github.com/leanprover/lean4-mode/pull/2

[Eric Meinhardt]

Should the instructions (for nix-doom-emacs) that are currently in the README still work?

[Eric Meinhardt]

Adam Topaz said:

https://github.com/leanprover/lean4-mode/pull/2

@Adam Topaz, would you mind elaborating about how you've packaged lean4-mode and made it legible to doom-emacs? The instructions you added leave a lot to the imagination.

[Adam Topaz]

I think if you add

(package! lean4-mode :recipe
  (:host github
   :repo "leanprover/lean4-mode"))

to your packages.el (and call doom sync, etc. as usual), it should work.

[Adam Topaz]

There's nothing packaged, this gets the code for the package directly from github. Is lean4-mode on melpa yet?

[Eric Meinhardt]

Adam Topaz said:

I think if you add

(package! lean4-mode :recipe
  (:host github
   :repo "leanprover/lean4-mode"))

to your packages.el (and call doom sync, etc. as usual), it should work.

Here's what I get when rebuilding my nixos config (including doom-emacs managed via home-manager/nix-doom-emacs):

> sudo -i nixos-rebuild build
building Nix...
building the system configuration...
building '/nix/store/vnll0mqgll34qp901qih5df5ixczcd8l-emacs-straight-packages.json.drv'...
installing
[nix-doom-emacs] Advising doom to keep it alive...
Loading /nix/store/myqh2sqs9v4nxp9pv462azx4y2vmabik-doom-src/bin/doom...
Installing Doom Emacs!

- Skipping /nix/store/ghy9rm08wk51vwky698xzdgi6vlyvhyj-doom.d/ (already exists)
  - Skipping init.el (already exists)
  - Skipping config.el (already exists)
  - Skipping packages.el (already exists)
Installing plugins
> Installing packages...
  - No packages need to be installed
Regenerating autoloads files
Deploying commit-msg and pre-push git hooks
  - Loaded "/nix/store/myqh2sqs9v4nxp9pv462azx4y2vmabik-doom-src/ci.el"
  ! Cannot locate a git repo in ./
✓  Finished! Doom is ready to go!

But before you doom yourself, here are some things you should know:

1. Don't forget to run 'doom sync', then restart Emacs, after modifying
   ~/.doom.d/init.el or ~/.doom.d/packages.el.

   This command ensures needed packages are installed, orphaned packages are
   removed, and your autoloads/cache files are up to date. When in doubt, run
   'doom sync'!

2. If something goes wrong, run `doom doctor`. It diagnoses common issues with
   your environment and setup, and may offer clues about what is wrong.

3. Use 'doom upgrade' to update Doom. Doing it any other way will require
   additional steps. Run 'doom help upgrade' to understand those extra steps.

4. Access Doom's documentation from within Emacs via 'SPC h d h' or 'C-h d h'
   (or 'M-x doom/help')

Have fun!

Error in kill-emacs-hook (straight--transaction-finalize): (file-missing "Opening output file" "No such file or directory" "/build/tmp.En4Aaxq3n9/local/straight/build-28.1-cache.el")
error: evaluation aborted with the following error message: 'Package not available: lean4-mode'
(use '--show-trace' to show detailed location information)

lean4-mode is not on melpa yet.

[Adam Topaz]

I'm very far from being a nix expert. Hopefully someone else can help.

[Eric Meinhardt]

Adam Topaz said:

I'm very far from being a nix expert. Hopefully someone else can help.

If you have a currently working nix-doom-emacs config you can share, that would definitely help.

[Adam Topaz]

I personally don't use nix.

[Mauricio Collares]

I use Nix, but not nix-doom-emacs. Is there somewhere you can put this in your Nix config? I use emacs-overlay and put it in extraEmacsPackages. I see nix-doom-emacs has an extraPackagesOverlay attribute, so perhaps you can do something like

emacsPackagesOverlay = self: super: {
  lean4-mode = self.melpaBuild rec {
    pname = "lean4-mode";
    version = "1";
    commit = "37d5c99b7b29c80ab78321edd6773200deb0bca6";
    src = self.fetchFromGitHub {
      owner = "leanprover";
      repo = "lean4-mode";
      rev = commit;
      sha256 = "sha256-+dRaXB7uvN/weSZiKcfSKWhcdJVNg9Vg8k0pJkDNjpc=";
    };
    packageRequires = with self.melpaPackages;
      [ dash f flycheck magit-section lsp-mode s ];
    recipe = self.writeText "recipe" ''
               (lean4-mode :repo "leanprover/lean4-mode" :fetcher github)
             '';
  });
};

[Mauricio Collares]

(deleted)

[Eric Meinhardt]

Mauricio Collares said:

I use Nix, but not nix-doom-emacs. Is there somewhere you can put this in your Nix config? I use emacs-overlay and put it in extraEmacsPackages. I see nix-doom-emacs has an extraPackagesOverlay attribute, so perhaps you can do something like

emacsPackagesOverlay = self: super: {
  lean4-mode = self.melpaBuild rec {
    pname = "lean4-mode";
    version = "1";
    commit = "37d5c99b7b29c80ab78321edd6773200deb0bca6";
    src = self.fetchFromGitHub {
      owner = "leanprover";
      repo = "lean4-mode";
      rev = commit;
      sha256 = "sha256-+dRaXB7uvN/weSZiKcfSKWhcdJVNg9Vg8k0pJkDNjpc=";
    };
    packageRequires = with self.melpaPackages;
      [ dash f flycheck magit-section lsp-mode s ];
    recipe = self.writeText "recipe" ''
               (lean4-mode :repo "leanprover/lean4-mode" :fetcher github)
             '';
  });
};

Yes! With very slight adaptation (self.fetchFromGitHub -> pkgs.fetchFromGitHub and self.writeText -> pkgs.writeText) for my non-flake and home-manager-based config this looks like it works. Working on a PR for lean4-mode now. Thanks!