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

Make type checker save type information #376

Merged
merged 6 commits into from Mar 25, 2024

Conversation

n-osborne
Copy link
Contributor

This PR proposes to marshall the product of the type checker and save it in a file with the .gospel file extension so that external tool does not have to run the type checker by themselves.

@n-osborne n-osborne force-pushed the write-gospel-file branch 4 times, most recently from 919c477 to f20380d Compare January 19, 2024 17:37
@n-osborne n-osborne force-pushed the write-gospel-file branch 2 times, most recently from f478d0a to 0294c6b Compare January 24, 2024 11:29
@n-osborne n-osborne added this to the 0.3 milestone Feb 5, 2024
@n-osborne n-osborne requested a review from shym February 5, 2024 13:48
Tools does not have to run the type checker again.
Moving to writing the type checking output in a file, we will ask dune
to run the gospel type checker. Printing `OK` on stdout add unnecessary
noise here.
Unfortunately, this requires generating dummy empty `.gospel` files for
failing tests
Copy link
Contributor

@shym shym left a comment

Choose a reason for hiding this comment

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

This is a simple and nice change, well done!
I’ve pushed in my drop-ok branch two extra commits to complete the change of dropping OKs and to make dune aware of the .gospel files that will be generated for succeeding tests. In turn, this makes an extra test that type checking succeeded on documentation :-)

I have one suggestion: it would be nice to teach gospel check how to process .gospel files, among other things as a way to test the read_gospel_file and that the marshalling did work as expected. It would also serve as a simple way to inspect the content of a .gospel file.

Simplify error message along the way as there are now too many different
cases to have a detailed yet concise message.
@n-osborne
Copy link
Contributor Author

n-osborne commented Feb 23, 2024

Thank you @shym for your comment :-)
I've integrated your two commits and, following your suggestion, made gospel check handle .gospel files and test that reading back the typing information from a .gospel file give the same output than typing from the initial .mli file.

@n-osborne n-osborne requested a review from shym February 23, 2024 15:32
Copy link
Contributor

@shym shym left a comment

Choose a reason for hiding this comment

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

This is nice, thank you!
(I only reviewed the diff with my drop-ok branch, not commit by commit)
A tiny suggestion: with GNU’s wc, wc -l < bar is just the line count, so you don’t need an extra cut).
I’m not sure about portability (but that’s already the case with the cut, I might argue :-).

Copy link
Contributor

@mariojppereira mariojppereira left a comment

Choose a reason for hiding this comment

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

I believe this pull request is ready to be merged.

@n-osborne
Copy link
Contributor Author

Thanks.
Merging.

@n-osborne n-osborne merged commit c198f14 into ocaml-gospel:main Mar 25, 2024
6 checks passed
@n-osborne n-osborne deleted the write-gospel-file branch March 25, 2024 10:11
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.

None yet

3 participants