Skip to content

Conversation

@sonmarcho
Copy link
Member

@sonmarcho sonmarcho commented Jan 10, 2026

This PR introduces a minor change which is worth mentioning by updating the formatting of body regions in Charon-ML. Instead of displaying, e.g., &'0 ..., we display &°0 .... I'm not super happy with the use of the symbol ° and it can be changed: the only important thing is that I need to use a different symbol for the bound regions and for the body regions, otherwise the logs can be quite confusing when debugging.

ci: use AeneasVerif/eurydice#367
ci: use AeneasVerif/aeneas#691

@sonmarcho sonmarcho enabled auto-merge January 11, 2026 12:03
@sonmarcho sonmarcho disabled auto-merge January 11, 2026 12:03
@sonmarcho sonmarcho added this pull request to the merge queue Jan 11, 2026
github-merge-queue bot pushed a commit that referenced this pull request Jan 11, 2026
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Jan 11, 2026
@sonmarcho sonmarcho added this pull request to the merge queue Jan 11, 2026
Merged via the queue into main with commit a93a43d Jan 11, 2026
14 of 18 checks passed
@sonmarcho sonmarcho deleted the son/fixes branch January 11, 2026 12:09
@Nadrieril
Copy link
Member

Nadrieril commented Jan 12, 2026

FYI they were already different: '_42 is an anonymous bound region whereas '42 is a body region (the idea being that _42 is a valid rust identifier but 42 isn't). Did you not notice or was that not clear enough still?

@sonmarcho
Copy link
Member Author

FYI they were already different: '_42 is an anonymous bound region whereas '42 is a body region (the idea being that _42 is a valid rust identifier but 42 isn't). Did you not notice or was that not clear enough still?

I see, thanks for this! I found the issue in a case where there were only body regions and it was unclear to me whether they were body regions or anonymous regions. Had there been both in the context I would probably have noticed the difference. I'm still in favour of having a more discriminative formatting.

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.

3 participants