|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
;;; eev-lean4.el -- ???. -*- 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: 20240619
;; 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:
;;
;; Index:
;; «.ee-let*-macro-leandoc» (to "ee-let*-macro-leandoc")
;; «.code-leandocpdf» (to "code-leandocpdf")
;; «.ee-leandoc-:fplean4» (to "ee-leandoc-:fplean4")
;; «.ee-leandoc-:lean4» (to "ee-leandoc-:lean4")
;; «.ee-leandoc-:leanmeta» (to "ee-leandoc-:leanmeta")
;; «.ee-leandoc-:tpil4» (to "ee-leandoc-:tpil4")
;; «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}"))
(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) ""))
(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)})
;; Try: (find-{kw}doc \"{base}\")
;; (find-{kw}docw \"{base}\")
;; (find-{kw}docr \"{base}\")
;; (find-{kw}docrfile \"\")
;; (find-rstdoc-links :{kw})
;;
(setq ee-rstdoc-:{kw}
'(:base \"{base}\"
:base-web \"{baseweb}\"
:base-html \"file:///home/edrx/snarf/https/{baseweb-}\"
:base-rst \"{baserst}\"
:rst \"{rst}\"
:res (\"#.*$\" \"\\\\?.*$\"
\"\\\\.html$\" \"\\\\.txt$\" \"\\\\.rst$\" \"\\\\.md$\" \"\\\\.lean$\"
\"^file://+\" \"^/\" \"^home/edrx/\" \"^~/\" \"^snarf/\" \"^https:?/+\"
\"^{baseweb-}\"
\"^{baserst-}\")
:kill {kill}
))
;; Try: (find-code-rstdoc :{kw})
(code-rstdoc :{kw})
;; Try: (find-{kw}page)
;; (find-{kw}text)
(code-pdf-page \"{kw}\" \"{basewebl}print.pdf\")
(code-pdf-text8 \"{kw}\" \"{basewebl}print.pdf\")
;; 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)
")))
;; «ee-leandoc-:fplean4» (to ".ee-leandoc-:fplean4")
;; 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"
: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")
;; 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"
: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")
;; 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"
: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-:tpil4» (to ".ee-leandoc-:tpil4")
;; 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"
: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: