Hevea

Bez dwóch zdań, TeX i LaTeX to najlepsza rzecz jaka przydarzyła się w dziedzinie programów komputerowych logikom i filozofom. Opowieści o kartkach wkręcanych do maszyzny do pisania do góry nogami aby zrobić znaczek kwantyfikatora to już tylko bajki do strasznie rozbrykanych studentów.

Tym niemniej format wynikowy LaTeX-a pozostawia trochę do życenia. Czytniki DVI nie są zbyt rozpowszechnione, a PDF-y mają to do siebie, że choć są ładne, są też ciężkie i powolne. Jesteśmy na nie skazani, bo jakolwiek konwersja np. do HTML-a powoduje albo utratę wszystkich znaczków, co większość prac logicznych pozbawi wartości, albo będzie się korzystać z formuł przerobionymi na obrazki, co ogólnie obsysa.

Tak mniej więcej myślałem aż do momentu, gdy odkryłem narzędzie o nazwie Hevea, które (w miarę bezstratnie) przerabia źródło TeX-a na HTML. Jest to możliwe dzięki dobrodziejstwu kodowania UTF-8, które zawiera takie bajery, jak ∀ czy ∃. Oczywiście, stracimy ładny TeX-owy skład wyrażeń matematycznych, ale za to możemy np. zaznaczyć formułę i wkleić do okienka Jabbera abo naszego ulubionego IM. Nie mówiąc już o przeglądaniu artykułów na słabych maszynach, takich jak mój laptop (16 MB RAM-u).

Program nie jest niestety do końca doskonały. Szczególnie kiepsko radzi sobie z pakietami AMS. Nie widzi na przykład żadnych linii oprócz pierwszejw multline. Miejmy jednak na dzieję, że z czasem to się poprawi.

A poza tym, Konrad Zdanowski pokazał mi dzisiaj swój dowód drugiego twierdzenia Goedla, który zajmuje (i to bez żadnych tricków ani skrótów) niecałą kartkę formatu A4. Korzysta głównie z pojęć teorii obliczalności i jest wyjątkowo przyjazny dla czytelnika.