Thiago Galbiatti Vespa – Thiago Galbiatti Vespa

Coq – Provando teoremas de forma programática

Fri, 17 Oct 2025 16:26:53 +0000

O Coq é um “provador” de teoremas de maneira interativa. Ele nos auxilia a definir funções, predicados, a verificar as provas e suas consistências de maneira programática. Existem outras ferramentas que tem um propósito similar, como o Isabelle da Universidade de Cambridge, que iremos abordar em outro post.

Para instalar, você pode fazer o download da última release no github ou utilizar o seu gerenciador de pacotes padrão. Outra opção boa é utilizar o docker com a imagem coqorg/coq. Utilize a forma que fique mais adequada a você. Caso tenha alguma dúvida, me avise.

]]>

File not found e unknown option no latex

Mon, 19 Jul 2021 14:01:53 +0000

Para poder escrever minha qualificação no Latex, era necessário o pacote do abntex2. Entretanto não encontrei ele na minha distribuição linux, que no caso é o Gentoo. Após obter o seguinte erro:

[sourcecode]File `abntex2.cls’ not found. ^^M[/sourcecode]

Fiz uma busca e encontrei esse arquivo no pacote dev-texlive/texlive-publishers. Instalei ele:

[sourcecode language=”bash”]sudo emerge -av dev-texlive/texlive-publishers[/sourcecode]

Após tentar compilar o meu arquivo latex, obtive outro erro:

[sourcecode]Package babel Error: Unknown option `spanish’. Either you misspelled itd. \ProcessOptions*[/sourcecode]

Vi que meu template havia suporte para língua espanhola, para isso, também tive que instalar os pacotes do idioma espanhol:

[sourcecode language=”bash”]sudo emerge -av dev-texlive/texlive-langspanish[/sourcecode]

Após isso, mais isso problema:

[sourcecode]File `glossaries.sty’ not found. \RequirePackage[/sourcecode]

Procurei onde poderia encontrar esses arquivos e há um pacote glossaries. Após a instalação do pacote:

[sourcecode language=”bash”]sudo emerge -av dev-tex/glossaries[/sourcecode]

Todos os problemas foram resolvidos.

]]>

Como fazer download de todas as mídias e anexos de um canal do Telegram

Mon, 25 May 2020 19:17:14 +0000

Entrei num canal de compartilhamento de arquivo, mas não consegui pegá-lo logo no início. Por isso senti a necessidade de fazer o download de todos os arquivos que estavam nesse canal. Achei um código parecido no stackoverflow e resolvi escrever esse post.

Para poder realizar essa operação, crie um ambiente virtual python e depois execute as configurações necessárias para a biblioteca do Telethon. Após isso instale uma biblioteca que mostre o percentual em uma barra “bonitinha”:

[sourcecode language=”bash”]pip install tqdm[/sourcecode]

O tqdm irá mostrar o nosso loop de baixar arquivos de uma maneira mais elegante.

Abaixo segue o código para baixar os arquivos do canal:

[sourcecode language=”python”]from telethon import TelegramClient, events, sync from tqdm import tqdm import os api_id = api_hash = ‘’ client = TelegramClient(‘umasessao’, api_id, api_hash) client.start() messages = client.get_messages(‘’, limit=) for msg in tqdm(messages): msg.download_media(file=os.path.join(‘media’, ‘’)) [/sourcecode]

Substitua , , , e pelos valores adequados e o script irá baixar os arquivos do no caminho .

]]>

Como conversar no Telegram de forma programática

Mon, 25 May 2020 18:53:57 +0000

Tem interesse em fazer um chatbot ou automatizar atividades que possam te notificar pelo celular?

O Telegram expõe suas APIs de forma gratuita e com isso podemos criar programas e utilizar suas funcionalidades, basta utilizar sua criatividade. Para isso é necessário acessar o https://my.telegram.org.

Informe o seu número de telefone em formato internacional. Por exemplo, no Brasil, acrescentar +55. Então o número: (12) 34567-8901, ficaria: +5512345678901.

Você receberá uma senha pelo Telegram com o texto: Web login code. Não passe esse código para ninguém, pois com esse código, é possível até deletar a conta.
Cada vez que você tentar fazer o login ele irá gerar uma nova senha e enviar no seu Telegram.

Selecione a opção “API development tools” para criar uma aplicação.

Informe os dados da aplicação e clique em Create application. Evite colocar acentuação nos primeiros campos, tive alguns problemas por conta disso.

Você irá receber algumas informações importantes… anote-as, clique em “Save changes”.

Em nosso projeto, nós vamos utilizar uma biblioteca python para facilitar a manipulação das APIs do Telegram. Essa biblioteca chama-se Telethon. Para usá-la é necessário ter o python 3 instalado, incluindo o pip. É interessante criar um Ambiente virtual para poder trabalhar.

Para instalar a biblioteca digite o seguinte comando:

[sourcecode language=”bash”]pip3 install telethon[/sourcecode]

Crie um arquivo python com o seguinte conteúdo:

[sourcecode language=”python”]from telethon import TelegramClient, events, sync api_id = api_hash = ‘’ client = TelegramClient(‘umasessao’, api_id, api_hash) client.start() client.send_message(‘thiagovespa’, ‘Olá. Estou testando o envio de mensagem do Telegram’) [/sourcecode]

Substituia a api_id e a api_hash com os valores obtidos nas etapas anteriores. E execute o arquivo python. A última linha envia uma mensagem para o usuário thiagovespa. No primeiro acesso ele irá solicitar as seu telefone, um códio recebido pelo Telegram e sua senha:

Please enter your phone (or bot token): +55
Please enter the code you received:
Please enter your password:

Após informar, um arquivo de sessão do SQLite será criado e você pode executar utilizando a mesma sessão e aí a senha não será mais solicitada.

Para outras funções, consulte a documentação.

]]>

virtualenv: Ambientes Virtuais para Python

Mon, 25 May 2020 14:56:19 +0000

Para isolar bibliotecas e configurações, o python tem um utilitário que cria ambientes virtuais. A grande vantagem da criação desses ambientes é que você pode ter versões diferentes de bibliotecas e uma dependência não afetar a outra. Assim ao instalar uma biblioteca ela não será mais feita de forma global, mas somente para esse ambiente virtual.

O jeito mais simples de fazer isso é utilizando o pip:

[sourcecode language=”bash”]sudo pip install virtualenv[/sourcecode]

Entretanto, em algumas distribuições como o Gentoo, isso normalmente oferece um risco, pois você estará instalando uma biblioteca interna que pode ocasionar conflitos com as bibliotecas de sistema. No meu caso, o Gentoo oferece já um pacote de sistema que faça isso. Se você utiliza essa distro que eu, ao invés de utilizar o comando anterior, utilize esse:

[sourcecode language=”bash”]sudo emerge -av dev-python/virtualenv[/sourcecode]

Verifique se a instalação foi bem sucedida:

[sourcecode language=”bash”]virtualenv –version[/sourcecode]

Para criar um ambiente virtual novo é bem simples. Acesse um diretório onde vai ser criado o ambiente e digite o seguinte comando substituindo nome_do_ve pelo nome do ambiente desejado:

[sourcecode language=”bash”]virtualenv nome_do_ve[/sourcecode]

Você deverá ter uma saída como essa:

Using base prefix ‘/usr’
New python3.7 executable in /development/testes/nome_do_ve/bin/python3.7
Not overwriting existing python3.7 script /development/testes/nome_do_ve/bin/python3.7 (you must use /development/testes/nome_do_ve/bin/python3.7)
Installing setuptools, pip, wheel…
done.

Para utilizar o ambiente é só ativá-lo:

[sourcecode language=”bash”]source nome_do_ve/bin/activate[/sourcecode]

Com isso, você pode instalar as dependências que você precisa e trabalhar com o python, após terminar é só desativar:

[sourcecode language=”bash”]source nome_do_ve/bin/activate[/sourcecode]

Para sair do ambiente é só digitar: deactivate. Para apagar o ambiente é só remover a pasta.

]]>

Instalação do Elasticsearch no Ubuntu 18.04

Mon, 09 Mar 2020 21:53:02 +0000

O Elasticsearch é um motor de busca distribuído feito em Java e de código aberto. Ele é baseado no Apache Lucene, que é uma excelente API para indexação e busca.

Para instalar o Elasticsearch no Ubuntu, a melhor forma é utilizando o repositório oficial. Como pré-requisito, é necessário instalar o Java 8 ou superior (instale o de sua preferência) e o repositório apt via https:

sudo apt install apt-transport-https openjdk-8-jdk

Importe a chave do repositorio:

wget -qO - https://artifacts.elastic.co/GPG-KEY-elasticsearch | sudo apt-key add -

O resultado deverá ser OK. Adicione o repositório do Elasticsearch da versão 7. Se quiser você pode alterar para uma versão anterior:

sudo sh -c 'echo "deb https://artifacts.elastic.co/packages/7.x/apt stable main" > /etc/apt/sources.list.d/elastic-7.x.list'

Atualize o apt e instale normalmente o pacote elasticsearch:

sudo apt update && apt install elasticsearch

Você pode habilitar como serviço:

sudo systemctl enable elasticsearch.service

Ou iniciar de acordo com a demanda:

sudo systemctl start elasticsearch.service

Veja se está funcionando:

curl localhost:9200

Pronto!

]]>

Habilitar System.out e System.err no log do WebLogic

Mon, 20 May 2019 18:41:22 +0000

Embora seja uma má prática utilizar o System.out e System.err para depuração e habilitá-lo no log. Em alguns casos, é preciso. Não entrarei nos méritos quando isso é necessário, mas se você está acessando essa página, já deve saber.

Para habilitar, acesse o WebLogic console. Vá em Environment, Server e escolha o server no qual você deseja habilitar o System.out e System.err no log. Acesse a aba Logging, General e Advanced.

Selecione os dois combos onde diz para redirecionar o stdout e stderr para o log.

Pronto! Só não faça isso em ambiente de produção.

]]>

Iniciando com Qt

Thu, 21 Mar 2019 10:50:38 +0000

O Qt (sua pronúncia é como “cute” em inglês) é um framework para interfaces gráficas feita em C++. Esse framework tem o foco de ser multiplataforma e é largamente utilizado no KDE.

Para iniciar o desenvolvimento é necessário fazer o download da plataforma. No site há algumas opções, como a versão comercial, opensource, download online e offline, além das versões para cada sistema operacional. Para prosseguir nesse artigo, vamos utilizar a versão online com a versão 64 bits do linux.

Após o download, transforme o arquivo em executável e execute-o:

[sourcecode language=”bash”]chmod +x qt-unified-linux-x64-3.0.6-online.run ./qt-unified-linux-x64-3.0.6-online.run[/sourcecode]

Irá abrir uma tela de boas vindas:

Prossiga com as instruções, crie uma conta Qt, especifique o diretório de instalação. Na etapa de seleção de componentes, você poderá especificar a versão do qt a ser utilizada, se vai utilizar a IDE de desenvolvimento (Qt Creator) e se possui necessidade de se trabalhar com gráficos 3D (Qt 3D Studio), além de poder selecionar componentes individuais:

Prossiga com a instalação. Ao final dela você poderá ter acesso ao QT Creator, que está disponível no caminho de instalação que você forneceu:

Agora é só se aventurar. Se você quiser também trabalhar com outras arquiteturas é necessário configurar a plataforma e um debugguer.

Para o debugger eu estou utilizando o gdb, se você já tiver instalado, o QtCreator pode identificá-lo automaticamente. Em Tools, Options, Kits, na aba Debbugers, você poderá ver essa informação:

Na aba Kits você pode configurar outras plataformas, como o Android.

]]>

Kotlin para programadores Java

Wed, 20 Mar 2019 12:17:46 +0000

Comecei a me aventurar no mundo do Kotlin e resolvi criar uma mini referência para facilitar para quem vem do universo Java. Abaixo temos um resuminho inicial que pode facilitar a vida de quem está começando no Kotlin:

Ponto e vírgula é opcional
Constantes não precisam de tipo e são declaradas com a palavra val. Ex: val titulo = “Blog” é o equivalente em Java a final String titulo = “Blog”;
Variáveis também não precisam de tipo e são declaradas com a palavra var. Ex: var nome = “Vespa” é o equivalente em Java a String nome = “Vespa”;
Quando necessário identificar o tipo da variável, constante ou retorno de função é só colocar dois pontos e o tipo após a declaração. Ex: var nome: String
Quando a variável permite nulo é só colocar o ponto de interrogação no tipo. Ex: var nome: String? = null
O operador ternário para verificação de nulo para atribuição de valor default não é mais necessário (e não existe). Isso também é feito com o ponto de interrogação. Ex: var tamanho = nome?.length ?: 0 (Se o nome for nulo o valor para tamanho é zero, caso contrário é o tamanho). Você também pode executar uma ação como dar um return na função ou lançar uma exceção.
Declaração de funções (de modo grosseiro: o equivalente a métodos em java). Utilize fun.

[sourcecode] fun soma(a: Int, b: Int): Int { return a + b } [/sourcecode] ou [sourcecode] fun soma(a: Int, b: Int) = a + b [/sourcecode]

O construtor primário é definido já na declaração de classe. Ex: class Pessoa(val nome: String, var idade: Int)
Herança é feita semelhante à declaração de tipos de variáveis, mas passando o construtor que será chamado. Ex: class PessoaJuridica(nome: String) : Pessoa (nome)
Para sobrescrever uma função, é necessário usar a palavra override.

Há outros recursos bem interessantes do Kotlin, como Data classes, expressão When, coleções, extensões e afins, que abordaremos em outros artigos. Aguarde!

]]>

Resolução de libcurl-gnutls.so.4: cannot open shared object file no Linux

Tue, 18 Sep 2018 13:51:32 +0000

Alguns projetos precisam da referência a libcurl-gnutls, entretanto essa lib pode não estar disponível na sua distribuição (no meu caso Gentoo). Para resolver esse problema:

[code language=”bash”]libcurl-gnutls.so.4: cannot open shared object file: No such file or directory
Error: libcurl-gnutls.so.4: cannot open shared object file: No such file or directory[/code]

Crie um link simbólico da libcurl referenciando a lib necessária:
[code language=”bash”]ln -s /usr/lib/libcurl.so.4 /usr/lib/libcurl-gnutls.so.4[/code]

Com isso a lib é encontrada e o problema resolvido.

]]>