LeanInk silently eats lean compile errors

leanprover / LeanInk

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.

Apache License 2.0

60 stars 16 forks source link

LeanInk silently eats lean compile errors #24

Open lovettchris opened 2 years ago

lovettchris commented 2 years ago

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 2 years ago

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: