`nix-doom-emacs` install instructions

[emeinhardt]

I'm not sure if I've done something wrong or if the installation instructions could be made a little more explicit.

Currently, my environment is:

1. NixOS 22.05 (just upgraded today), in general using the 22.05 channels for NixOS and home-manager.
2. I install doom-emacs from nix-community/nix-doom-emacs and manage it via home-manager.
3. I use the emacs overlay from nix-community/emacs-overlay, plus the overlay fixes suggested in vlaci/nix-doom-emacs/issues/394.
   4. elan is currently globally available, and leanprover/lean4:stable is the default toolchain.

When I add

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

to my packages.el and rebuild my nixos config (including doom-emacs), I get the following error:

building Nix...
building the system configuration...
error: evaluation aborted with the following error message: 'Package not available: lean4-mode'
(use '--show-trace' to show detailed location information)

I also got this error before upgrading to 22.05. I also got this error before installing elan systemwide.

Is there a path I need to set (vaguely comparable to the first set of instructions for installing lean4-mode) to lean4 binaries?

My other guess is that doom-emacs is looking in the wrong place (or an out-of-date place) for available packages, but I don't know why that would be the case. Maybe the package name has been tweaked?

[Kha]

lean4-mode is not packaged as a Nix derivation in Nixpkgs yet, so you need to package it yourself, e.g. as in https://github.com/leanprover/lean4/blob/bfce841985356185235a6cab465cf5976c95817f/nix/packages.nix#L48-L57. If you expect to be able to install arbitrary packages without additional setup, you may not want to use nix-doom-emacs.

[Kha]

This might also be solved by adding lean4-mode to melpa

[emeinhardt]

I've opened a separate issue for adding lean4-mode to melpa.

Would you mind updating the doom-emacs instructions in the readme to at least explicitly indicate whatever you think is appropriate? As it stands, there's nothing at all to suggest that the user needs to package lean4mode themselves.

I'd submit a pull request myself with more information if I had figured out yet how to do that - I'm looking at what emacsPackages.melpaBuild does to figure out how I can recreate that through some combination of my config.el and a nix overlay.

EDIT: I've added a PR that would close this issue.

[xhalo32]

Thank you @emeinhardt for your work and for saving my time!

I would like to note for those managing their home-manager configuration as a flake, that you can avoid the pkgs.fetchFromGitHub ... by specifying it in your flake inputs as follows:

inputs = {
  lean4-mode = {
    url = "github:leanprover/lean4-mode";
    flake = false;
  };
};

and specifying emacsPackagesOverlay in the doom-emacs configuration as follows:

    emacsPackagesOverlay = self: super: {
      lean4-mode = self.melpaBuild rec {
        src = inputs.lean4-mode;
        commit = inputs.lean4-mode.rev;
        version = "1";
        pname = "lean4-mode";
        packageRequires = with self; [ dash f flycheck magit-section lsp-mode s ];
        recipe = pkgs.writeText "recipe" ''
          (lean4-mode :repo "leanprover/lean4-mode" :fetcher github)
        '';
      };
    };

This way lean4-mode is tracked in the flake.lock and nix flake update updates lean4-mode as well.