search

ocaml-gospel / gospel

A tool-agnostic formal specification language for OCaml.
https://ocaml-gospel.github.io/gospel
MIT License
123 stars 16 forks source link

Merge implementations branch with main #390

Open ionchirica opened 5 months ago

ionchirica commented 5 months ago

This pull request extends the Gospel toolchain with the OCaml parsetree for structure elements. This allows one to parse Gospel-decorated OCaml implementation files, yet without type-checking them. The introduced changes derive from the work we have been conducting in Cameleer for the past four years. In particular, integrating this pull request in Gospel would unblock an official release of Cameleer itself.

n-osborne commented 5 months ago

Thank you very much for this huge amount of work!

As this end up in a very very large PR (117 commits as for today), could it be possible to clean up the git history so that it is easier to understand what's going on and review it?

ionchirica commented 5 months ago

As this end up in a very very large PR (117 commits as for today), could it be possible to clean up the git history so that it is easier to understand what's going on and review it?

Sure thing, I'm on it!

I also found that the changes I did to the PPS do not deal very well with uncommon ways of writing loops (or long formatted) such as:

while
  uncommon_way_of_writing_conditions
do
  ...
done

I'll be sure to fix that and add some tests.

mariojppereira commented 5 months ago

Thank you very much for this huge amount of work!

As this end up in a very very large PR (117 commits as for today), could it be possible to clean up the git history so that it is easier to understand what's going on and review it?

You are absolutely right! I will try to help @ionchirica on cleaning up a little bit the history.

n-osborne commented 3 months ago

Do you need some help cleaning up the git history?