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.

Sign up for GitHub

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

Jump to bottom

Engine: get rid of most of exception throwing function calls, improve parsers and error reports #1197

Merged
merged 12 commits into from
Dec 18, 2024
Merged

Engine: get rid of most of exception throwing function calls, improve parsers and error reports #1197

merged 12 commits into from
Dec 18, 2024

Conversation

W95Psp
Copy link
Collaborator

@W95Psp W95Psp commented Dec 18, 2024 •
edited
Loading

This PR:

  • adds a version to haxmeta files
  • adds a version to the engine
  • makes the frontend check haxmeta versions
  • makes the engine check the frontend version
  • improve parsing error reporting
  • makes generated parsers conform to yojson style
  • report parsing errors in the F* backend
  • removes most of *_exn calls
  • removes most of failwith calls

Fixes #1150, fixes #1188, fixes #1187

Context: this PR goes toward better user experience for releasing hax v0.1, it gets rid of most of remaining unhandled explicit failures

@W95Psp W95Psp requested a review from maximebuyse December 18, 2024 14:28
@W95Psp W95Psp marked this pull request as ready for review December 18, 2024 14:28
@W95Psp W95Psp changed the title Improve parsers Engine: get rid of most of exception throwing function calls, improve parsers and error reports Dec 18, 2024
maximebuyse
maximebuyse approved these changes Dec 18, 2024
View reviewed changes
Copy link
Contributor

@maximebuyse maximebuyse left a comment

Choose a reason for hiding this comment

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

Great 🎉

@W95Psp W95Psp added this pull request to the merge queue Dec 18, 2024
github-merge-queue bot pushed a commit that referenced this pull request Dec 18, 2024
@W95Psp
Merge pull request #1197 from hacspec/improve-parsers
14faff5 
Engine: get rid of most of exception throwing function calls, improve parsers and error reports
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to Branch Protection failures Dec 18, 2024
You're not authorized to push to this branch. Visit "About protected branches" for more information.
karthikbhargavan
karthikbhargavan approved these changes Dec 18, 2024
View reviewed changes
Copy link
Contributor

@karthikbhargavan karthikbhargavan left a comment

Choose a reason for hiding this comment

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

Looks great. Did you try on libcrux? If not, I can tomorrow.

@W95Psp
Copy link
Collaborator Author

W95Psp commented Dec 18, 2024

I spawned a job just now just in case (should be OK though, it's only adding more reporting, I don't see how that could fail): https://github.com/cryspen/libcrux/actions/runs/12398704866

@W95Psp
Copy link
Collaborator Author

W95Psp commented Dec 18, 2024

The job is successful, I'm mergining

@W95Psp W95Psp added this pull request to the merge queue Dec 18, 2024
Merged via the queue into main with commit 9d78af6 Dec 18, 2024
15 checks passed
@W95Psp W95Psp deleted the improve-parsers branch December 18, 2024 18:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@maximebuyse maximebuyse maximebuyse approved these changes

@karthikbhargavan karthikbhargavan karthikbhargavan approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
3 participants
@W95Psp @karthikbhargavan @maximebuyse