LeanInk silently eats lean compile errors

[lovettchris]

Description

If I have a bug in my book chapter, LeanInk reports these errors in the hover over tooltip, but we need a process to ensure there are no bugs in the book.

Is there a way we can run LeanInk in the CI build that will break if there are bad code snippets?

Expected behaviour

Reproducing the issue

Environment information

• Operating System:
• Lean version:
• LeanInk version:
• Alectryon version:

Suggested fix

Additional Notes

[lovettchris]

Well now I'm not convinced this is a bug or a feature. Sometimes you do want to write about compile errors and show examples like I did in the chapter on monad transformers: