max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: lean4-mode: remove obsolete dependency

Browse source
This commit is contained in:
Sebastian Ullrich 2021-03-05 16:58:01 +01:00
parent f40e5411ac
commit edf4a2be72
4 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
lean4-mode/README.md
View file

@ -6,7 +6,7 @@ To use `lean4-mode` in Emacs, add the following to your `init.el`:
;; You need to modify the following line
(setq load-path (cons "/path/to/lean4/lean4-mode" load-path))
(setq lean4-mode-required-packages '(dash dash-functional f flycheck lsp-mode s))
(setq lean4-mode-required-packages '(dash f flycheck lsp-mode s))
(require 'package)
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/"))

2
lean4-mode/lean4-mode.el
View file

@ -10,7 +10,7 @@
;; Maintainer: Sebastian Ullrich <sebasti@nullri.ch>
;; Created: Jan 09, 2014
;; Keywords: languages
;; Package-Requires: ((emacs "24.3") (dash "2.12.0") (dash-functional "1.2.0") (s "1.10.0") (f "0.19.0") (flycheck "30"))
;; Package-Requires: ((emacs "24.3") (dash "2.18.0") (s "1.10.0") (f "0.19.0") (flycheck "30"))
;; URL: https://github.com/leanprover/lean4-mode
;; Released under Apache 2.0 license as described in the file LICENSE.

1
lean4-mode/lean4-util.el
View file

@ -8,7 +8,6 @@
(require 'f)
(require 's)
(require 'dash)
(require 'dash-functional)
(defun lean4-setup-rootdir ()
(let ((root (executable-find lean4-executable-name)))

2
nix/packages.nix
View file

@ -48,7 +48,7 @@ let
pname = "lean4-mode";
version = "1";
src = ../lean4-mode;
packageRequires = with pkgs.emacsPackages.melpaPackages; [ dash dash-functional f flycheck lsp-mode s ];
packageRequires = with pkgs.emacsPackages.melpaPackages; [ dash f flycheck lsp-mode s ];
recipe = pkgs.writeText "recipe" ''
(lean4-mode :repo "leanprover/lean4" :fetcher github :files ("*.el"))
'';