|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2025adapting-lean-tuts.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2025adapting-lean-tuts.tex" :end))
% (defun C () (interactive) (find-LATEXsh "lualatex 2025adapting-lean-tuts.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2025adapting-lean-tuts.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2025adapting-lean-tuts.pdf"))
% (defun e () (interactive) (find-LATEX "2025adapting-lean-tuts.tex"))
% (defun o () (interactive) (find-LATEX "2022ebl.tex"))
% (defun u () (interactive) (find-latex-upload-links "2025adapting-lean-tuts"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun d0 () (interactive) (find-ebuffer "2025adapting-lean-tuts.pdf"))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun oe () (interactive) (find-2a '(o) '(e)))
% (code-eec-LATEX "2025adapting-lean-tuts")
% (find-pdf-page "~/LATEX/2025adapting-lean-tuts.pdf")
% (find-sh0 "cp -v ~/LATEX/2025adapting-lean-tuts.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2025adapting-lean-tuts.pdf /tmp/pen/")
% (find-xournalpp "/tmp/2025adapting-lean-tuts.pdf")
% file:///home/edrx/LATEX/2025adapting-lean-tuts.pdf
% file:///tmp/2025adapting-lean-tuts.pdf
% file:///tmp/pen/2025adapting-lean-tuts.pdf
% http://anggtwu.net/LATEX/2025adapting-lean-tuts.pdf
% (find-LATEX "2019.mk")
% (find-Deps1-links "Caepro5 Piecewise2 Maxima2")
% (find-Deps1-cps "Caepro5 Piecewise2 Maxima2")
% (find-Deps1-anggs "Caepro5 Piecewise2 Maxima2")
% (find-MM-aula-links "2025adapting-lean-tuts" "2" "adab" "adab")
% «.defs» (to "defs")
% «.defs-T-and-B» (to "defs-T-and-B")
% «.defs-caepro» (to "defs-caepro")
% «.defs-pict2e» (to "defs-pict2e")
% «.defs-maxima» (to "defs-maxima")
% «.defs-V» (to "defs-V")
% «.title» (to "title")
% «.links» (to "links")
% «.abstract» (to "abstract")
% «.bibliography» (to "bibliography")
\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
\usepackage{colorweb} % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (find-LATEX "dednat7-test1.tex")
%\usepackage{proof} % For derivation trees ("%:" lines)
%\input diagxy % For 2D diagrams ("%D" lines)
%\xyoption{curve} % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx21} % (find-LATEX "edrx21.sty")
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrx21chars.tex % (find-LATEX "edrx21chars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
\usepackage{cite}
%
% (find-es "tex" "geometry")
\usepackage[a6paper, landscape,
top=1.5cm, bottom=.25cm, left=1cm, right=1cm, includefoot
]{geometry}
%
\begin{document}
% «defs» (to ".defs")
% (find-LATEX "edrx21defs.tex" "colors")
% (find-LATEX "edrx21.sty")
\def\drafturl{http://anggtwu.net/LATEX/2025-1-C2.pdf}
\def\drafturl{http://anggtwu.net/2025.1-C2.html}
\def\draftfooter{\tiny \href{\drafturl}{\jobname{}} \ColorBrown{\shorttoday{} \hours}}
% (find-LATEX "2024-1-C2-carro.tex" "defs-caepro")
% (find-LATEX "2024-1-C2-carro.tex" "defs-pict2e")
\catcode`\^^J=10
\directlua{dofile "dednat7load.lua"} % (find-LATEX "dednat7load.lua")
\directlua{dednat7preamble()} % (find-angg "LUA/DednatPreamble1.lua")
\directlua{dednat7oldheads()} % (find-angg "LUA/Dednat7oldheads.lua")
% «defs-T-and-B» (to ".defs-T-and-B")
\long\def\ColorDarkOrange#1{{\color{orange!90!black}#1}}
\def\T(Total: #1 pts){{\bf(Total: #1)}}
\def\T(Total: #1 pts){{\bf(Total: #1 pts)}}
\def\T(Total: #1 pts){\ColorRed{\bf(Total: #1 pts)}}
\def\B (#1 pts){\ColorDarkOrange{\bf(#1 pts)}}
% «defs-caepro» (to ".defs-caepro")
%L dofile "Caepro5.lua" -- (find-angg "LUA/Caepro5.lua" "LaTeX")
\def\Caurl #1{\expr{Caurl("#1")}}
\def\Cahref#1#2{\href{\Caurl{#1}}{#2}}
\def\Ca #1{\Cahref{#1}{#1}}
% «defs-pict2e» (to ".defs-pict2e")
%L dofile "Piecewise2.lua" -- (find-LATEX "Piecewise2.lua")
%L --dofile "Escadas1.lua" -- (find-LATEX "Escadas1.lua")
\def\pictgridstyle{\color{GrayPale}\linethickness{0.3pt}}
\def\pictaxesstyle{\linethickness{0.5pt}}
\def\pictnaxesstyle{\color{GrayPale}\linethickness{0.5pt}}
\celllower=2.5pt
% «defs-maxima» (to ".defs-maxima")
%L dofile "Maxima2.lua" -- (find-angg "LUA/Maxima2.lua")
\pu
% «defs-V» (to ".defs-V")
%L --- See: (find-angg "LUA/MiniV1.lua" "problem-with-V")
%L V = MiniV
%L v = V.fromab
\pu
% _____ _ _ _
% |_ _(_) |_| | ___ _ __ __ _ __ _ ___
% | | | | __| |/ _ \ | '_ \ / _` |/ _` |/ _ \
% | | | | |_| | __/ | |_) | (_| | (_| | __/
% |_| |_|\__|_|\___| | .__/ \__,_|\__, |\___|
% |_| |___/
%
% «title» (to ".title")
% (adabp 1 "title")
% (adaba "title")
\thispagestyle{empty}
\begin{center}
\vspace*{0.5cm}
\begin{tabular}{c}
\phantom{a}\\[-15pt]
{\Large {\bf Adapting Lean Tutorials}} \\[1pt]
{\Large {\bf to the Brazilian Case}} \\[1pt]
\\[-9pt]
\ColorGray{(talk @ XXI EBL)}\\[-5pt]
\\[-9pt]
{\tiny\url{http://anggtwu.net/math-b.html#2025-ebl}}\\[8pt]
Eduardo Ochs \\
Serra Negra, 2022may13 \\
\end{tabular}
\end{center}
\newpage
% «links» (to ".links")
% (adabp 2 "links")
% (adaba "links")
{\bf Links}
\scalebox{0.6}{\def\colwidth{16cm}\firstcol{
}\anothercol{
}}
\newpage
% «abstract» (to ".abstract")
% (find-angg "EBL2025/Submission-Template-EN.tex")
{\bf Abstract}
\def\cite #1{\CFname{#1}{}}
\def\bibitem#1{\CFname{#1}{}}
\scalebox{0.5}{\def\colwidth{16cm}\firstcol{
Lean4 (\cite{Overview}) is a proof assistant that is also a
general-purpose language, and that has ``metaprogramming facilities''
(\cite{Meta}) that let people extend its syntax in many ways. It is
becoming very popular, and the page \cite{Courses} has links to more
than 40 courses on Lean, or using Lean.
\msk
{\sl I don't think that these courses are adequate for Brazilians.}
They all start from some point like ``everybody knows VSCode'' and
they move to non-trivial ideas very quickly. But ``everybody knows the
programs such and such'' is not true in Brazil at all; half of the
Brazilian logicians that I know only use computers in a very basic
way, and here ``knowledge about programs does not propagate'' (see
\cite{EmacsConf2024}).
\msk
In this presentation I will show how I adapted the approach in
\cite{EmacsConf2024} -- that I use to teach Maxima to undergraduate
students with {\sl very} little experience with computers -- to create
a short workshop on Lean (\cite{Oficina0}) that teaches people how to
install Lean4, how to navigate its manuals, how to understand its
interface, and how to run and modify simplified versions of some
examples from the main books on Lean.
\bsk
\par \bibitem{Overview} {\em Lean Documentation Overview}:
\par \url{https://lean-lang.org/lean4/doc/}.
\ssk
\par \bibitem{Meta} {\em Metaprogramming in Lean4}:
\par \url{https://leanprover-community.github.io/lean4-metaprogramming-book/}
\ssk
\par \bibitem{Courses} {\em Courses using Lean}:
\par \url{https://leanprover-community.github.io/teaching/courses.html}
\ssk
\par \bibitem{EmacsConf2024} {\em Emacs, eev, and Maxima -- Now!}:
\par \url{http://anggtwu.net/emacsconf2024.html}.
\ssk
\par \bibitem{Oficina0} {\em Oficina de Lean4 -- versão 0}:
\par \url{http://anggtwu.net/2024-lean4-oficina-0.html}.
}\anothercol{
}}
\newpage
% «bibliography» (to ".bibliography")
\GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
\end{document}
% (find-pdfpages2-links "~/LATEX/" "2025adapting-lean-tuts")
% Local Variables:
% coding: utf-8-unix
% ee-tla: "adab"
% ee-tla: "adab"
% End: