EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
321 stars 49 forks source link

The pretty printer does not line wrap module parameters #594

Closed oskgo closed 3 months ago

oskgo commented 3 months ago

This causes very wide and hard to read output when using long module names or deeply nested modules, especially when using pRHL where line wrapping issues affect the quality of the entire output rather than just the line where the issue occurred.

I've got the following minimal reproduction:

module type Foo = {}.
module VeeeeeeeeeeeeeeeryLongName1 = {}.
module VeeeeeeeeeeeeeeeryLongName2 (F: Foo) = {
  proc main() = {}
}.
module VeeeeeeeeeeeeeeeryLongName3 (F: Foo) = {
  proc main() = {}
}.

equiv test: VeeeeeeeeeeeeeeeryLongName2(
              VeeeeeeeeeeeeeeeryLongName1).main
          ~ VeeeeeeeeeeeeeeeryLongName3(
              VeeeeeeeeeeeeeeeryLongName1).main
           : true ==> true.
proc*.