Sem Categoria – 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.

]]>

Túnel SSH

Mon, 21 Sep 2015 22:47:40 +0000

Por motivo de segurança, em algumas situações você não tem acesso direto ao servidor alvo. Contudo, liberam acesso SSH à uma outra máquina que acessa esse servidor e você precisa utilizar aplicativos à partir da sua máquina, mas acessando o servidor alvo. Como resolver esse problema de maneira transparente? Para isso, existe o túnel SSH.

Esse túnel pode ser contemplado pelo seguinte comando:

[sourcecode language=”bash”]ssh -f USUARIO@SERVIDORCOMACESSO -L PORTAACESSAR:SERVIDORACESSAR:PORTAORIGINAL -N[/sourcecode]

O parâmetro mais importante é o -L que é responsável por mapear qual porta você irá acessar pela sua máquina (PORTAACESSAR), de qual servidor (SERVIDORACESSAR), e qual porta desse servidor você irá acessar (PORTAORIGINAL).

Por exemplo, se eu quero acessar o servidor de AD que está disponível no servidor 192.168.18.6 e na porta 389 à partir da minha máquina na porta 2000, sendo que só tenho acesso ao servidor 192.168.18.1, executo o seguinte comando:

[sourcecode language=”bash”]ssh -f [email protected] -L 2000:192.168.18.6:2000 -N[/sourcecode]

Com isso, tenho acesso ao servidor de AD da máquina 192.168.18.6 pela porta 2000 da máquina 192.168.18.1, que seria a única máquina que eu deveria ter acesso.

O parâmetro -f especifica que o SSH deve rodar em background após informar a senha. O -N especifica que nenhum comando remoto será executado, ou seja, só irá fazer o port forward utilizado no nosso túnel.

Agora é só aproveitar esse recurso que é muito útil quando temos acesso limitados à servidores ou necessitamos fazer port forwading.

]]>

Alterando o Hostname Oracle Linux

Wed, 20 Nov 2013 17:58:21 +0000

Para alterar o hostname no Oracle Linux ou distribuições baseadas no RedHat basta alterar a linha HOSTNAME do arquivo /etc/sysconfig/network.

Verifique também o arquivo /etc/hosts. Reinicie o Linux ou o serviço xinetd.

]]>

Cursos e Patrocínio

Mon, 06 May 2013 14:47:03 +0000

Olá Pessoal!

A Trainning está nos patrocinando e oferecendo vários cursos com desconto para os leitores desse blog. A Trainning é uma escola de treinamentos de TI e de Governança de Projetos, que possui sua sede em São Paulo e filiais espalhadas em diversas capitais do Brasil. Se você tem interesse em fazer algum dos vários cursos disponíveis é só informar que você é leitor do meu blog que irá ganhar 5% de desconto.

Alguns cursos oferecidos são:

Essa promoção vale para qualquer curso da Trainning, basta informar que você lê o meu blog. Eu vou fazer um curso de ITIL e vou avaliar para vocês como é a Trainning. Qualquer dúvida é só avisar!

]]>

Retrospectiva 2010

Mon, 03 Jan 2011 14:51:53 +0000

Mesmo eu reativando o blog somente em Agosto, acho que vale a pena fazer uma retrospectiva de 2010. Para isso utilizei alguns plugins do wordpress e obtive o seguinte resultado.

Foram 23401 visitas no website, sendo realizada por 8897 visitantes. 61.98% vieram de sistemas de buscas, 22.68% acesso direto e 15.34% de sites que referenciam o blog. 53.95% dos visitantes utilizam Firefox, 22.56% Chrome, 20.23% IE, 1.48% Opera, 1.18% Safari e o restante outros browsers (Konqueror, Opera Mini, …). Os 15 países que mais visitaram o site foram: Brazil, Portugal, Estados Unidos, China, França, Espanha, Argentina, Alemanha, Angola, Suiça, Rússia, Japão, México, Canadá e Hungria. Do Brasil as 15 cidades que mais visitaram o blog foram: São Paulo, Ribeirão Preto, Rio de Janeiro, São José do Rio Preto, Brasília, Belo Horizonte, Fortaleza, Campinas, Porto Alegre, Goiânia, Curitiba, Recife, Salvador, Florianópolis e Cuiabá.

Os 5 termos mais buscados no Google que direcionam pro meu site foram: java ubuntu 10.10, extensao bpm para o jdeveloper, eclipse helios jboss tools, openswing, captcha receita federal. As buscas mais realizadas dentro do site foram: jboss, apache, soa, popup adf, subversion.

Em 2010 eu escrevi 42 posts e adicionei 3 página nesse blog, com o total de 112 anexos.

Número de posts em cada mês:

janeiro:	2 (4.76%)
julho:	1 (2.38%)
agosto:	8 (19.05%)
setembro:	21 (50%)
outubro:	15 (35.71%)
novembro:	11 (26.19%)
dezembro:	6 (14.29%)

Número de posts em cada dia da semana:

domingo:	6 (14.29%)
segunda-feira:	16 (38.1%)
terça-feira:	6 (14.29%)
quarta-feira:	7 (16.67%)
quinta-feira:	6 (14.29%)
sexta-feira:	11 (26.19%)
sábado:	12 (28.57%)

Horário de publicação dos posts:

0:	3 (7.14%)
1:	2 (4.76%)
8:	3 (7.14%)
9:	5 (11.9%)
10:	8 (19.05%)
11:	1 (2.38%)
12:	8 (19.05%)
13:	5 (11.9%)
14:	4 (9.52%)
15:	2 (4.76%)
16:	3 (7.14%)
18:	3 (7.14%)
19:	2 (4.76%)
20:	2 (4.76%)
21:	3 (7.14%)
22:	9 (21.43%)
23:	1 (2.38%)

Em 2010 os posts foram comentados 59 vezes, 10 comentários (16.95%) foram escritos por usuários/autores registrados.

Gostaria de agradecer ao seguintes usuários por suas contribuições:

Eliane Cavalheiro
Antonio Carlos
André Gonçalves Rodrigues
Cássio Alexandre de Sousa

Os post mais comentados em 2010 foram:

Testando o OpenSwing: 11 comentários
Quebrando CAPTCHAs: 7 comentários
Instalação do Eclipse + JBoss Tools: 4 comentários
Tomcat produtivo no JDeveloper com JSF: 3 comentários
Introdução ao HTML 5: 3 comentários
Editor de BDJO para autoração de blu-ray: 2 comentários
Instalação do Tomcat 7 – Servlet 3.0, JSP 2.2 e EL 2.2.: 2 comentários
Eclipse com Subversion = Subclipse: 2 comentários
Começando com Google App Engine: 2 comentários
Palestra Unifev: 2 comentários

Número de comentários em cada mês:

agosto:	4 (6.78%)
setembro:	17 (28.81%)
outubro:	13 (22.03%)
novembro:	18 (30.51%)
dezembro:	7 (11.86%)

Dias que as pessoas comentaram:

domingo:	3 (5.08%)
segunda-feira:	14 (23.73%)
terça-feira:	7 (11.86%)
quarta-feira:	8 (13.56%)
quinta-feira:	14 (23.73%)
sexta-feira:	7 (11.86%)
sábado:	6 (10.17%)

Horário dos comentários:

0:	1 (1.69%)
1:	1 (1.69%)
5:	1 (1.69%)
7:	1 (1.69%)
8:	1 (1.69%)
9:	7 (11.86%)
10:	2 (3.39%)
11:	3 (5.08%)
12:	6 (10.17%)
13:	8 (13.56%)
14:	4 (6.78%)
15:	1 (1.69%)
16:	4 (6.78%)
17:	2 (3.39%)
18:	2 (3.39%)
19:	2 (3.39%)
20:	4 (6.78%)
21:	2 (3.39%)
22:	2 (3.39%)
23:	5 (8.47%)

É isso aí… Muito obrigado a todos e que 2011 seja muito melhor!

]]>