flux-rs / flux

Refinement Types for Rust
MIT License
658 stars 21 forks source link

Do not pretty print fixpoint constraints by default #858

Open nilehmann opened 1 month ago

nilehmann commented 1 month ago

We currently pretty print fixpoint horn constraints in the Display implementation, i.e., we add newlines and indentation to make the sexpr easier to read. This is wasteful if we are not looking at the constraint and it has caused problems in the past (e.g., https://github.com/flux-rs/flux/issues/857#issuecomment-2430070077). I still think is valuable to pretty print them in cases where we do look at them. We should disable pretty printing by default and implement a flag to enable it on demand.

Additionally, the PadAdapter is probably not the most efficient implementation. We could use normal functions instead of implementing Display to avoid wrapping the formatter to get the padding behavior.