search

ualib / agda-algebras

The Agda Universal Algebra Library (html docs available at the url below)
https://ualib.github.io/agda-algebras/
Creative Commons Attribution Share Alike 4.0 International
28 stars 7 forks source link

update HSP.lagda for html (instead of tex) #228

Closed williamdemeo closed 2 years ago

williamdemeo commented 2 years ago

This translates HSP.lagda from LaTeX to Markdown so it will look better on web pages.

JacquesCarette commented 2 years ago

That feels like a lot of "make work". Also, I'm pretty sure there are decent automated tools to do this.

williamdemeo commented 2 years ago

Well, yes, of course I would like to use the right tools and a workflow that avoids the tedium. And I intend to figure out the best way to do this, but it's non-trivial and not obvious (to me), so will take some time to figure out.

In the meantime, I just wanted to get the Demo.HSP module typeset so it looks less horrible than before (with all the latex macros appearing on the web page), so I used pandoc to convert from tex to markdown. That produces a markdown file that is far from usable without substantial editing, because of all the special macros we use to typeset Agda code in a TeX document.

I agree that there must be a better way to do this. Unfortunately, I haven't found it yet. Of course, you are more than welcomed to suggest solutions!