(Re)generate: (find-lean4-intro)
Source code:  (find-efunction 'find-lean4-intro)
More intros:  (find-eev-quick-intro)
              (find-eev-intro)
              (find-eepitch-intro)
This buffer is _temporary_ and _editable_.
It is meant as both a tutorial and a sandbox.


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")



. 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")

  (find-windows-beginner-intro)
  (find-windows-beginner-intro "6. Learn the basics of Emacs and eev")

  (find-emacs-keys-intro "1. Basic keys (eev)")
  (find-emacs-keys-intro "2. Key sequences and how to abort them")
  (find-emacs-keys-intro "3. Cutting & pasting")
  (find-emacs-keys-intro "4. Moving point")
  (find-emacs-keys-intro "5. Undoing")
  (find-emacs-keys-intro "6. Windows")
  (find-emacs-keys-intro "7. Files and buffers")

  (find-eev-quick-intro "2. Evaluating Lisp")
  (find-eev-quick-intro "3. Elisp hyperlinks")
  (find-eev-quick-intro "3.1. Non-elisp hyperlinks")
  (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/2024-find-dot-emacs-links.html

  (find-eev-quick-intro "6.1. The main key: <F8>")
  (find-eev-quick-intro "6.2. Other targets")
  (find-eev-quick-intro "6.3. Creating eepitch blocks: `M-T'")
  (find-eev-quick-intro "6.4. Red stars")
    http://anggtwu.net/eepitch.html#test-blocks
    http://anggtwu.net/eepitch.html#trying-it

  (find-eev-quick-intro "7. Quick access to one-liners")
  (find-eev-quick-intro "7.1. `eejump'")
  (find-eev-quick-intro "7.2. The list of eejump targets")
  (find-eev-quick-intro "8. Anchors")
  (find-eev-quick-intro "8.1. Introduction: `to'")
  (find-eev-quick-intro "9. Shorter hyperlinks")
  (find-eev-quick-intro "9.1. `code-c-d'")
  (find-eev-quick-intro "9.2. Extra arguments to `code-c-d'")

  (find-psne-intro "1. Local copies of files from the internet")
  (find-psne-intro "3. The new way: `M-x brep'")
    http://anggtwu.net/eev-videos.html#links-to-videos
    http://anggtwu.net/eev-videos.html#what-are-local-copies
    http://anggtwu.net/eev-videos.html#first-class-videos
    http://anggtwu.net/eev-videos.html#mpv-keys

  (find-pdf-like-intro "1. PDF-like documents")
  (find-pdf-like-intro "2. Preparation")
  (find-pdf-like-intro "3. Hyperlinks to PDF files")
  (find-pdf-like-intro "4. Hyperlinks to pages of PDF files")
  (find-pdf-like-intro "5. A convention on page numbers")
  (find-pdf-like-intro "6. How the external programs are called")
  (find-pdf-like-intro "7. Shorter hyperlinks to PDF files")
  (find-pdf-like-intro "8. `find-pdf'-pairs")

  (find-kl-here-intro "1. Introduction")
  (find-kl-here-intro "2. Try it!")
  (find-kl-here-intro "3. Info")





. Download the five manuals
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
  mkdir -p $S
  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



. Setup the ~/.emacs
See: http://anggtwu.net/2024-find-dot-emacs-links.html
Use: (find-dot-emacs-links "eevgit eev angges melpa lean4 maxima5470 mfms")



. Test the five manuals
  (find-fplean4doc   "getting-to-know/evaluating")
  (find-lean4doc     "whatIsLean")
  (find-leanmetadoc  "main/01_intro")
  (find-tclean4doc   "trust/trust")
  (find-tpil4doc     "introduction")
  (find-fplean4page  9 "Evaluating Expressions")
  (find-fplean4text  9 "Evaluating Expressions")
  (find-lean4page    1 "What is Lean")
  (find-lean4text    1 "What is Lean")
  (find-leanmetapage 1 "What's the goal of this book?")
  (find-leanmetatext 1 "What's the goal of this book?")
  (find-tclean4page  5 "Trust")
  (find-tclean4text  5 "Trust")
  (find-tpil4page    1 "Introduction")
  (find-tpil4text    1 "Introduction")

  Broken - I did not include this one:
  (find-leanrefdoc   "using_lean#using-lean-with-emacs")
  (find-leanrefdocw  "using_lean#using-lean-with-emacs")
  https://leanprover.github.io/reference/using_lean.html#using-lean-with-emacs



. 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 -- -y --default-toolchain leanprover/lean4:stable

The "-y" after the "sh" in the last line makes the installer use
certain defaults without asking questions.

Note about $PATH: if you remove the "-y" then the installer may 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,
you can say no - because of this:

  (find-eev "eev-lean4.el" "PATH")




. 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")





. Install lean4-mode
The instructions in

  https://github.com/leanprover-community/lean4-mode

are not very beginner-friendly. So: follow the instructions
in the temporary buffer generated by the sexp below,

  (find-package-vc-install-links "https://github.com/leanprover-community/lean4-mode")

then run this progn,

  (progn
    (find-2a nil '(find-ebuffer "*Messages*"))
    (add-to-list 'package-archives
      '("melpa" . "https://melpa.org/packages/"))
    ;;
    ;; See:
    ;; https://mail.gnu.org/archive/html/help-gnu-emacs/2024-05/msg00248.html
    ;; https://www.reddit.com/r/emacs/comments/bn6k1y/updating_gnu_elpa_keys/
    ;; http://anggtwu.net/2024-no-public-key.html
    (package-initialize)
    (setq package-check-signature nil)
    (package-refresh-contents)
    (package-install 'gnu-elpa-keyring-update)
    (setq package-check-signature 'allow-unsigned)
    ;;
    ;; See:
    ;; https://emacs.stackexchange.com/questions/80871/how-to-provide-updated-seq-package-to-magit
    (setq package-install-upgrade-built-in t)
    (package-install 'compat)
    (package-install 'seq)
    (progn (unload-feature 'seq t) (require 'seq))
    (package-install 'magit)
    ;;
    ;; Missing in the instructions for lean4-mode:
    (package-install 'company)
    ;;
    ;; From the instructions for lean4-mode:
    (package-install 'dash)
    (package-install 'flycheck)
    (package-install 'lsp-mode)
    (package-install 'magit-section)
    )

and try:

  (require 'lean4-mode)

If that `require' returns `lean4-mode', that's a good sign.




. 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 ("i") to say that it is at the directory above, i.e., at:

  ~/.elan/toolchains/leanprover--lean4---stable/

Answer "i". Note: I don't understand projects and project roots well
enough... =(




. 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 to   (xref-find-definitions)
  M-,   - go back (xref-go-back)

For a demo of these keys, see this part of the video (in Portuguese):

  (find-2024lean4of0hsubs "14:12" "`go to' e `go back'")
  (find-2024lean4of0video "14:12" "`go to' e `go back'")




. Try a snippet
Watch this part of the video,

  (find-2024lean4of0hsubs "16:31" "(anotações sobre coerção)")
  (find-2024lean4of0video "16:31" "(anotações sobre coerção)")
  (find-2024lean4of0hsubs "17:39" "bota isso aqui no clipboard do Emacs")
  (find-2024lean4of0video "17:39" "bota isso aqui no clipboard do Emacs")

and try to use the notes in the link below, including the snippet.
If LSP asks for a project root, answer "i", for:

  i ==> Import project root /tmp/L/

Here is the link:

  (find-es "lean" "Std.Format")