From dbf9e9e2c7cf3a3c56ad398cfe3ce43407bbacd4 Mon Sep 17 00:00:00 2001 From: Rudi Grinberg Date: Sat, 7 Sep 2019 02:18:51 +0900 Subject: [PATCH 1/4] Add a module for the lean theorem prover Signed-off-by: Rudi Grinberg --- modules/lang/lean/config.el | 33 +++++++++++++++++++++++++++++++++ modules/lang/lean/packages.el | 7 +++++++ 2 files changed, 40 insertions(+) create mode 100644 modules/lang/lean/config.el create mode 100644 modules/lang/lean/packages.el diff --git a/modules/lang/lean/config.el b/modules/lang/lean/config.el new file mode 100644 index 000000000..faf37150c --- /dev/null +++ b/modules/lang/lean/config.el @@ -0,0 +1,33 @@ +;;; lang/lean/config.el -*- lexical-binding: t; -*- + +(use-package! company-lean + :when (featurep :completion 'company) + :after lean-mode + :config (set-company-backend! 'lean-mode 'company-lean)) + +(use-package! lean-mode + :config + (set-lookup-handlers! 'lean-mode + :definition #'lean-find-definition) + (sp-with-modes 'lean-mode + (sp-local-pair "/-" "-/") + (sp-local-pair "`'" nil :actions :rem) + (sp-local-pair "{" "}") + (sp-local-pair "«" "»")) + (map! + :map lean-mode-map + :localleader + "g" #'lean-toggle-show-goal + "n" #'lean-toggle-next-error + (:prefix "s" + "r" #'lean-server-restart + "s" #'lean-server-stop + "v" #'lean-server-switch-version) + (:prefix "p" + "t" #'lean-leanpkg-test + "b" #'lean-leanpkg-build + "c" #'lean-leanpkg-configure) + "f" #'lean-fill-placeholder + "h" #'lean-hole + "m" #'lean-message-boxes-toggle + "e" #'lean-execute)) diff --git a/modules/lang/lean/packages.el b/modules/lang/lean/packages.el new file mode 100644 index 000000000..6061c61f6 --- /dev/null +++ b/modules/lang/lean/packages.el @@ -0,0 +1,7 @@ +;; -*- no-byte-compile: t; -*- +;;; lang/lean/packages.el + +(package! lean-mode) + +(when (featurep! :completion company) + (package! company-lean)) From 2527306069d122478acf118a5ce0b19bbbd5bc05 Mon Sep 17 00:00:00 2001 From: Rudi Grinberg Date: Sat, 7 Sep 2019 15:27:20 +0900 Subject: [PATCH 2/4] Use map! with after! to setup bindings Signed-off-by: Rudi Grinberg --- modules/lang/lean/config.el | 53 +++++++++++++++++++------------------ 1 file changed, 27 insertions(+), 26 deletions(-) diff --git a/modules/lang/lean/config.el b/modules/lang/lean/config.el index faf37150c..676bf3534 100644 --- a/modules/lang/lean/config.el +++ b/modules/lang/lean/config.el @@ -1,33 +1,34 @@ ;;; lang/lean/config.el -*- lexical-binding: t; -*- -(use-package! company-lean - :when (featurep :completion 'company) - :after lean-mode - :config (set-company-backend! 'lean-mode 'company-lean)) - -(use-package! lean-mode - :config +(after! lean-mode (set-lookup-handlers! 'lean-mode :definition #'lean-find-definition) (sp-with-modes 'lean-mode (sp-local-pair "/-" "-/") - (sp-local-pair "`'" nil :actions :rem) + (sp-local-pair "`" "`") (sp-local-pair "{" "}") - (sp-local-pair "«" "»")) - (map! - :map lean-mode-map - :localleader - "g" #'lean-toggle-show-goal - "n" #'lean-toggle-next-error - (:prefix "s" - "r" #'lean-server-restart - "s" #'lean-server-stop - "v" #'lean-server-switch-version) - (:prefix "p" - "t" #'lean-leanpkg-test - "b" #'lean-leanpkg-build - "c" #'lean-leanpkg-configure) - "f" #'lean-fill-placeholder - "h" #'lean-hole - "m" #'lean-message-boxes-toggle - "e" #'lean-execute)) + (sp-local-pair "«" "»") + (sp-local-pair "⟨" "⟩") + (sp-local-pair "⟪" "⟫")) + (map! :map lean-mode-map + :localleader + "g" #'lean-toggle-show-goal + "n" #'lean-toggle-next-error + (:prefix ("s" . "server") + "r" #'lean-server-restart + "s" #'lean-server-stop + "v" #'lean-server-switch-version) + (:prefix ("p" . "leanpkg") + "t" #'lean-leanpkg-test + "b" #'lean-leanpkg-build + "c" #'lean-leanpkg-configure) + "f" #'lean-fill-placeholder + "h" #'lean-hole + "m" #'lean-message-boxes-toggle + "e" #'lean-execute)) + + +(use-package! company-lean + :when (featurep! :completion company) + :after lean-mode + :config (set-company-backend! 'lean-mode 'company-lean)) From 8778eb22883fcdbca757993a844c57b8589f3649 Mon Sep 17 00:00:00 2001 From: Rudi Grinberg Date: Mon, 9 Sep 2019 12:36:29 +0900 Subject: [PATCH 3/4] Disable auto initializatinon of company in lean mode Signed-off-by: Rudi Grinberg --- modules/lang/lean/config.el | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/modules/lang/lean/config.el b/modules/lang/lean/config.el index 676bf3534..3cff278d5 100644 --- a/modules/lang/lean/config.el +++ b/modules/lang/lean/config.el @@ -29,6 +29,8 @@ (use-package! company-lean + :init + (advice-add #'company-lean-hook :override #'ignore) + (set-company-backend! 'lean-mode 'company-lean) :when (featurep! :completion company) - :after lean-mode - :config (set-company-backend! 'lean-mode 'company-lean)) + :after lean-mode) From bba0e1cb79a978e01e4f8fa9d70e2ecdc684d4e0 Mon Sep 17 00:00:00 2001 From: Rudi Grinberg Date: Tue, 10 Sep 2019 09:50:21 +0900 Subject: [PATCH 4/4] Add lean to init.example.el Signed-off-by: Rudi Grinberg --- init.example.el | 1 + 1 file changed, 1 insertion(+) diff --git a/init.example.el b/init.example.el index fec33a81c..39303ef3f 100644 --- a/init.example.el +++ b/init.example.el @@ -118,6 +118,7 @@ ;;julia ; a better, faster MATLAB ;;kotlin ; a better, slicker Java(Script) ;;latex ; writing papers in Emacs has never been so fun + ;;lean ;;ledger ; an accounting system in Emacs ;;lua ; one-based indices? one-based indices markdown ; writing docs for people to ignore