[elpa] externals/eev 85894082c5: Several changes in (find-lean4-intro) and related code.

[ELPA Syncer]

branch: externals/eev
commit 85894082c5f4de2617e9e7efee30817708174f7e
Author: Eduardo Ochs <eduardoochs@gmail.com>
Commit: Eduardo Ochs <eduardoochs@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  <eduardoochs@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 <eduardoochs@gmail.com>
 ;; Maintainer: Eduardo Ochs <eduardoochs@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 <eduardoochs@gmail.com>
 ;; Maintainer: Eduardo Ochs <eduardoochs@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 <eduardoochs@gmail.com>
 ;; Maintainer: Eduardo Ochs <eduardoochs@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))