branch: externals/eev
commit 85894082c5f4de2617e9e7efee30817708174f7e
Author: Eduardo Ochs <eduardoo...@gmail.com>
Commit: Eduardo Ochs <eduardoo...@gmail.com>
Several changes in (find-lean4-intro) and related code.
---
ChangeLog | 2 ++
VERSION | 4 +--
eev-intro.el | 104 +++++++++++++++++++++++++++++++++++++++++++++++++++-------
eev-lean4.el | 22 ++++++++++---
eev-tlinks.el | 12 +++++--
5 files changed, 124 insertions(+), 20 deletions(-)
diff --git a/ChangeLog b/ChangeLog
index 4f27c110e5..4de12e3d8d 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,7 @@
2024-07-26 Eduardo Ochs <eduardoo...@gmail.com>
+ * eev-tlinks.el (ee-dot-emacs-eevgit): new function.
+
* eev.el: bumped the version.
* eev-videolinks.el (ee-1stclassvideos-info): new video:
diff --git a/VERSION b/VERSION
index ccac3183e0..bb452b0c12 100644
--- a/VERSION
+++ b/VERSION
@@ -1,2 +1,2 @@
-Fri Jul 26 05:30:34 GMT 2024
-Fri Jul 26 02:30:34 -03 2024
+Sat Jul 27 00:17:49 GMT 2024
+Fri Jul 26 21:17:49 -03 2024
diff --git a/eev-intro.el b/eev-intro.el
index d9ccf313b0..21c32589f7 100644
--- a/eev-intro.el
+++ b/eev-intro.el
@@ -19,7 +19,7 @@
;;
;; Author: Eduardo Ochs <eduardoo...@gmail.com>
;; Maintainer: Eduardo Ochs <eduardoo...@gmail.com>
-;; Version: 20240724
+;; Version: 20240726
;; Keywords: e-scripts
;;
;; Latest version: <http://anggtwu.net/eev-current/eev-intro.el>
@@ -17799,18 +17799,24 @@ This buffer is _temporary_ and _editable_.
It is meant as both a tutorial and a sandbox.
-Warning: WORK IN PROGRESS!
-VERY EARLY DRAFT!
-UNFINISHED! UNTESTED!
+THIS IS A WORK IN PROGRESS!!!
+I am using it in this workshop:
+ Page: http://anggtwu.net/2024-lean4-oficina-0.html
+ Play: (find-2024lean4of0video \"00:00\")
+ HSubs: (find-2024lean4of0hsubs \"00:00\")
+ Info: (find-1stclassvideo-links \"2024lean4of0\")
0. Prerequisites
================
+See: http://anggtwu.net/2024-first-executable-notes.html
+Copy the rest of this section to your ~/TODO, and try to
+understand its links:
+
(find-eev-quick-intro \"7. Quick access to one-liners\")
(find-eev-quick-intro \"7. Quick access to one-liners\" \"forget\")
- http://anggtwu.net/2024-lean4-oficina-0.html
(find-windows-beginner-intro)
(find-windows-beginner-intro \"6. Learn the basics of Emacs and eev\")
@@ -17828,7 +17834,6 @@ UNFINISHED! UNTESTED!
(find-eev-quick-intro \"5. Links to Emacs documentation\")
(find-eev-quick-intro \"5.1. Navigating the Emacs manuals\")
(find-eev-quick-intro \"5.2. Cutting and pasting\")
- http://anggtwu.net/IMAGES/2024-emacs-cut-copy-and-paste.png
http://anggtwu.net/2024-find-dot-emacs-links.html
(find-eev-quick-intro \"6.1. The main key: <F8>\")
@@ -17880,6 +17885,7 @@ UNFINISHED! UNTESTED!
cd /tmp/
wget -N http://anggtwu.net/tmp/2024-lean4-oficina-manuais.tgz
# (find-fline \"/tmp/2024-lean4-oficina-manuais.tgz\")
+ tar -tvzf /tmp/2024-lean4-oficina-manuais.tgz
tar -C $S/ -xvzf /tmp/2024-lean4-oficina-manuais.tgz
@@ -17887,7 +17893,7 @@ UNFINISHED! UNTESTED!
2. Setup the ~/.emacs
=====================
See: http://anggtwu.net/2024-find-dot-emacs-links.html
-Use: (find-dot-emacs-links \"eev angges melpa lean4 maxima5470 mfms\")
+Use: (find-dot-emacs-links \"eevgit eev angges melpa lean4 maxima5470 mfms\")
@@ -17913,12 +17919,52 @@ Use: (find-dot-emacs-links \"eev angges melpa lean4
maxima5470 mfms\")
4. Install Lean4
================
+Follow the instructions here:
+
(find-es \"lean\" \"install-2024\")
+i.e.,:
+
+ (eepitch-shell)
+ (eepitch-kill)
+ (eepitch-shell)
+ rm -Rv /tmp/elan-install/
+ mkdir /tmp/elan-install/
+ cd /tmp/elan-install/
+ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
-sSf \
+ | sh -s -- --default-toolchain leanprover/lean4:stable
+
+The installer will ask if you want it to change some files like
+~/.bashrc and ~/.zshrc to include ~/.elan/bin/ in the PATH. If you're
+only going to use Lean from Emacs, say no - because of this:
+
+ (find-eev \"eev-lean4.el\" \"PATH\")
+
+
+
+
+5. Take a look at the libraries
+===============================
+If everything went right then the installer will put Lean's libraries
+here,
+
+ (find-fline \"~/.elan/toolchains/\")
+ (find-fline \"~/.elan/toolchains/leanprover--lean4---stable/\")
+
+and these short hyperlink should work:
+
+ (find-lean4prefile \"\")
+ (find-lean4presh \"find * | sort\")
+
+If they don't work you will need to override a `code-c-d' that is here:
+
+ (find-eev \"eev-lean4.el\" \"code-c-ds\")
+
+
-5. Install lean4-mode
+6. Install lean4-mode
=====================
The instructions in
@@ -17939,17 +17985,53 @@ then run this progn,
(package-install 'flycheck)
(package-install 'lsp-mode)
(package-install 'magit-section)
+ (package-install 'company)
)
and try:
(require 'lean4-mode)
+If that `require' returns `lean4-mode', that's a good sign.
-6. Test lean4-mode
-==================
- (find-es \"lean\" \"Std.Format\")
+
+
+7. Project root
+===============
+If you open the file Init.lean with the second sexp below,
+
+ (find-lean4prefile \"\")
+ (find-lean4prefile \"Init.lean\")
+
+then lsp-mode will ask where is the \"project root\", and there will be
+an option to say that it is at that the directory above, i.e., at:
+
+ ~/.elan/toolchains/leanprover--lean4---stable/
+
+I don't understand projects and project roots well... =(
+
+
+
+
+8. Visit a .lean file
+=====================
+Try this with `M-3 M-e':
+
+ (find-lean4prefile \"Init/Data/Format/Basic.lean\" \"inductive Format\")
+
+the prefix `M-3' will make the file be opened at the window at the
+right. Then try these navigation keys:
+
+ M-. - go forward (xref-find-definitions)
+ M-, - go back (xref-go-back)
+
+
+
+9. Try a snippet
+================
+In: (find-es \"lean\" \"Std.Format\")
+TODO: explain this!
diff --git a/eev-lean4.el b/eev-lean4.el
index 65534498e2..6aae421a8b 100644
--- a/eev-lean4.el
+++ b/eev-lean4.el
@@ -19,7 +19,7 @@
;;
;; Author: Eduardo Ochs <eduardoo...@gmail.com>
;; Maintainer: Eduardo Ochs <eduardoo...@gmail.com>
-;; Version: 20240707
+;; Version: 20240726
;; Keywords: e-scripts
;;
;; Latest version: <http://anggtwu.net/eev-current/eev-lean4.el>
@@ -33,15 +33,18 @@
;; This file contains part of the setup for this workshop:
;;
;; http://anggtwu.net/2024-lean4-oficina-0.html
+;; (find-lean4-intro)
;;
;; This is very experimental and very undocumented!
;;
-;; (load (buffer-file-name))
+;; (load (buffer-file-name))
;;
;; Index:
;; «.PATH» (to "PATH")
+;; «.lean4-mode» (to "lean4-mode")
+;; «.code-c-ds» (to "code-c-ds")
;; «.etc» (to "etc")
;; «.ee-let*-macro-leandoc» (to "ee-let*-macro-leandoc")
;; «.code-leandocpdf» (to "code-leandocpdf")
@@ -74,13 +77,20 @@
;; (find-sh "echo $PATH | tr : '\n'")
-;; «etc» (to ".etc")
+;; «lean4-mode» (to ".lean4-mode")
+;; See: (find-lean4-intro "6. Install lean4-mode")
+(add-to-list 'load-path "~/.emacs.d/elpa/lean4-mode")
+(ignore-errors (require 'lean4-mode))
+
+
+;; «code-c-ds» (to ".code-c-ds")
;; (find-lean4prefile "")
;; (find-lean4presh "find * | sort")
(code-c-d "lean4pre"
"~/.elan/toolchains/leanprover--lean4---stable/src/lean/")
-;; If lean4-mode or lsp-mode are not installed
-;; these `code-c-d's will do weird things.
+;; If lean4-mode or lsp-mode are not installed then the `code-c-d's
+;; below will point to "nil" instead of to a real directory, and you
+;; will have to rerun them at some point.
;;
;; (find-code-c-d "lean4mode" (ee-locate-library "lean4-mode"))
;; (find-code-c-d "lspmode" (ee-locate-library "lsp-mode"))
@@ -89,6 +99,8 @@
;; (find-lean4modefile "")
;; (find-lspmodefile "")
+
+;; «etc» (to ".etc")
;; (find-es "lean" "lean4-mode-vc")
;; (find-es "lsp" "lsp-mode-git")
diff --git a/eev-tlinks.el b/eev-tlinks.el
index 92d4d3108f..a55c1f1b6e 100644
--- a/eev-tlinks.el
+++ b/eev-tlinks.el
@@ -19,7 +19,7 @@
;;
;; Author: Eduardo Ochs <eduardoo...@gmail.com>
;; Maintainer: Eduardo Ochs <eduardoo...@gmail.com>
-;; Version: 20240721
+;; Version: 20240726
;; Keywords: e-scripts
;;
;; Latest version: <http://anggtwu.net/eev-current/eev-tlinks.el>
@@ -3970,6 +3970,12 @@ is nil, use the result of (ee-1stclassvideos)."
collect (funcall sym))
"\n"))
+;; Test: (find-estring-elisp (ee-dot-emacs-eevgit))
+(defun ee-dot-emacs-eevgit (&rest rest) "\
+;; See: (find-package-vc-install-links \"https://github.com/edrx/eev\";)
+(add-to-list 'load-path \"~/.emacs.d/elpa/eev\")
+")
+
;; Test: (find-estring-elisp (ee-dot-emacs-eev))
(defun ee-dot-emacs-eev (&rest rest) "\
;; See: (find-eev-levels-intro)
@@ -4015,8 +4021,10 @@ is nil, use the result of (ee-1stclassvideos)."
;; Test: (find-estring-elisp (ee-dot-emacs-lean4))
(defun ee-dot-emacs-lean4 (&rest rest) "\
;; See: (find-lean4-intro)
-(require 'eev-lean4) ; (find-eev \"eev-lean4.el\")
+(add-to-list 'load-path \"~/.emacs.d/elpa/lean4-mode\")
+(defun fli () (interactive) (find-lean4-intro))
(defun el4 () (interactive) (find-eev \"eev-lean4.el\"))
+(require 'eev-lean4) ; (find-eev \"eev-lean4.el\")
")
;; Test: (find-estring-elisp (ee-dot-emacs-mfms))
