feat: add toTex support for Manual.keywordOf

[kpadmasola]

This PR adds TeX rendering support for Manual.keywordOf.

Relates to #434

[kpadmasola]

@david-christiansen Thanks for your review comments. I have updated the PR.
This time I read the Verso manual carefully (I should have done that earlier :-)

I have few doubts though..

The toHtml logic is using the metadata and constructing a link, while the toTex method I filled in is not making use of the metadata.

1. Is there a way to verify that the toTex logic is doing the right thing, because unless all TeX issues are fixed, the TeX output is not available for proof reading?
2. How do we know what the right thing to do is, in case of TeX?
3. Is there a specification that describes the expected rendering for each Genre+output format?

These are probably very basic questions, but please bear with me as I am still very new to Lean, so it is taking me some time to understand the Verso framework.
Thank you for your patience.

[david-christiansen]

I have few doubts though..

These are good questions!

The toHtml logic is using the metadata and constructing a link, while the toTex method I filled in is not making use of the metadata.

That's fine - PDF links can be added later, as a nice extra, but they're not really necessary in a PDF the same way as on a web page.

1. Is there a way to verify that the `toTex` logic is doing the right thing, because unless all TeX issues are fixed, the TeX output is not available for proof reading?

Good question. Right now, you could do this by deleting all the text of the manual except for a use of keywordOf and building it, but that's not a great workflow.

I'd accept a Verso PR that added a flag to downgrade this error to a warning, and put some kind of placeholder text in the TeX (e.g. "\color{red}{Missing toTeX for Manual.keywordOf}". That'd make the process easier.

2. How do we know what the right thing to do is, in case of TeX?

This is a matter for taste and judgment. How would you like to read this in a printed book? What about on an e-reader? You should think about what is being represented, and use the HTML output as a general guide, taking the different media's tradeoffs into account.

3. Is there a specification that describes the expected rendering for each Genre+output format?

This work is only for the manual genre and TeX/PDF. There's no spec - writing a spec would be harder than just writing the code in this case. You can think of the HTML as being a good guideline for most of it, but not always.

These are probably very basic questions, but please bear with me as I am still very new to Lean, so it is taking me some time to understand the Verso framework. Thank you for your patience.

Not a problem! Thanks for helping out!

[kpadmasola]

@david-christiansen I see that you already made a change in Verso to log error instead of panic when toTeX is missing. However when I do lake update to pull that change in this repo, build is failing

error: Lean exited with code 1
Some required targets logged failures:
- Manual.Meta.Lean
- Manual.Meta.LakeOpt
- Manual.Meta.ElanOpt
error: build failed

Shall I take a shot at fixing the build issue and follow it up with putting placeholder text in the toTeX implementations where appropriate?

[david-christiansen]

Hmm, it certainly builds with the results of #576 locally, and it would really surprise me if CI let us commit something to main that didn't build. Try lake clean before building, perhaps?

[github-actions]

Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit 8a65ca2.

[kpadmasola]

@david-christiansen I figured out why I was getting the error. I had done a lake update to get the new verso version, but forgot to pull the latest changes from main branch in this repo. I remember checking that my fork was up to date, but I must have forgotten to pull the changes locally. My mistake :-)

[david-christiansen]

Good news!

The thing to do is not to put placeholder text in the toTeX implementations one-by-one, but rather get Verso to insert it when there is no such implementation. That way, it becomes obvious what needs to be done in order to build a given document.

[kpadmasola]

@david-christiansen thanks for the suggestion, let me try that.

[kpadmasola]

@david-christiansen After the suggested verso changes, I am able to generate _out/tex/main.tex. There are some Undefined control sequence errors when running lualatex main.tex. I'll look into this some more and raise a draft PR tomorrow.

[kpadmasola]

@david-christiansen After manually fixing the errors in the generated main.tex file, I was able to generate main.pdf by running lualatex main.tex. I have collected the issues that we need to fix. The errors fall into about 7 or 8 categories. The fixes will be on the Verso side I suppose, although I haven't identified the code level changes yet.

I'll raise the verso PR now. Next I'll try to identify the code level changes needed to fix TeX compilation errors. If you have any suggestions about where I should look, please let me know.

Here's the generated main.pdf. I haven't gone through it yet. Initially we should make it work, i.e., no TeX errors, and then make it make it look good.

[kpadmasola]

@david-christiansen The related verso PR for inserting placeholder text for missing toTex implementations is leanprover/verso#518