Add support for the Lean language

plugins/default.nix

@@ -43,6 +43,7 @@
 
     ./languages/clangd-extensions.nix
     ./languages/julia/julia-cell.nix
+    ./languages/lean.nix
     ./languages/ledger.nix
     ./languages/markdown-preview.nix
     ./languages/nix.nix

plugins/languages/lean.nix

@@ -0,0 +1,316 @@
+{
+  lib,
+  helpers,
+  config,
+  pkgs,
+  ...
+}:
+with lib; let
+  cfg = config.plugins.lean;
+in {
+  options.plugins.lean =
+    helpers.extraOptionsOptions
+    // {
+      enable = mkEnableOption "lean-nvim";
+
+      package = helpers.mkPackageOption "lean-nvim" pkgs.vimPlugins.lean-nvim;
+
+      leanPackage = mkOption {
+        type = with types; nullOr package;
+        default = pkgs.lean4;
+        description = "Which package to use for lean.";
+        example = null;
+      };
+
+      lsp =
+        helpers.defaultNullOpts.mkNullable
+        (
+          with types;
+            submodule {
+              freeformType = types.attrs;
+              options = {
+                enable = helpers.defaultNullOpts.mkBool true ''
+                  Whether to enable the Lean language server(s) ?
+
+                  Set to `false` to disable, otherwise should be a table of options to pass to
+                  `leanls`.
+                  See https://github.com/neovim/nvim-lspconfig/blob/master/doc/server_configurations.md#leanls
+                  for details.
+                '';
+
+                on_attach = helpers.mkNullOrOption types.str ''
+                  The LSP handler.
+                '';
+
+                init_options = helpers.mkNullOrOption (with types; attrsOf anything) ''
+                  The options to configure the lean language server.
+                  See `Lean.Lsp.InitializationOptions` for details.
+                '';
+              };
+            }
+        )
+        "{}"
+        "LSP settings.";
+
+      ft = {
+        default = helpers.defaultNullOpts.mkStr "lean" ''
+          The default filetype for Lean files.
+        '';
+
+        nomodifiable = helpers.mkNullOrOption (with types; listOf str) ''
+          A list of patterns which will be used to protect any matching Lean file paths from being
+          accidentally modified (by marking the buffer as `nomodifiable`).
+
+          By default, this list includes the Lean standard libraries, as well as files within
+          dependency directories (e.g. `_target`)
+          Set this to an empty table to disable.
+        '';
+      };
+
+      abbreviations = {
+        enable = helpers.defaultNullOpts.mkBool true ''
+          Whether to enable expanding of unicode abbreviations.
+        '';
+
+        extra = helpers.defaultNullOpts.mkNullable (with types; attrsOf str) "{}" ''
+          Additional abbreviations.
+
+          Example:
+          ```
+            {
+              # Add a \wknight abbreviation to insert ♘
+              #
+              # Note that the backslash is implied, and that you of
+              # course may also use a snippet engine directly to do
+              # this if so desired.
+              wknight = "♘";
+            }
+        '';
+
+        leader = helpers.defaultNullOpts.mkStr "\\" ''
+          Change if you don't like the backslash.
+          (comma is a popular choice on French keyboards)
+        '';
+      };
+
+      mappings = helpers.defaultNullOpts.mkBool false ''
+        Whether to enable suggested mappings.
+      '';
+
+      infoview = {
+        autoopen = helpers.defaultNullOpts.mkBool true ''
+          Automatically open an infoview on entering a Lean buffer?
+          Should be a function that will be called anytime a new Lean file is opened.
+          Return true to open an infoview, otherwise false.
+          Setting this to `true` is the same as `function() return true end`, i.e. autoopen for any
+          Lean file, or setting it to `false` is the same as `function() return false end`,
+          i.e. never autoopen.
+        '';
+
+        autopause = helpers.defaultNullOpts.mkBool false "";
+
+        width = helpers.defaultNullOpts.mkPositiveInt 50 ''
+          Set infoview windows' starting width.
+          Windows are opened horizontally or vertically depending on spacing.
+        '';
+
+        height = helpers.defaultNullOpts.mkPositiveInt 20 ''
+          Set infoview windows' starting height.
+          Windows are opened horizontally or vertically depending on spacing.
+        '';
+
+        horizontalPosition = helpers.defaultNullOpts.mkEnum ["top" "bottom"] "bottom" ''
+          Put the infoview on the top or bottom when horizontal.
+        '';
+
+        separateTab = helpers.defaultNullOpts.mkBool false ''
+          Always open the infoview window in a separate tabpage.
+          Might be useful if you are using a screen reader and don't want too many dynamic updates
+          in the terminal at the same time.
+          Note that `height` and `width` will be ignored in this case.
+        '';
+
+        indicators = helpers.defaultNullOpts.mkEnum ["always" "never" "auto"] "auto" ''
+          Show indicators for pin locations when entering an infoview window.
+          `"auto"` = only when there are multiple pins.
+        '';
+
+        lean3 = {
+          showFilter = helpers.defaultNullOpts.mkBool true "";
+
+          mouseEvents = helpers.defaultNullOpts.mkBool false ''
+            Setting this to `true` will simulate mouse events in the Lean 3 infoview, this is buggy
+            at the moment so you can use the I/i keybindings to manually trigger these.
+          '';
+        };
+
+        showProcessing = helpers.defaultNullOpts.mkBool true "";
+
+        showNoInfoMessage = helpers.defaultNullOpts.mkBool false "";
+
+        useWidgets = helpers.defaultNullOpts.mkBool true "Whether to use widgets.";
+
+        mappings =
+          helpers.defaultNullOpts.mkNullable
+          (with types; attrsOf str)
+          ''
+            {
+              K = "click";
+              "<CR>" = "click";
+              gd = "go_to_def";
+              gD = "go_to_decl";
+              gy = "go_to_type";
+              I = "mouse_enter";
+              i = "mouse_leave";
+              "<Esc>" = "clear_all";
+              C = "clear_all";
+              "<LocalLeader><Tab>" = "goto_last_window";
+            }
+          ''
+          "Mappings.";
+      };
+
+      progressBars = {
+        enable = helpers.defaultNullOpts.mkBool true ''
+          Whether to enable the progress bars.
+        '';
+
+        priority = helpers.defaultNullOpts.mkUnsignedInt 10 ''
+          Use a different priority for the signs.
+        '';
+      };
+
+      stderr = {
+        enable = helpers.defaultNullOpts.mkBool true ''
+          Redirect Lean's stderr messages somehwere (to a buffer by default).
+        '';
+
+        height = helpers.defaultNullOpts.mkPositiveInt 5 "Height of the window.";
+
+        onLines = helpers.mkNullOrOption types.str ''
+          A callback which will be called with (multi-line) stderr output.
+
+          e.g., use:
+          ```nix
+            onLines = "function(lines) vim.notify(lines) end";
+          ```
+          if you want to redirect stderr to `vim.notify`.
+          The default implementation will redirect to a dedicated stderr
+          window.
+        '';
+      };
+
+      lsp3 =
+        helpers.defaultNullOpts.mkNullable
+        (
+          with types;
+            submodule {
+              freeformType = types.attrs;
+              options = {
+                enable = helpers.defaultNullOpts.mkBool true ''
+                    Whether to enable the legacy Lean 3 language server ?
+
+                    Set to `false` to disable, otherwise should be a table of options to pass to
+                  `lean3ls`.
+                  See https://github.com/neovim/nvim-lspconfig/blob/master/doc/server_configurations.md#lean3ls
+                    for details.
+                '';
+
+                on_attach = helpers.mkNullOrOption types.str "The LSP handler.";
+              };
+            }
+        )
+        "{}"
+        "Legacy Lean3 LSP settings.";
+    };
+
+  config = mkIf cfg.enable {
+    extraPlugins = [cfg.package];
+
+    assertions = [
+      {
+        assertion =
+          !(
+            # leanls lsp server is disabled in nvim-lspconfig
+            config.plugins.lsp.servers.leanls.enable
+            # lsp is not (!) disabled in the lean.nvim plugin
+            && !(
+              # lsp is explicitly set to `false`.
+              (isBool cfg.lsp.enable)
+              && !cfg.lsp.enable
+            )
+          );
+        message = ''
+          You have not explicitly set `plugins.lean.lsp` to `false` while having `plugins.lsp.servers.leanls.enable` set to `true`.
+          You need to either
+
+            - Remove the configuration in `plugins.lsp.servers.leanls` and move it to `plugins.lean.lsp`.
+            - Explicitly disable the autoconfiguration of the lsp in the lean.nvim plugin by setting `plugins.lean.lsp` to `false`.
+
+          https://github.com/neovim/nvim-lspconfig/blob/master/doc/server_configurations.md#leanls
+        '';
+      }
+    ];
+
+    extraPackages = optional (cfg.leanPackage != null) cfg.leanPackage;
+
+    extraConfigLua = let
+      setupOptions = with cfg;
+        {
+          inherit lsp;
+          ft = with ft; {
+            inherit
+              default
+              nomodifiable
+              ;
+          };
+          abbreviations = with abbreviations; {
+            inherit
+              enable
+              extra
+              leader
+              ;
+          };
+          inherit mappings;
+          infoview = with infoview; {
+            inherit
+              autoopen
+              autopause
+              width
+              height
+              ;
+            horizontal_position = horizontalPosition;
+            separate_tab = separateTab;
+            inherit indicators;
+            lean3 = with lean3; {
+              show_filter = showFilter;
+              mouse_events = mouseEvents;
+            };
+            show_processing = showProcessing;
+            show_no_info_message = showNoInfoMessage;
+            use_widgets = useWidgets;
+            inherit mappings;
+          };
+          progress_bars = with progressBars; {
+            inherit
+              enable
+              priority
+              ;
+          };
+          stderr = with stderr; {
+            inherit
+              enable
+              height
+              ;
+            on_lines =
+              helpers.ifNonNull' onLines
+              (helpers.mkRaw onLines);
+          };
+          inherit lsp3;
+        }
+        // cfg.extraOptions;
+    in ''
+      require("lean").setup(${helpers.toLuaObject setupOptions})
+    '';
+  };
+}

plugins/lsp/language-servers/default.nix

@@ -237,6 +237,11 @@ with lib; let
       description = "Enable kotlin language server";
       serverName = "kotlin_language_server";
     }
+    {
+      name = "leanls";
+      description = "Enable leanls, for Lean";
+      package = pkgs.lean;
+    }
     {
       name = "ltex";
       description = "Enable ltex-ls, for LanguageTool";