Oi gente, eu tou gravando esse vídeo assim
meio emergencialmente pra aula 2 da
oficina de Lean, que vai ser uma aula
estranhíssima, porque muito poucas pessoas
pessoas vão conseguir estar nela no horário...
então a gente vai tentar fazer
algumas coisas desse vídeo, e parece que
algumas pessoas vão tentar fazer as coisas
dele depois. Então, lembrem que se eu
executo essa expressão daqui
no meu computador ela vai para meu
arquivo de anotações sobre Lean,
mas no computador de vocês ela tá
configurada para baixar uma cópia da
versão pública desse arquivo, não gravar
ela em lugar nenhum, e mostrar ela
num buffer temporário. O material da aula 2
tá nessa seção daqui, "oficina 0, aula 2"
e aí eu usei como referência
alguns trechos das legendas
pra lembrar exatamente o que que eu
tinha planejado para as aulas 1 e 2.
Eu ainda não gravei o vídeo do
exercício grande da aula de hoje, que é fazer
algumas demonstrações não triviais.
eu acho que vocês já viram
links que terminam com "hsubs", eles
vão pra versão em HTML das legendas
de um vídeo, e o lsubs é uma coisa que é
mais útil para mim, que vai pra fonte em
Lua dessas legendas que depois eu
converto para montão de outros formatos...
e para mim a graça disso é que isso abre
dentro do Emacs.
Então, deixa eu só lembrar para vocês que
todo esse curso é feito para pessoas com
pouquíssima memória, com um buffer mental
pequenininho que nem o meu, então eu
vou sempre mostrar como é que a gente
faz para lembrar o mínimo e reconstruir
o resto a partir do pouquinho que a
gente lembrou.
Então o primeiro bloco que a gente vai ver
hoje é o seguinte... eu preciso confirmar
que todo mundo sabe duas teclas básicas,
que eu chamo de "go to" e "go back"...
os nomes oficiais delas são mais complicados.
Então a gente vai para esse bloco daqui,
sobre go to e go back, e elas estão
mencionadas em dois trechos do vídeo
sobre a oficina - o vídeo de divulgação,
aquele de, sei lá, 30 minutos ou algo assim,
que eu fiz.
O primeiro trecho é esse,
e talvez vocês precisem ver esse trecho
de novo para lembrar como essas teclas
funcionam...
e no (find-lean4-intro), que tem as instruções
pra instalar o Lean e as instruções muito
básicas de como testar ele, a seção 3
se chama "Test the five manuals", e no
final dela tem um manual que tá num
formato muito antigo, que foi gerado com
com ferramentas que as pessoas não tão
mais usando, que é o "Lean Reference", e
algumas teclas que a gente vai usar
estão explicadas aqui, nesse link daqui, ó,
nessa URL.
Então, voltando... isso aqui
aponta para esse trechinho onde estão os
links pro Lean Reference,
e esses dois links não vão funcionar no
no computador de vocês...
a seção que nos interessa é essa
daqui, então se vocês quiserem ler a
documentação original sigam esse link
daqui, e ele vai explicar um montão de
coisas interessantes e um montão de
coisas que não nos interessam...
e se vocês avançarem alguns
parágrafos vocês vão ver que ele fala
sobre o `M-.' e o `M-,', que
são o go to e o go back. Então, deixa eu
voltar para cá...
como é que a gente faz para descobrir
o que que essas teclas fazem?
É o seguinte. Essas teclas são
teclas globais que estão
definidas em todos os modos do Emacs,
e no tutorial principal do eev, que é
esse daqui, a seção 4, ela...
peraí, deixa eu lembrar se é a seção 4...
Sim. Ela explica um jeito de gerar
muitos hiperlinks sobre uma determinada
função ou sobre uma determinada tecla.
Ela começa dizendo que se você executar
essa expressão daqui você vai pra um
buffer temporário com montão de links
sobre o find-file... mas uma coisa que é
super importante é esse link daqui.
Se você lembrar essa sequência de
teclas daqui você consegue help sobre
qualquer função, nesse formato daqui...
Então, se eu bater M-h M-f em cima
do nome dessa função, find-file, ele vai
pedir pra eu confirmar que eu quero
help sobre essa função daqui, se eu
confirmar eu vou para um buffer que
coincidentemente era exatamente o que eu
já tinha gerado, e se eu rodar essa
expressão daqui eu vou pro help
tradicional sobre o find-file, que tem
hiperlinks no sentido tradicional,
que você clica neles e coisas assim, mas
que você não consegue ver o
código fonte deles.
Às vezes a gente vai querer seguir esse
hiperlink daqui, `find-efunction', que
vai pro código fonte do find-file, e em
alguns casos... daqui a pouco eu vou
mostrar casos assim. Então, deixa eu
voltar...
então: M-h M-f vai pra links sobre uma função
e M-h M-k vai pra links sobre uma tecla...
então se eu quiser mais informações sobre
o `M-.' e o `M-', que são go to e go back,
eu posso rodar essas expressões daqui...
lembrem que o eek
é um hiperlink pra ação de uma
sequência de teclas,
então ele faz a mesma coisa que
se eu batesse isso aqui na mão, e isso aqui
é um bom modo da gente lembrar uma
sequência de teclas que a gente quer
usar depois... e ele trata isso aqui como
um comentário, e esse comentário tem o
nome da função. Então se eu executar isso
aqui eu consigo um bocado de help sobre
essa função daqui, e se eu por acaso
quiser ver o código fonte eu posso ir ou
pra cá, que tem o o comentário de como é
que ela funciona - o "docstring" dela -
ou pra cá...
e aí eu vou pro arquivo onde ela tá
definida, que é um arquivo grandão
chamado xref.el, etc...
Deixa eu seguir esse link daqui.
Lembrem que no tutorial... quer dizer, no
intro sobre Lean4, a seção 8 pedia pra
vocês testarem isso daqui...
eu vou ter que reduzir a fonte...
e esse link daqui vai
pro código fonte do Lean... de um dos
arquivos da biblioteca básica do Lean...
o nome, `find-lean4prefile', não é muito bom...
eu tô chamando esses links de "preamble"
baseado em como as coisas são
no Haskell, em que as bibliotecas
básicas se chamam "Preamble", mas no Lean
isso tá meio errado... mas eu mantive
o nome errado por motivos históricos -
eu não tive tempo de consertar isso.
Então, se eu seguir esse link daqui
ele vai para um arquivo em Lean...
e Lean leva um tempinho para processar
esse arquivo, pra conseguir criar
links em alguns pontos dele e
coisas assim... e aqui eu posso testar
o `M-.', que é o "go to", e o `M-,',
que é o "go back"... então, por exemplo,
se eu quiser saber mais sobre a classe
Inhabited eu uso a tecla de "go to" aqui,
que é `M-.', e ele vai pra um
outro arquivo...
e se eu bater M-, eu volto para cá.
Então testem isso, tá...
isso é uma das primeiras coisas que eu
quero que vocês testem.
Agora o segundo bloquinho.
Eu não sei se vocês lembram disso, mas se
a gente bater `M-x l' a gente vai pra
esse arquivo de anotações de Lean.
Então nesse momento se eu bater `M-x l' isso
não faz nada porque eu já tou nesse arquivo.
No computador de vocês o Emacs vai pra
uma cópia temporária desse arquivo,
no meu ele vai pro arquivo em si...
Aqui tem um link que tá errado, caramba...
eu devia ter posto isso num outro bloco...
ah, não, não - tá certo.
Então, eu contei para vocês que `M-x l'
vem para cá, e eu não lembro se vocês
já testaram o `M-x a', que também faz
uma coisa parecida...
Então, agora há pouco a gente tava
vendo o `M-h M-k', que vai pro help
sobre uma tecla - `k' é de `key'...
e agora a gente vai ver `M-h M-f',
que vai pro help sobre uma função.
Aqui a gente tem uma função com um nome
muito curto - `l'. Como é que a gente
consegue mais informação sobre ela?
A gente pode bater `M-h M-h l ENTER',
E aí ele abre esse buffer aqui,
com montão de links sobre a função `l',
ou a gente pode seguir isso aqui,
que é um link pro efeito de bater
`M-h M-f l'...
E aí nesse caso isso é uma função que
não tem uma descrição - ela não tá
documentada... então é melhor a gente ir
para cá e ver o código fonte dela. Ela é
uma função muito curta, ó - é uma função
que tem uma linha só, é isso aqui...
e ela vai pro arquivo de anotações sobre Lean.
a mesma coisa pro a - e um dos links aqui
vai pro código fonte dela - é esse...
e o `a' ele garante que esse
diretório existe - /tmp/L/ -
e ele abre o arquivo /tmp/L/a.lean.
Tá? Isso vai ser importante depois.
Nesse momento o a.lean... bom, eu
tou usando esse a.lean como um arquivo
temporário, e aqui tem umas coisas que eu
botei nele agora há pouco, num dos testes.
Outra coisa que pode ser útil para
algumas pessoas é a seguinte... algumas
pessoas vão precisar definir sequências
novas de teclas - o Halian precisou
disso porque o F8 pra ele já tava
definido de um outro jeito...
nas minhas anotações sobre MacOS, OSX,
ou whatever, como as pessoas queiram chamar...
tem uma seção sobre o arquivo de
configuração que eu criei pro Halian - que
a gente criou juntos... e tem esse
trechinho no arquivo de anotações dele...
ele precisou definir o `C-RET',
`C-Return', como a função que tava
associada ao F8...
Então esse comando daqui define
que o `C-Return' faz isso aqui,
e essa linha daqui foi gerada
por essa linha daqui, find-esetkey-links,
que gera esse buffer temporário...
E eu escolhi mandar isso aqui pro Halian.