Today I learnt to produce Hasse diagrams of lattice reducts of
residuated binars with involution in TeX:) The process starts with
parsing a JSON response from the Isabelle server. Then I extract
Cayley tables of meet and join operations from a somewhat structured
reply of Nitpick. After that, I construct a partial order relation of
lattice reduct. Then I get a Hasse diagram from an adjacency matrix.
I tried to do these two steps with Sage but failed. Unfortunately,
Sage works only with system Python by default, and it's incredibly
tough to run it in a virtual environment. Finally, when you have a
Hasse diagram, you can create a GraphViz input string from it. That
idea I borrowed from Sage, so my experiments with it were not
useless:) And then, hurrah, there exists a pretty Python package
``dot2tex``. It converts from GraphViz format to ``tikz``! I never
used GraphViz before, and I can't say that I liked it. But in
general, the pipeline built looks quite good. I think that I will
publish it in the nearest future.
