fix: generate placeholder text for missing toTex implementations

[kpadmasola]

Generate placeholder text for missing toTex implementations instead failing.

[kpadmasola]

@david-christiansen With this change, the main.tex gets generated. However, running lualatex main.tex fails with errors. I have categorized the errors below along with the fixes to enable successful conversion to main.pdf.

• FIX: Need to add the following for showing error text in red color
  \usepackage{xcolor}
\colorlet{RED}{black}
• FIX: Replace \Verb with \verb
• ERROR: Cannot have verbatim text inside section titles
  • LaTeX Error: \verb illegal in argument.
  • e.g., \subsubsection{The \verb|ToFormat| Class}
  • FIX: We may need something like https://tex.stackexchange.com/questions/152229/strange-error-related-to-verb-in-section-titles
  • Or https://tex.stackexchange.com/questions/24574/how-to-put-verb-command-inside-of-textbf-block
  • Or https://tex.stackexchange.com/questions/2790/when-should-one-use-verb-and-when-texttt
• ERROR: LaTeX Error: \verb ended by end of line — happens in hyperlink args
  • e.g., in \hyperlink{"https://lean-lang.org/doc/reference/4.23.0-rc2/find/?domain=Verso.Genre.Manual.section&name=do-notation"}{\verb|do|
    -notation}.Because the resulting value is treated as a side-effect-free term, the compiler may re-order,`
  • FIX: use \texttt instead
• ERROR: LaTeX Error: Command \item invalid in math mode.
  • e.g., .\item The syntax \verb|have (eq := h) pat := e|
is equivalent to \verb|match h : e with | pat => _|
  • FIX: In the second line there is a | inside \verb
  • So we should use some other delimiter character, such as !
  • Or use \begin{verbatim}
  • Also \item should probably begin on a new line, perhaps?
• ERROR: LaTeX Error: Lonely \item--perhaps a missing list environment.
  • Issue due to \hyperlink second arg having underscore
  • FIX: escape underscore
• ERROR: ! Text line contains an invalid character.
  • e.g., l.32508 ... or. Usually accessed via the \verb|^^^
  • FIX: Try \verb|\^\^\^|
• ERROR: LaTeX Error: \verb illegal in argument.
  • FIX: Replace with \texttt instead

[david-christiansen]

This is a good start! Thanks!

But I think it's important that authors don't have to proofread their document to know if something went wrong. The best situation is that they get error messages and a non-zero return code, but also output that is as readable as possible.

[david-christiansen]

I think this error message should be retained. It's important to prominently tell authors that their document isn't as they expect, without them needing to proofread the resulting text.

[kpadmasola]

done.

[david-christiansen]

Similarly, I think this error message should be retained too. It's good to emit better TeX though.

[kpadmasola]

done.

[david-christiansen]

This should also be a proper error, and it should insert a notice like the other two into the document that is unmistakable.

[kpadmasola]

done.

[david-christiansen]

Thanks for the big list of things that need fixing! That'll be really helpful to check off as it goes.

[david-christiansen]

I'm away from the computer for a few days but will look again as soon as I'm back. Thanks again!