Adds flags to control Alectryon output

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

Adds flags to control Alectryon output #42

Closed vanessa-rodrigues closed 1 year ago

vanessa-rodrigues commented 1 year ago

Description

This PR creates flags on LeanInk to allow users to better control alectryon output as requested in this issue. This only covers bullet points one and two of the issue. These points are about not having alectryon bubbles on calc blocks nor on blocks containing sorrys.

Notable Changes

New command line options are: --x-disable-sorry-info, --x-disable-calc-info

Additional Notes

Output not enabling new flags:

Output enabling new flags:

gebner commented 1 year ago

CI failure is unrelated afaict.