From b46aa0524142ae5dfd77aa255fa9401a019bba2a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 27 Aug 2021 15:37:55 +0200 Subject: [PATCH] doc: new way to install lean4-mode The current installation procedure requires you to have and update a checkout of lean4 yourself which is rather annoying if you are just someone who wants to work with lean4-mode for another project. straight.el + use-package provide a nice alternative to the current approach. --- lean4-mode/README.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/lean4-mode/README.md b/lean4-mode/README.md index 95251d5413..0b3bfceaa5 100644 --- a/lean4-mode/README.md +++ b/lean4-mode/README.md @@ -21,6 +21,25 @@ To use `lean4-mode` in Emacs, add the following to your `init.el`: (require 'lean4-mode) ``` +Alternatively if you are a fan of `use-package` and `straight.el` you +can use: +``` +(use-package lean4-mode + :straight (lean4-mode :type git :host github :repo "leanprover/lean4" + :files ("lean4-mode/lean4*.el")) + ;; to defer loading the package until required + :commands (lean4-mode)) +``` +If you are working on the `lean4` repository already and don't want to +have two separate checkouts you can use: +``` +(use-package lean4-mode + :straight (lean4-mode :local-repo "/path/to/your/lean4" + :files ("lean4-mode/lean4*.el")) + ;; to defer loading the package until required + :commands (lean4-mode)) +``` + Trying It Out =============