LeanInk silently eats lean compile errors
Opened this issue · 1 comments
lovettchris commented
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 commented
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:
