[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[elpa] externals/eev 0d6ae77866: Added `ee-symbol-function'; added eev-l
|
From: |
ELPA Syncer |
|
Subject: |
[elpa] externals/eev 0d6ae77866: Added `ee-symbol-function'; added eev-lean4.el. |
|
Date: |
Wed, 24 Jul 2024 15:58:08 -0400 (EDT) |
branch: externals/eev
commit 0d6ae77866450faf5e543d5b679d638347c88879
Author: Eduardo Ochs <eduardoochs@gmail.com>
Commit: Eduardo Ochs <eduardoochs@gmail.com>
Added `ee-symbol-function'; added eev-lean4.el.
---
ChangeLog | 7 +
VERSION | 4 +-
eev-blinks.el | 39 ++++-
eev-intro.el | 48 +++++-
eev-lean4.el | 487 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
5 files changed, 572 insertions(+), 13 deletions(-)
diff --git a/ChangeLog b/ChangeLog
index 6a68cfcc47..89ac17b6ea 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,10 @@
+2024-07-24 Eduardo Ochs <eduardoochs@gmail.com>
+
+ * eev-blinks.el (ee-closure-to-lambda, ee-symbol-function): new
+ functions.
+ (ee-defun-sexp-for, ee-shortdefp, find-efunctionpp): use
+ `ee-symbol-function'.
+
2024-07-22 Eduardo Ochs <eduardoochs@gmail.com>
* eev-intro.el (find-lean4-intro): small changes.
diff --git a/VERSION b/VERSION
index 0d0211ace5..6adcd6f687 100644
--- a/VERSION
+++ b/VERSION
@@ -1,2 +1,2 @@
-Mon Jul 22 05:40:28 GMT 2024
-Mon Jul 22 02:40:28 -03 2024
+Wed Jul 24 18:34:05 GMT 2024
+Wed Jul 24 15:34:05 -03 2024
diff --git a/eev-blinks.el b/eev-blinks.el
index 8edc9bd0c1..dfe3a22630 100644
--- a/eev-blinks.el
+++ b/eev-blinks.el
@@ -21,7 +21,7 @@
;;
;; Author: Eduardo Ochs <eduardoochs@gmail.com>
;; Maintainer: Eduardo Ochs <eduardoochs@gmail.com>
-;; Version: 20240530
+;; Version: 20240724
;; Keywords: e-scripts
;;
;; Latest version: <http://anggtwu.net/eev-current/eev-blinks.el>
@@ -73,6 +73,7 @@
;; «.find-einternals» (to "find-einternals")
;; «.find-einsert» (to "find-einsert")
;; «.find-eunicode» (to "find-eunicode")
+;; «.ee-symbol-function» (to "ee-symbol-function")
;; «.find-eejumps» (to "find-eejumps")
;; «.find-eeshortdefs» (to "find-eeshortdefs")
;; «.find-eaproposf» (to "find-eaproposf")
@@ -1407,7 +1408,7 @@ that `find-epp' would print in a single line."
(body (format ";; %s\n;; See: %S\n;;\n%s\n"
fefpp
'(find-eev "eev-blinks.el" "find-efunctionpp")
- (pp-to-string (symbol-function symbol)))))
+ (pp-to-string (ee-symbol-function symbol)))))
(apply 'find-estring-elisp body pos-spec-list)))
;; Test: (find-eppp-with-prefix ";; HELLO\n" '(1 "2" (3 4)))
@@ -1680,6 +1681,30 @@ Hint: install the Debian package \"unicode-data\".")
+;;; _
+;;; ___| | ___ ___ _ _ _ __ ___ ___
+;;; / __| |/ _ \/ __| | | | '__/ _ \/ __|
+;;; | (__| | (_) \__ \ |_| | | | __/\__ \
+;;; \___|_|\___/|___/\__,_|_| \___||___/
+;;;
+;; «ee-symbol-function» (to ".ee-symbol-function")
+;; This is an experimental hack for handling some versions of Emacs31. See:
+;; https://lists.gnu.org/archive/html/help-gnu-emacs/2024-07/msg00292.html
+;; https://lists.gnu.org/archive/html/help-gnu-emacs/2024-07/msg00311.html
+
+(defun ee-closure-to-lambda (c)
+ "Experimental!!! See the comments in the source!"
+ `(lambda ,(aref c 0) ,@(aref c 1)))
+
+(defun ee-symbol-function (sym)
+ "Experimental!!! See the comments in the source!"
+ (let ((o (symbol-function sym)))
+ (if (closurep o)
+ (ee-closure-to-lambda o)
+ o)))
+
+
+
;;; __ _ _ _
@@ -1696,7 +1721,7 @@ Hint: install the Debian package \"unicode-data\".")
;; Related to: (find-eev "eejump.el")
(defun ee-defun-sexp-for (symbol)
- `(defun ,symbol ,@(cdr (symbol-function symbol))))
+ `(defun ,symbol ,@(cdr (ee-symbol-function symbol))))
(defun ee-defun-str-for (symbol)
(replace-regexp-in-string
@@ -1752,10 +1777,10 @@ Hint: install the Debian package \"unicode-data\".")
(defun ee-shortdefp (sym)
(and (fboundp sym)
(commandp sym)
- (listp (symbol-function sym))
- (eq (car (symbol-function sym)) 'lambda)
- (<= (length (symbol-name sym)) ee-shortdefp-maxlen-name)
- (<= (length (ee-defun-str-for sym)) ee-shortdefp-maxlen-def)))
+ (listp (ee-symbol-function sym))
+ (eq (car (ee-symbol-function sym)) 'lambda)
+ (<= (length (symbol-name sym)) ee-shortdefp-maxlen-name)
+ (<= (length (ee-defun-str-for sym)) ee-shortdefp-maxlen-def)))
(defun ee-shortdef-symbols ()
(apropos-internal "^.*$" 'ee-shortdefp))
diff --git a/eev-intro.el b/eev-intro.el
index 1b812342a3..86a212ed2e 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: 20240722
+;; Version: 20240724
;; Keywords: e-scripts
;;
;; Latest version: <http://anggtwu.net/eev-current/eev-intro.el>
@@ -17807,6 +17807,9 @@ UNFINISHED! UNTESTED!
0. Prerequisites
================
+ (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\")
@@ -17883,8 +17886,8 @@ UNFINISHED! UNTESTED!
2. Setup the ~/.emacs
=====================
- http://anggtwu.net/2024-find-dot-emacs-links.html
- (find-dot-emacs-links \"eev angges melpa lean4 maxima5470 mfms\")
+See: http://anggtwu.net/2024-find-dot-emacs-links.html
+Use: (find-dot-emacs-links \"eev angges melpa lean4 maxima5470 mfms\")
@@ -17914,9 +17917,46 @@ UNFINISHED! UNTESTED!
+
5. Install lean4-mode
=====================
- (find-es \"lean\" \"lean4-mode-vc\")
+Check the version of your Emacs:
+ (emacs-version)
+If it is at least 29, then running this sexp should be enough:
+
+ (package-vc-install \"https://github.com/leanprover-community/lean4-mode\";)
+
+If not then you need to download lean4-mode with this eepitch block,
+
+ (eepitch-shell)
+ (eepitch-kill)
+ (eepitch-shell)
+# (find-fline \"~/.emacs.d/elpa/lean4-mode/\")
+ rm -Rfv ~/.emacs.d/elpa/lean4-mode/
+ mkdir -p ~/.emacs.d/elpa/lean4-mode/
+ cd ~/.emacs.d/elpa/lean4-mode/
+ git clone https://github.com/leanprover-community/lean4-mode .
+
+Then add \"~/.emacs.d/elpa/lean4-mode/\" to the Emacs load-path, with:
+
+(add-to-list 'load-path \"~/.emacs.d/elpa/lean4-mode/\")
+;; Tests: (find-fline \"~/.emacs.d/elpa/lean4-mode/\")
+;; (ee-locate-library \"lean4-mode\")
+;; (find-eppp load-path)
+
+
+
+
+See: https://github.com/leanprover-community/lean4-mode
+
+
+
+
+ (find-es \"lean\" \"lean4-mode-vc\")
+ (find-efunction 'ee-locate-library)
+ (ee-locate-library \"lean4-mode\")
+ (find-eev \"eev-lean4.el\" \"etc\")
+
(package-vc-install \"https://github.com/leanprover-community/lean4-mode\";)
(find-lean4modefile \"README.md\")
diff --git a/eev-lean4.el b/eev-lean4.el
new file mode 100644
index 0000000000..65534498e2
--- /dev/null
+++ b/eev-lean4.el
@@ -0,0 +1,487 @@
+;;; eev-lean4.el -- Definitions for a workshop on Lean4. -*- lexical-binding:
nil; -*-
+
+;; Copyright (C) 2024 Free Software Foundation, Inc.
+;;
+;; This file is part of GNU eev.
+;;
+;; GNU eev is free software: you can redistribute it and/or modify
+;; it under the terms of the GNU General Public License as published by
+;; the Free Software Foundation, either version 3 of the License, or
+;; (at your option) any later version.
+;;
+;; GNU eev is distributed in the hope that it will be useful,
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+;; GNU General Public License for more details.
+;;
+;; You should have received a copy of the GNU General Public License
+;; along with GNU Emacs. If not, see <http://www.gnu.org/licenses/>.
+;;
+;; Author: Eduardo Ochs <eduardoochs@gmail.com>
+;; Maintainer: Eduardo Ochs <eduardoochs@gmail.com>
+;; Version: 20240707
+;; Keywords: e-scripts
+;;
+;; Latest version: <http://anggtwu.net/eev-current/eev-lean4.el>
+;; htmlized: <http://anggtwu.net/eev-current/eev-lean4.el.html>
+;; See also: <http://anggtwu.net/eev-current/eev-beginner.el.html>
+;; <http://anggtwu.net/eev-intros/find-lean4-intro.html>
+;; (find-lean4-intro)
+
+;;; Comment:
+;;
+;; This file contains part of the setup for this workshop:
+;;
+;; http://anggtwu.net/2024-lean4-oficina-0.html
+;;
+;; This is very experimental and very undocumented!
+;;
+;; (load (buffer-file-name))
+
+;;
+
+;; Index:
+;; «.PATH» (to "PATH")
+;; «.etc» (to "etc")
+;; «.ee-let*-macro-leandoc» (to "ee-let*-macro-leandoc")
+;; «.code-leandocpdf» (to "code-leandocpdf")
+;; «.find-leandocprep-links» (to "find-leandocprep-links")
+;; «.find-leanbook-links» (to "find-leanbook-links")
+;; «.find-leanrstdoc-links» (to "find-leanrstdoc-links")
+;;
+;; «.books» (to "books")
+;; «.leandoc-specs» (to "leandoc-specs")
+;; «.ee-leandoc-:fplean4» (to "ee-leandoc-:fplean4")
+;; «.ee-leandoc-:lean4» (to "ee-leandoc-:lean4")
+;; «.ee-leandoc-:leanmeta» (to "ee-leandoc-:leanmeta")
+;; «.ee-leandoc-:tclean4» (to "ee-leandoc-:tclean4")
+;; «.ee-leandoc-:tpil4» (to "ee-leandoc-:tpil4")
+
+
+
+
+;;; ____ _ _____ _ _
+;;; | _ \ / \|_ _| | | |
+;;; | |_) / _ \ | | | |_| |
+;;; | __/ ___ \| | | _ |
+;;; |_| /_/ \_\_| |_| |_|
+;;;
+;; «PATH» (to ".PATH")
+;; See: (find-es "lean" "install-2024")
+;; export PATH=$HOME/.elan/bin:$PATH
+(setenv "PATH" (format "%s/.elan/bin:%s" (getenv "HOME") (getenv "PATH")))
+;; (find-sh "echo $PATH")
+;; (find-sh "echo $PATH | tr : '\n'")
+
+
+;; «etc» (to ".etc")
+;; (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.
+;;
+;; (find-code-c-d "lean4mode" (ee-locate-library "lean4-mode"))
+;; (find-code-c-d "lspmode" (ee-locate-library "lsp-mode"))
+ (code-c-d "lean4mode" (ee-locate-library "lean4-mode"))
+ (code-c-d "lspmode" (ee-locate-library "lsp-mode"))
+;; (find-lean4modefile "")
+;; (find-lspmodefile "")
+
+;; (find-es "lean" "lean4-mode-vc")
+;; (find-es "lsp" "lsp-mode-git")
+
+(defun l () (interactive) (find-es "lean"))
+(defun a () (interactive) (mkdir "/tmp/L/" t) (find-fline "/tmp/L/a.lean"))
+
+;; See: (find-eev "eev-tlinks.el" "ee-copy-rest-3-intro")
+(defun cr3 () (interactive)
+ (insert "# (ee-copy-rest-3m nil \"-- end\" \"/tmp/L/a.lean\")\n\n-- end\n"))
+
+
+
+
+
+;;; _ _
+;;; | | ___| |___/\__ _ __ ___ __ _ ___ _ __ ___
+;;; | |/ _ \ __\ /_____| '_ ` _ \ / _` |/ __| '__/ _ \
+;;; | | __/ |_/_ _\_____| | | | | | (_| | (__| | | (_) |
+;;; |_|\___|\__| \/ |_| |_| |_|\__,_|\___|_| \___/
+;;;
+;; «ee-let*-macro-leandoc» (to ".ee-let*-macro-leandoc")
+;; See: (find-templates-intro "7. let* macros")
+;; Skel: (find-let*-macro-links "leandoc" "plist" "g kw kill baseweb gitrepo
gitname")
+;; Test: (ee-let*-macro-leandoc '(:usrc "~/bigsrc/") usrc)
+;;
+(defmacro ee-let*-macro-leandoc (pl &rest code)
+ "An internal function used by `find-leandoc-links'."
+ `(cl-letf*
+ ((pl ,pl)
+ (plist (if (symbolp pl) (symbol-value pl) pl))
+ ((symbol-function 'g) (lambda (field) (plist-get plist field)))
+ (kw (or (g :kw) "{kw}"))
+ (kill (or (g :kill) "{kill}"))
+ (k2 (or (g :k2) "{k2}"))
+ (base (or (g :base) "{base}"))
+ (baseweb (or (g :base-web) "{baseweb}"))
+ (rst (or (g :rst) ".rst"))
+ (usrc (or (g :usrc) "~/usrc/"))
+ (gitrepo (or (g :git-repo) "{gitrepo}"))
+ (gitsubdir (or (g :git-subdir) ""))
+ (username user-login-name)
+ (basewebl (ee-url-to-fname0 baseweb))
+ (baseweblu (format "file://%s" (ee-url-to-fname baseweb)))
+ (baseweb- (replace-regexp-in-string "https://"; "" baseweb))
+ (gitname (replace-regexp-in-string "^.*/\\([^/]*\\)/?$" "\\1"
gitrepo))
+ (gitdir (or (g :git-dir) (format "%s%s/" usrc gitname)))
+ (baserst (cond ((g :base-rst) (g :base-rst))
+ ((g :git-repo) (format "%s%s" gitdir gitsubdir))
+ (t "/BASE-RST/")))
+ (baserst- (replace-regexp-in-string "~/" "" baserst))
+ )
+ ,@code))
+
+
+
+;;; _ _ _ __
+;;; | | ___ __ _ _ __ __| | ___ ___ _ __ __| |/ _|
+;;; | |/ _ \/ _` | '_ \ / _` |/ _ \ / __| '_ \ / _` | |_
+;;; | | __/ (_| | | | | (_| | (_) | (__| |_) | (_| | _|
+;;; |_|\___|\__,_|_| |_|\__,_|\___/ \___| .__/ \__,_|_|
+;;; |_|
+;;
+;; «code-leandocpdf» (to ".code-leandocpdf")
+;; Skel: (find-code-xxx-links "leandocpdf" "pl" "")
+;; Test: (find-code-leandocpdf 'ee-leandoc-:lean4)
+;;
+(defun code-leandocpdf (pl)
+ (eval (ee-read (ee-code-leandocpdf pl))))
+(defun find-code-leandocpdf (pl)
+ (let ((ee-buffer-name
+ (or ee-buffer-name "*find-code-leandocpdf*")))
+ (find-estring-elisp (ee-code-leandocpdf pl))))
+(defun ee-code-leandocpdf (pl)
+ (ee-let*-macro-leandoc
+ pl
+ (ee-template0 "\
+;; (find-code-leandocpdf '{(ee-S pl)})
+;; (code-leandocpdf '{(ee-S pl)})
+;;
+;; The fields of this leandoc spec are (probably) here:
+;; (find-eev \"eev-lean4.el\" \"ee-leandoc-:{kw}\")
+;; The code that generates this temporary buffer is here:
+;; (find-eev \"eev-lean4.el\" \"code-leandocpdf\")
+
+;; Try: (find-{kw}doc \"{base}\")
+;; (find-{kw}docw \"{base}\")
+;; (find-{kw}docr \"{base}\")
+;; (find-{kw}docrfile \"\")
+;; (find-rstdoc-links :{kw})
+;; (find-code-rstdoc :{kw})
+;; (find-{kw}page)
+;; (find-{kw}text)
+
+;; The `setq' below creates a rstdoc spec from this leandoc spec.
+;; See: (find-rstdoc-intro)
+;;
+(setq ee-rstdoc-:{kw}
+ '(:base \"{base}\"
+ :base-web \"{baseweb}\"
+ :base-html \"file:///home/{username}/snarf/https/{baseweb-}\"
+ :base-rst \"{baserst}\"
+ :rst \"{rst}\"
+ :res (\"#.*$\" \"\\\\?.*$\"
+ \"\\\\.html$\" \"\\\\.txt$\" \"\\\\.rst$\" \"\\\\.md$\"
\"\\\\.lean$\"
+ \"^file://+\" \"^/\" \"^home/{username}/\" \"^~/\"
\"^snarf/\" \"^https:?/+\"
+ \"^{baseweb-}\"
+ \"^{baserst-}\")
+ :kill {kill}
+ ))
+
+;; Try: (find-code-rstdoc :{kw})
+ (code-rstdoc :{kw})
+
+(code-c-d \"{kw}doc\" \"{basewebl}\")
+;; (find-{kw}docfile \"\")
+;; (find-{kw}docfile \"\" \"print\")
+
+(code-c-d \"{kw}\" \"{gitdir}\")
+;; (find-{kw}file \"\")
+
+;; Try: (find-{kw}page)
+;; (find-{kw}text)
+(code-pdf-page \"{kw}\" \"{basewebl}print.pdf\")
+(code-pdf-text8 \"{kw}\" \"{basewebl}print.pdf\")
+
+;; Try: ({k2}l \"Copyright\")
+(defun {k2}l (&rest rest) (interactive)
+ (apply 'find-leanbook-links '{kw} rest))
+
+;; See: (find-leandocprep-links '{(ee-S pl)})
+
+")))
+
+
+;;; _ _
+;;; | | ___ __ _ _ __ __| | ___ ___ _ __ _ __ ___ _ __
+;;; | |/ _ \/ _` | '_ \ / _` |/ _ \ / __| '_ \| '__/ _ \ '_ \
+;;; | | __/ (_| | | | | (_| | (_) | (__| |_) | | | __/ |_) |
+;;; |_|\___|\__,_|_| |_|\__,_|\___/ \___| .__/|_| \___| .__/
+;;; |_| |_|
+;;
+;; «find-leandocprep-links» (to ".find-leandocprep-links")
+;; Skel: (find-find-links-links-new "leandocprep" "pl" "ee-buffer-name")
+;; Test: (find-leandocprep-links 'ee-leandoc-:lean4)
+;;
+(defun find-leandocprep-links (&optional pl &rest pos-spec-list)
+"Visit a temporary buffer containing a script for preparing the
+local files for the leandoc PL."
+ (interactive)
+ (setq pl (or pl "{pl}"))
+ (let* ((ee-buffer-name "*find-leandocprep-links*"))
+ (ee-let*-macro-leandoc
+ pl
+ (apply
+ 'find-elinks-elisp
+ `((find-leandocprep-links ',pl ,@pos-spec-list)
+ ;; Convention: the first sexp always regenerates the buffer.
+ (find-efunction 'find-leandocprep-links)
+ ""
+ ,(ee-template0 "\
+;; 1. Make sure that we have a local copy of the htmls:
+;; (find-fline \"{basewebl}\")
+;; (find-wgetrecursive-links \"{baseweb}\")
+
+
+;; 2. Produce the files `print.pdf' and `print.txt'.
+;;
+;; a) Do we already have the print.pdf and print.txt? Check:
+;; (find-fline \"{basewebl}\")
+;; (find-fline \"{basewebl}\" \"print\")
+;;
+;; b) If not, then use `M-x brg' on the url below, and
+;; make the browser print it to /tmp/print.pdf:
+;; (kill-new \"/tmp/print.pdf\")
+;; {baseweb}print.html
+;;
+;; c) Copy the `print.pdf' to the right place:
+;; (find-sh0 \"cp -v /tmp/print.pdf {basewebl}\")
+;;
+;; d) Generate the `print.txt':
+;; (find-{kw}docfile \"\")
+;; (find-{kw}docfile \"\" \"print\")
+;; (find-{kw}docsh \"pdftotext -layout print.pdf print.txt\")
+;; (find-{kw}docfile \"print.txt\")
+
+
+;; 3. I use this to adjust how blogme htmlizes `find-{kw}doc':
+;; (find-blogme3-rstdoc-links \"{kw}\")
+;; ^ This only works on my machine!
+")
+ )
+ pos-spec-list))))
+
+
+
+;;; _ _ _
+;;; | | ___ __ _ _ __ | |__ ___ ___ | | __
+;;; | |/ _ \/ _` | '_ \| '_ \ / _ \ / _ \| |/ /
+;;; | | __/ (_| | | | | |_) | (_) | (_) | <
+;;; |_|\___|\__,_|_| |_|_.__/ \___/ \___/|_|\_\
+;;;
+;; «find-leanbook-links» (to ".find-leanbook-links")
+;; Skel: (find-find-links-links-new "leanbook" "bk secname" "ee-buffer-name")
+;; Test: (find-leanbook-links 'leanmeta)
+;;
+(defun find-leanbook-links (&optional bk secname &rest pos-spec-list)
+"Visit a temporary buffer containing hyperlinks for leanbook."
+ (interactive)
+ (setq bk (or bk "{bk}"))
+ (setq secname (or secname "{secname}"))
+ (let* ((ee-buffer-name (format "*(find-leanbook-links '%s ...)*" bk)))
+ (apply
+ 'find-elinks
+ `((find-leanbook-links ',bk ,secname ,@pos-spec-list)
+ (fpl ,secname)
+ (ldl ,secname)
+ (lml ,secname)
+ (tcl ,secname)
+ (tpl ,secname)
+ ;; Convention: the first sexp always regenerates the buffer.
+ (find-efunction 'find-leanbook-links)
+ ""
+ ,(ee-template0 "\
+# (find-eev \"eev-lean4.el\" \"ee-leandoc-:{bk}\")
+# (find-{bk}doc)
+# (find-{bk}docw)
+# (find-{bk}docr)
+# (find-{bk}docrfile \"\")
+# (find-{bk}page)
+# (find-{bk}text)
+# (find-{bk}text 1 \"{secname}\")
+# (find-{bk}docfile \"\" \"print\")
+# (find-{bk}docfile \"print.txt\")
+# (find-{bk}docgrep \"grep --color=auto -nH --null -e '{secname}' print.txt\")
+
+")
+ )
+ pos-spec-list)))
+
+
+
+;; «find-leanrstdoc-links» (to ".find-leanrstdoc-links")
+;; Superseded by: (find-efunction 'find-code-leandocpdf)
+
+
+
+
+
+;;; _ _ _
+;;; | | ___ __ _ _ __ | |__ ___ ___ | | _____ __ _ ___
+;;; | | / _ \/ _` | '_ \ | '_ \ / _ \ / _ \| |/ / __| / _` / __|
+;;; | |__| __/ (_| | | | | | |_) | (_) | (_) | <\__ \_ | (_| \__ \
+;;; |_____\___|\__,_|_| |_| |_.__/ \___/ \___/|_|\_\___( ) \__,_|___/
+;;; _ _ |/
+;;; | | ___ __ _ _ __ __| | ___ ___ ___ _ __ ___ ___ ___
+;;; | |/ _ \/ _` | '_ \ / _` |/ _ \ / __| / __| '_ \ / _ \/ __/ __|
+;;; | | __/ (_| | | | | (_| | (_) | (__ \__ \ |_) | __/ (__\__ \
+;;; |_|\___|\__,_|_| |_|\__,_|\___/ \___| |___/ .__/ \___|\___|___/
+;;; |_|
+;; «books» (to ".books")
+;; «leandoc-specs» (to ".leandoc-specs")
+
+;; «ee-leandoc-:fplean4» (to ".ee-leandoc-:fplean4")
+;; "Functional Programming in Lean".
+;; Try: (find-fplean4doc "introduction")
+;; (find-fplean4docw "introduction")
+;; (find-fplean4docr "introduction")
+;; (find-fplean4docrfile "")
+;; (find-rstdoc-links :fplean4)
+;; (find-code-rstdoc :fplean4)
+;; (find-fplean4page)
+;; (find-fplean4text)
+(setq ee-leandoc-:fplean4
+ '(:kw "fplean4"
+ :kill "fpk"
+ :k2 "fp"
+ :rst ".md"
+ :base-web "https://lean-lang.org/functional_programming_in_lean/";
+ :git-repo "https://github.com/leanprover/fp-lean";
+ :git-subdir "functional-programming-lean/src/"
+ :base "introduction"
+ ))
+;; (find-code-leandocpdf 'ee-leandoc-:fplean4)
+ (code-leandocpdf 'ee-leandoc-:fplean4)
+
+;; «ee-leandoc-:lean4» (to ".ee-leandoc-:lean4")
+;; "Lean Manual".
+;; Try: (find-lean4doc "whatIsLean")
+;; (find-lean4docw "whatIsLean")
+;; (find-lean4docr "whatIsLean.md")
+;; (find-lean4docrfile "")
+;; (find-rstdoc-links :lean4)
+;; (find-code-rstdoc :lean4)
+;; (find-lean4page)
+;; (find-lean4text)
+(setq ee-leandoc-:lean4
+ '(:kw "lean4"
+ :kill "ldk"
+ :k2 "ld"
+ :base-web "https://lean-lang.org/lean4/doc/";
+ :git-repo "https://github.com/leanprover/lean4";
+ :usrc "~/bigsrc/"
+ :base-rst "~/bigsrc/lean4/doc/"
+ :base "whatIsLean"
+ :rst ""
+ ))
+;; (find-code-leandocpdf 'ee-leandoc-:lean4)
+ (code-leandocpdf 'ee-leandoc-:lean4)
+
+;; «ee-leandoc-:leanmeta» (to ".ee-leandoc-:leanmeta")
+;; "Metaprogramming in Lean 4".
+;; Try: (find-leanmetadoc "main/01_intro")
+;; (find-leanmetadocw "main/01_intro")
+;; (find-leanmetadocr "main/01_intro")
+;; (find-leanmetadocrfile "")
+;; (find-rstdoc-links :leanmeta)
+;; (find-code-rstdoc :leanmeta)
+;; (find-leanmetapage)
+;; (find-leanmetatext)
+(setq ee-leandoc-:leanmeta
+ '(:kw "leanmeta"
+ :kill "lmk"
+ :k2 "lm"
+ :rst ".lean"
+ :base-web
"https://leanprover-community.github.io/lean4-metaprogramming-book/";
+ :git-repo
"https://github.com/leanprover-community/lean4-metaprogramming-book";
+ :git-subdir "lean/"
+ :base "main/01_intro"
+ ))
+;; (find-code-leandocpdf 'ee-leandoc-:leanmeta)
+ (code-leandocpdf 'ee-leandoc-:leanmeta)
+
+;; «ee-leandoc-:tclean4» (to ".ee-leandoc-:tclean4")
+;; "Type Checking in Lean 4".
+;; Try: (find-tclean4doc "title_page")
+;; (find-tclean4docw "title_page")
+;; (find-tclean4docr "title_page")
+;; (find-tclean4docrfile "")
+;; (find-rstdoc-links :tclean4)
+;; (find-code-rstdoc :tclean4)
+;; (find-tclean4page)
+;; (find-tclean4text)
+(setq ee-leandoc-:tclean4
+ '(:kw "tclean4"
+ :kill "tck"
+ :k2 "tc"
+ :rst ".md"
+ :base-web "https://ammkrn.github.io/type_checking_in_lean4/";
+ :git-repo "https://github.com/ammkrn/type_checking_in_lean4";
+ :git-subdir "src/"
+ :base "title_page"
+ ))
+;; (find-code-leandocpdf 'ee-leandoc-:tclean4)
+ (code-leandocpdf 'ee-leandoc-:tclean4)
+;;
+;; (find-2a nil '(find-leanrstdoc-links 'ee-leandoc-:tclean4))
+
+
+;; «ee-leandoc-:tpil4» (to ".ee-leandoc-:tpil4")
+;; "Theorem Proving in Lean 4".
+;; Try: (find-tpil4doc "introduction")
+;; (find-tpil4docw "introduction")
+;; (find-tpil4docr "introduction")
+;; (find-tpil4docrfile "")
+;; (find-rstdoc-links :tpil4)
+;; (find-code-rstdoc :tpil4)
+;; (find-tpil4page)
+;; (find-tpil4text)
+(setq ee-leandoc-:tpil4
+ '(:kw "tpil4"
+ :kill "tpk"
+ :k2 "tp"
+ :rst ".md"
+ :base-web "https://lean-lang.org/theorem_proving_in_lean4/";
+ :git-repo "https://github.com/leanprover/theorem_proving_in_lean4";
+ :git-subdir ""
+ :base "introduction"
+ ))
+;; (find-code-leandocpdf 'ee-leandoc-:tpil4)
+ (code-leandocpdf 'ee-leandoc-:tpil4)
+
+
+
+
+
+
+
+
+
+
+(provide 'eev-lean4)
+
+;; Local Variables:
+;; coding: utf-8-unix
+;; no-byte-compile: t
+;; End:
| [Prev in Thread] |
Current Thread |
[Next in Thread] |
- [elpa] externals/eev 0d6ae77866: Added `ee-symbol-function'; added eev-lean4.el.,
ELPA Syncer <=