Skip to content

Conversation

@JNC4
Copy link
Contributor

@JNC4 JNC4 commented Feb 12, 2026

Summary

  • Remove the @, (break hint) from the format string in pp_msymbol when printing multi-component module paths
  • The break hint allowed OCaml's Format module to insert line breaks between namespace components (e.g., between G. and RO), producing incorrect output

Before:

proc sample(x : G.in_t) : unit = {
    G.
    RO.get(x);
}

module Alias = G.
RO.

After:

proc sample(x : G.in_t) : unit = {
    G.RO.get(x);
}

module Alias = G.RO.

Test plan

Fixes #696.

Remove the `@,` (break hint) from the format string in `pp_msymbol`
when printing multi-component module paths. The break hint allowed
the formatter to insert line breaks between namespace components,
causing output like `G.\nRO.get(x)` or `module Alias = G.\nRO.`
instead of the correct `G.RO.get(x)` and `module Alias = G.RO.`

Fixes EasyCrypt#696.
@strub
Copy link
Member

strub commented Feb 12, 2026

Note that the way that hint is used by Format indicates that the procedure call is printed with a vertical box, something that we might want to avoid.

Anyway, since the parser does not support namespace with spaces, the hint is invalid.

@strub strub enabled auto-merge (rebase) February 12, 2026 10:33
@strub strub merged commit 3866ec1 into EasyCrypt:main Feb 12, 2026
16 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Newline in pretty printing modules with namespaces

2 participants