Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Derive eq #548

Merged
merged 2 commits into from
Feb 12, 2025
Merged

Derive eq #548

merged 2 commits into from
Feb 12, 2025

Conversation

N1ark
Copy link
Contributor

@N1ark N1ark commented Feb 11, 2025

Derive eq on types, to expose an equal_typ : typ -> typ -> bool function.

The diff is a mess because for some reason running dune fmt formats the code quite differently? If you have an idea on what causes it let me know, and I'll try fixing it :)

@N1ark
Copy link
Contributor Author

N1ark commented Feb 11, 2025

Update on the formatting thing: hmm, seems like I just can't get ocamlformat to install in OCaml 4.13.1, because uucp won't install due to it trying to access ocaml-base-compiler.5.3.0? Sorry about that will try to get it fixed but this is odd :/

@Nadrieril
Copy link
Member

I'm very unfamiliar with the status of ocaml toolchains. If you have access to nix, I recommend running nix develop to get the pinned version of ocamlformat and the ocaml toolchain that we use.

@N1ark
Copy link
Contributor Author

N1ark commented Feb 11, 2025

Hmm well not sure what was happening, I just changed the diff manually to make sure the formatting remained consistent. Ready for review : )

@sonmarcho
Copy link
Member

Hmm well not sure what was happening, I just changed the diff manually to make sure the formatting remained consistent. Ready for review : )

Sorry about that: this is a really annoying issue, I'm not sure what happened with Opam. Did you install the OCaml switch following the instructions given in the README?
Overall it looks good to me: let's see what the CI says.

@N1ark
Copy link
Contributor Author

N1ark commented Feb 11, 2025

Did you install the OCaml switch following the instructions given in the README?

Yep :/ I'll clear the switch and re-do it just in case; I fixed the couple things CI wasn't happy about in 3c0590b.

@N1ark
Copy link
Contributor Author

N1ark commented Feb 12, 2025

@sonmarcho Sadly I can't do much about this invisible character problem; running nix develop fails on my system (arm64) and I can't replicate the formatting with ocamlformat for some reason – you're more than welcome to commit the change yourself if you can, sorry 😅

@Nadrieril
Copy link
Member

This is unfortunate, is there maybe a version of ocamlformat that's easier to install?

Anyway, I fixed up the missing space character, the PR should be mergeable. I'll wait for #551 to be merged first because that PR required some cross-repo synchronization.

@N1ark
Copy link
Contributor Author

N1ark commented Feb 12, 2025

Ah, thank you so much! Will try to get this situation sorted for the next time I need to contribute :)

This is unfortunate, is there maybe a version of ocamlformat that's easier to install?

So after one last attempt downgrading to ocamlformat.0.26.2 mostly did the trick (I was on 0.27.0). Having the latest version is probably best, but otherwise just maybe indicating somewhere what version you use would be sufficient :)

The only issue I'm running into is I still get two small formatting changes when formatting, though this is much more manageable of course. Tried downgrading all the way back to 0.24.1 and this change keeps happening.

File "charon-ml/src/PrintTypes.ml", line 1, characters 0-0:
diff --git a/_build/default/charon-ml/src/PrintTypes.ml b/_build/default/charon-ml/src/.formatted/PrintTypes.ml
index 19259dd9..19f64493 100644
--- a/_build/default/charon-ml/src/PrintTypes.ml
+++ b/_build/default/charon-ml/src/.formatted/PrintTypes.ml
@@ -371,7 +371,7 @@ let trait_clause_to_string (env : 'a fmt_env) (clause : trait_clause) : string =
 
 let generic_params_to_strings (env : 'a fmt_env) (generics : generic_params) :
     string list * string list =
-  let { regions; types; const_generics; trait_clauses; _ } : generic_params =
+  let ({ regions; types; const_generics; trait_clauses; _ } : generic_params) =
     generics
   in
   let regions = List.map region_var_to_string regions in
File "charon-ml/src/NameMatcher.ml", line 1, characters 0-0:
diff --git a/_build/default/charon-ml/src/NameMatcher.ml b/_build/default/charon-ml/src/.formatted/NameMatcher.ml
index 62d1de95..2b654072 100644
--- a/_build/default/charon-ml/src/NameMatcher.ml
+++ b/_build/default/charon-ml/src/.formatted/NameMatcher.ml
@@ -1029,7 +1029,7 @@ and const_generic_to_pattern (ctx : ctx) (c : to_pat_config) (m : constraints)
 
 and generic_args_to_pattern (ctx : ctx) (c : to_pat_config) (m : constraints)
     (generics : T.generic_args) : generic_args =
-  let { regions; types; const_generics; trait_refs = _ } : T.generic_args =
+  let ({ regions; types; const_generics; trait_refs = _ } : T.generic_args) =
     generics
   in
   let regions = List.map (region_to_pattern m) regions in

@Nadrieril
Copy link
Member

maybe indicating somewhere what version you use would be sufficient

Oh of course! I was sure this was pinned in the .ocamlformat but I was wrong. I just added a commit to this PR so that at least you get a nice error if you're not on the expected version.

@sonmarcho sonmarcho merged commit a285029 into AeneasVerif:main Feb 12, 2025
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.

3 participants