Skip to content

Clean json generation - #1102

Merged
Nadrieril merged 15 commits into
AeneasVerif:mainfrom
soteria-tools:clean-json
Apr 27, 2026
Merged

Clean json generation#1102
Nadrieril merged 15 commits into
AeneasVerif:mainfrom
soteria-tools:clean-json

Conversation

@N1ark

@N1ark N1ark commented Apr 17, 2026

Copy link
Copy Markdown
Collaborator

This PR sets up the codebase to enable the addition of a new serialisation format, using serde's postcard format.

This cleans up a lot of ad-hoc behaviours in serialisation: the crate's type is now entirely derived, and it's deserialiser entirely generated too, with only a tiny wrapper to get a more nicely shaped crate out of it.

More precisely:

  • Split generate-ml/main.rs (previously 1400 lines) into several modules: to_ocaml_ty for the generation of OCaml types, of_json for the generation of the JSON deserializer, and util.
  • Add Generated_FullAst.ml (exposed in GAst.ml), which contains the "root" types of the AST that weren't generated before: translated_crate and body (and I also moved some related types in there)
  • Merged all _OfJson files, to simplify translation
  • Merged all Print_ files, to also simplify things

I tried splitting the commits to be as reviewable as possible; note that OCaml does not compile from commit 4 (Add FullAst) to commit 10 (Merge all OfJson), since making everything compile in one go would have been too big of a commit.

ci: use AeneasVerif/aeneas#959
ci: use AeneasVerif/eurydice#397

@N1ark

N1ark commented Apr 18, 2026

Copy link
Copy Markdown
Collaborator Author

hmm the OCaml tests pass for me locally, not sure how this fails given files should be deserialized first? could it be Nix somehow reusing old .llbc files or not re-building something...? i forgot to push a change :p

if you're happy with this I'll update Aeneas and Eurydice

Comment thread charon/src/ast/gast.rs Outdated
Comment thread charon-ml/src/GAstUtils.ml Outdated
Comment thread charon/src/ast/krate.rs Outdated
Comment thread charon/src/bin/generate-ml/util.rs Outdated
Comment thread charon/src/bin/generate-ml/util.rs Outdated

@Nadrieril Nadrieril left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's so much better :') Looks great to me

@N1ark
N1ark force-pushed the clean-json branch 2 times, most recently from af6828e to 3367ed0 Compare April 24, 2026 11:35
@N1ark
N1ark force-pushed the clean-json branch 2 times, most recently from 72d1dbf to 16055a1 Compare April 24, 2026 17:00
None => false,
Some(ty) => self.type_to_ocaml_ident_raw(ty).0 == "translated_crate",
}
self.current_item == Some("translated_crate".to_string())

@Nadrieril Nadrieril Apr 27, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No need to fix this but fyi self.current_item.as_deref() == Some("translated_crate") exists :)

@Nadrieril

Copy link
Copy Markdown
Member

Let's goooo

@Nadrieril
Nadrieril added this pull request to the merge queue Apr 27, 2026
Merged via the queue into AeneasVerif:main with commit cb4df88 Apr 27, 2026
5 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.

2 participants