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.