Provide a way to tell leanink to generate comments on #eval, #check commands
Opened this issue · 2 comments
Description
Readers are saying always visible comments are more readable than the little bubbles we are adding to eval statements. So we should make this an option when generating leanink books, like the new chapter on monads.
Detailed behaviour
Even better if we can do what David is doing in his functional programming in Lean book, which is to also write the "expected" values in the book so that the tool can then verify if that is what it is seeing when evaluating the code, so it can report errors if it finds a difference. This way the book author can verify the new values, rather than blindly posting something that might be entirely an error caused by some breaking change in the Lean compiler.
Testscenarios
References
I think the problem is not the bubble, but the fact that their content is not visible by default.
The bubbles look great to me, the problem is that we have to hover or click them to see the content.
See https://github.com/cpitclaudel/alectryon#controlling-output and https://github.com/cpitclaudel/alectryon#output-assertions. Alectryon has a ton of annotations like this, which we will have to reimplement if we don't want to go through it and docutils.