Oficina de Lean4 - versão 0 - aula 2 (legendas muito incompletas)

00:00

00:01 Oi gente, eu tou gravando esse vídeo assim
00:03 meio emergencialmente pra aula 2 da
00:05 oficina de Lean, que vai ser uma aula
00:07 estranhíssima, porque muito poucas pessoas
00:09 pessoas vão conseguir estar nela no horário...

00:10 então a gente vai tentar fazer
00:12 algumas coisas desse vídeo, e parece que
00:14 algumas pessoas vão tentar fazer as coisas
00:16 dele depois. Então, lembrem que se eu
00:20 executo essa expressão daqui
00:22 no meu computador ela vai para meu
00:24 arquivo de anotações sobre Lean,
00:27 mas no computador de vocês ela tá
00:29 configurada para baixar uma cópia da
00:33 versão pública desse arquivo, não gravar
00:36 ela em lugar nenhum, e mostrar ela
00:38 num buffer temporário. O material da aula 2
00:41 tá nessa seção daqui, "oficina 0, aula 2"
00:45 e aí eu usei como referência
00:49 alguns trechos das legendas
00:52 pra lembrar exatamente o que que eu
00:54 tinha planejado para as aulas 1 e 2.

00:56 Eu ainda não gravei o vídeo do
00:58 exercício grande da aula de hoje, que é fazer
01:00 algumas demonstrações não triviais.

01:04 eu acho que vocês já viram
01:07 links que terminam com "hsubs", eles
01:09 vão pra versão em HTML das legendas
01:13 de um vídeo, e o lsubs é uma coisa que é
01:16 mais útil para mim, que vai pra fonte em
01:18 Lua dessas legendas que depois eu
01:19 converto para montão de outros formatos...

01:21 e para mim a graça disso é que isso abre
01:23 dentro do Emacs.
01:28 Então, deixa eu só lembrar para vocês que
01:32 todo esse curso é feito para pessoas com
01:34 pouquíssima memória, com um buffer mental
01:36 pequenininho que nem o meu, então eu
01:39 vou sempre mostrar como é que a gente
01:41 faz para lembrar o mínimo e reconstruir
01:43 o resto a partir do pouquinho que a
01:44 gente lembrou.

01:46 Então o primeiro bloco que a gente vai ver
01:48 hoje é o seguinte... eu preciso confirmar
01:51 que todo mundo sabe duas teclas básicas,
01:53 que eu chamo de "go to" e "go back"...
01:55 os nomes oficiais delas são mais complicados.

01:58 Então a gente vai para esse bloco daqui,
02:01 sobre go to e go back, e elas estão
02:04 mencionadas em dois trechos do vídeo
02:07 sobre a oficina - o vídeo de divulgação,
02:09 aquele de, sei lá, 30 minutos ou algo assim,
02:12 que eu fiz.

02:16 O primeiro trecho é esse,
02:19 e talvez vocês precisem ver esse trecho
02:22 de novo para lembrar como essas teclas
02:24 funcionam...

02:28 e no (find-lean4-intro), que tem as instruções
02:31 pra instalar o Lean e as instruções muito
02:33 básicas de como testar ele, a seção 3
02:36 se chama "Test the five manuals", e no
02:40 final dela tem um manual que tá num
02:42 formato muito antigo, que foi gerado com
02:44 com ferramentas que as pessoas não tão
02:48 mais usando, que é o "Lean Reference", e
02:52 algumas teclas que a gente vai usar
02:53 estão explicadas aqui, nesse link daqui, ó,
02:56 nessa URL.

02:58 Então, voltando... isso aqui
03:02 aponta para esse trechinho onde estão os
03:03 links pro Lean Reference,
03:06 e esses dois links não vão funcionar no
03:09 no computador de vocês...

03:11 a seção que nos interessa é essa
03:15 daqui, então se vocês quiserem ler a
03:17 documentação original sigam esse link
03:20 daqui, e ele vai explicar um montão de
03:21 coisas interessantes e um montão de
03:22 coisas que não nos interessam...

03:24 e se vocês avançarem alguns
03:28 parágrafos vocês vão ver que ele fala
03:30 sobre o `M-.' e o `M-,', que
03:33 são o go to e o go back. Então, deixa eu
03:37 voltar para cá...

03:39 como é que a gente faz para descobrir
03:41 o que que essas teclas fazem?

03:43 É o seguinte. Essas teclas são
03:47 teclas globais que estão
03:48 definidas em todos os modos do Emacs,
03:53 e no tutorial principal do eev, que é
03:57 esse daqui, a seção 4, ela...
04:02 peraí, deixa eu lembrar se é a seção 4...

04:10 Sim. Ela explica um jeito de gerar
04:12 muitos hiperlinks sobre uma determinada
04:15 função ou sobre uma determinada tecla.
04:17 Ela começa dizendo que se você executar
04:19 essa expressão daqui você vai pra um
04:21 buffer temporário com montão de links
04:23 sobre o find-file... mas uma coisa que é
04:26 super importante é esse link daqui.
04:26 Se você lembrar essa sequência de
04:30 teclas daqui você consegue help sobre
04:32 qualquer função, nesse formato daqui...

04:34 Então, se eu bater M-h M-f em cima
04:39 do nome dessa função, find-file, ele vai
04:41 pedir pra eu confirmar que eu quero
04:44 help sobre essa função daqui, se eu
04:46 confirmar eu vou para um buffer que
04:47 coincidentemente era exatamente o que eu
04:49 já tinha gerado, e se eu rodar essa
04:53 expressão daqui eu vou pro help
04:56 tradicional sobre o find-file, que tem
04:58 hiperlinks no sentido tradicional,
05:01 que você clica neles e coisas assim, mas
05:03 que você não consegue ver o
05:04 código fonte deles.

05:05 Às vezes a gente vai querer seguir esse
05:07 hiperlink daqui, `find-efunction', que
05:10 vai pro código fonte do find-file, e em
05:13 alguns casos... daqui a pouco eu vou
05:14 mostrar casos assim. Então, deixa eu
05:17 voltar...

05:19 então: M-h M-f vai pra links sobre uma função
05:23 e M-h M-k vai pra links sobre uma tecla...
05:26 então se eu quiser mais informações sobre
05:31 o `M-.' e o `M-', que são go to e go back,
05:34 eu posso rodar essas expressões daqui...
05:38 lembrem que o eek
05:42 é um hiperlink pra ação de uma
05:44 sequência de teclas,
05:45 então ele faz a mesma coisa que
05:47 se eu batesse isso aqui na mão, e isso aqui
05:49 é um bom modo da gente lembrar uma
05:51 sequência de teclas que a gente quer
05:52 usar depois... e ele trata isso aqui como
05:55 um comentário, e esse comentário tem o
05:57 nome da função. Então se eu executar isso
05:59 aqui eu consigo um bocado de help sobre
06:01 essa função daqui, e se eu por acaso
06:04 quiser ver o código fonte eu posso ir ou
06:07 pra cá, que tem o o comentário de como é
06:09 que ela funciona - o "docstring" dela -
06:13 ou pra cá...

06:14 e aí eu vou pro arquivo onde ela tá
06:17 definida, que é um arquivo grandão
06:19 chamado xref.el, etc...

06:26 Deixa eu seguir esse link daqui.
06:30 Lembrem que no tutorial... quer dizer, no
06:33 intro sobre Lean4, a seção 8 pedia pra
06:36 vocês testarem isso daqui...

06:38 eu vou ter que reduzir a fonte...

06:39 e esse link daqui vai
06:41 pro código fonte do Lean... de um dos
06:45 arquivos da biblioteca básica do Lean...

06:47 o nome, `find-lean4prefile', não é muito bom...
06:50 eu tô chamando esses links de "preamble"
06:55 baseado em como as coisas são
06:57 no Haskell, em que as bibliotecas
06:59 básicas se chamam "Preamble", mas no Lean
07:01 isso tá meio errado... mas eu mantive
07:03 o nome errado por motivos históricos -
07:06 eu não tive tempo de consertar isso.

07:08 Então, se eu seguir esse link daqui
07:10 ele vai para um arquivo em Lean...
07:15 e Lean leva um tempinho para processar
07:18 esse arquivo, pra conseguir criar
07:22 links em alguns pontos dele e
07:25 coisas assim... e aqui eu posso testar
07:27 o `M-.', que é o "go to", e o `M-,',
07:32 que é o "go back"... então, por exemplo,
07:34 se eu quiser saber mais sobre a classe
07:36 Inhabited eu uso a tecla de "go to" aqui,
07:39 que é `M-.', e ele vai pra um
07:42 outro arquivo...

07:44 e se eu bater M-, eu volto para cá.

07:47 Então testem isso, tá...
07:49 isso é uma das primeiras coisas que eu
07:51 quero que vocês testem.

07:55 Agora o segundo bloquinho.

08:00 Eu não sei se vocês lembram disso, mas se
08:02 a gente bater `M-x l' a gente vai pra
08:05 esse arquivo de anotações de Lean.

08:07 Então nesse momento se eu bater `M-x l' isso
08:09 não faz nada porque eu já tou nesse arquivo.

08:11 No computador de vocês o Emacs vai pra
08:13 uma cópia temporária desse arquivo,
08:17 no meu ele vai pro arquivo em si...

08:25 Aqui tem um link que tá errado, caramba...
08:28 eu devia ter posto isso num outro bloco...
08:32 ah, não, não - tá certo.

08:34 Então, eu contei para vocês que `M-x l'
08:37 vem para cá, e eu não lembro se vocês
08:40 já testaram o `M-x a', que também faz
08:42 uma coisa parecida...

08:44 Então, agora há pouco a gente tava
08:47 vendo o `M-h M-k', que vai pro help
08:50 sobre uma tecla - `k' é de `key'...

08:53 e agora a gente vai ver `M-h M-f',
08:55 que vai pro help sobre uma função.

08:57 Aqui a gente tem uma função com um nome
08:58 muito curto - `l'. Como é que a gente
09:00 consegue mais informação sobre ela?

09:02 A gente pode bater `M-h M-h l ENTER',
09:05 E aí ele abre esse buffer aqui,
09:10 com montão de links sobre a função `l',

09:12 ou a gente pode seguir isso aqui,
09:14 que é um link pro efeito de bater
09:17 `M-h M-f l'...

09:20 E aí nesse caso isso é uma função que
09:22 não tem uma descrição - ela não tá
09:24 documentada... então é melhor a gente ir
09:26 para cá e ver o código fonte dela. Ela é
09:28 uma função muito curta, ó - é uma função
09:30 que tem uma linha só, é isso aqui...

09:34 e ela vai pro arquivo de anotações sobre Lean.
09:37 a mesma coisa pro a - e um dos links aqui
09:39 vai pro código fonte dela - é esse...

09:44 e o `a' ele garante que esse
09:48 diretório existe - /tmp/L/ -
09:50 e ele abre o arquivo /tmp/L/a.lean.
09:57 Tá? Isso vai ser importante depois.

10:00 Nesse momento o a.lean... bom, eu
10:04 tou usando esse a.lean como um arquivo
10:06 temporário, e aqui tem umas coisas que eu
10:08 botei nele agora há pouco, num dos testes.

10:19 Outra coisa que pode ser útil para
10:21 algumas pessoas é a seguinte... algumas
10:23 pessoas vão precisar definir sequências
10:25 novas de teclas - o Halian precisou
10:28 disso porque o F8 pra ele já tava
10:30 definido de um outro jeito...

10:32 nas minhas anotações sobre MacOS, OSX,
10:33 ou whatever, como as pessoas queiram chamar...
10:38 tem uma seção sobre o arquivo de
10:41 configuração que eu criei pro Halian - que
10:43 a gente criou juntos... e tem esse
10:47 trechinho no arquivo de anotações dele...

10:49 ele precisou definir o `C-RET',
10:53 `C-Return', como a função que tava
10:55 associada ao F8...

10:57 Então esse comando daqui define
10:59 que o `C-Return' faz isso aqui,
11:01 e essa linha daqui foi gerada
11:04 por essa linha daqui, find-esetkey-links,
11:07 que gera esse buffer temporário...

11:10 E eu escolhi mandar isso aqui pro Halian.

11:15