Quick
index
main
eev
eepitch
maths
angg
blogme
dednat6
littlelangs
PURO
(C2,C3,C4,
 λ,ES,
 GA,MD,
 Caepro,
 textos,
 Chapa 1)
emacs
lua
(la)tex
maxima
git
lean4
agda
forth
squeak
icon
tcl
tikz
fvwm
debian
irc
contact
☿

Oficina de Lean4 - versão 0 - material pra aula 1

Página da oficina: link.
Esta é uma página bagunçada só com material pra aula 1.

1. Coisas básicas

(find-windows-beginner-intro)
http://anggtwu.net/2024-first-executable-notes.html
http://anggtwu.net/2024-find-dot-emacs-links.html
(find-lean4-intro)


2. Eev from git

Parece que o ELPA não vai atualizar a versão do eev pra de ontem (2024jul25) antes da oficina... e aí algumas coisas do último terço da aula de hoje vão precisar que a gente use a versão do eev que está no repositório git ao invés da versão do ELPA.

;; (ee-copy-rest-3 nil ";;--end" "~/.emacs")
;; Use eev from git. THIS IS A HACK!
;; Adapted from: (find-dot-emacs-links "eev")
;; And: (find-package-vc-install-links "https://github.com/edrx/eev")
(add-to-list 'load-path "/home/edrx/.emacs.d/elpa/eev")

;; See: (find-eev-levels-intro)
(require 'eev-load)               ; (find-eev "eev-load.el")
(require 'eev-aliases)            ; (find-eev "eev-aliases.el")
(eev-mode 1)                      ; (find-eev "eev-mode.el")
;;--end

•• From: (find-epackage-links 'eev "eev" t)
• (package-initialize)
• (package-refresh-contents)
• (package-delete (ee-package-desc 'eev))
•
•• From: (find-package-vc-install-links "https://github.com/edrx/eev")
• (eepitch-shell)
• (eepitch-kill)
• (eepitch-shell)
rm -Rfv  /home/edrx/.emacs.d/elpa/eev
mkdir -p /home/edrx/.emacs.d/elpa/eev
cd       /home/edrx/.emacs.d/elpa/eev
git clone https://github.com/edrx/eev .