LeanInk silently eats lean compile errors

Open lovettchris opened this issue 3 years ago • 1 comments

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

Aug 26 '22 00:08 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:

Aug 30 '22 19:08 lovettchris