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

more principled generic printer #533

Merged
merged 22 commits into from
Oct 22, 2024
Merged

more principled generic printer #533

merged 22 commits into from
Oct 22, 2024

Conversation

W95Psp
Copy link
Collaborator

@W95Psp W95Psp commented Feb 27, 2024 •
edited
Loading

Exploring more principled/clean generic printer after chatting about the PV backend in Paris with Jonas.
Porting the PV printer should be easy, but that's a bit out of scope, I'm trying to play with the generic printer to converge to something nicer.

This generic printer supports fully source maps v3: any backend using the genric printer gets that for free.

The result is something like that or the fact a user can click in VSCode in some region of the extracted code and be directed to the Rust source.

Fixes #404

This was linked to issues Apr 11, 2024
Document the generic printer and how to write a backend #411
Closed
Generic printer: optionally output source maps #404
Closed
@W95Psp W95Psp removed a link to an issue Apr 11, 2024
Document the generic printer and how to write a backend #411
Closed
@jschneider-bensch jschneider-bensch mentioned this pull request Apr 11, 2024
Closed
@W95Psp W95Psp changed the title WIP more principled generic printer basis more principled generic printer Jul 1, 2024
@W95Psp W95Psp mentioned this pull request Jul 1, 2024
Open
@W95Psp
Copy link
Collaborator Author

W95Psp commented Jul 1, 2024

I updated this PR in a way the current generic printer and the new one cohabit.
We need to move PV to this generic printer (see #745), and then we will be able to remove the previous generic printer.

@W95Psp W95Psp marked this pull request as ready for review July 1, 2024 09:09
@W95Psp W95Psp added the waiting-on-reviewer Status: Awaiting review from the assignee but also interested parties. label Jul 2, 2024
@paulmure paulmure mentioned this pull request Jul 10, 2024
Merged
franziskuskiefer
franziskuskiefer previously requested changes Aug 12, 2024
View reviewed changes
Copy link
Member

@franziskuskiefer franziskuskiefer left a comment

Choose a reason for hiding this comment

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

Let's get some documentation in before we merge this.

cli/driver/src/exporter.rs Outdated Show resolved Hide resolved
engine/lib/new_generic_printer/new_generic_printer_api.ml Outdated Show resolved Hide resolved
engine/profile.dump Outdated Show resolved Hide resolved
@franziskuskiefer franziskuskiefer removed the waiting-on-reviewer Status: Awaiting review from the assignee but also interested parties. label Aug 12, 2024
@W95Psp W95Psp mentioned this pull request Oct 2, 2024
Closed
@W95Psp W95Psp marked this pull request as draft October 2, 2024 07:25
@W95Psp W95Psp mentioned this pull request Oct 3, 2024
Open
4 tasks
@W95Psp W95Psp force-pushed the rust-generic-printer branch 2 times, most recently from acd590b to 436c78b Compare October 8, 2024 08:14
@W95Psp W95Psp force-pushed the rust-generic-printer branch 2 times, most recently from 7817e2f to 9ad1058 Compare October 21, 2024 12:39
@W95Psp W95Psp marked this pull request as ready for review October 21, 2024 12:56
@W95Psp W95Psp requested a review from cmester0 October 21, 2024 13:05
cmester0
cmester0 approved these changes Oct 22, 2024
View reviewed changes
Copy link
Contributor

@cmester0 cmester0 left a comment

Choose a reason for hiding this comment

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

Seems fine, just some extra comments left over, and some duplicate util functions.

engine/backends/fstar/fstar_backend.ml Outdated Show resolved Hide resolved
engine/lib/print_rust.ml Show resolved Hide resolved
engine/utils/sourcemaps/prelude.ml Show resolved Hide resolved
engine/utils/generate_from_ast/codegen_printer.ml Show resolved Hide resolved
@W95Psp W95Psp enabled auto-merge October 22, 2024 09:16
@W95Psp W95Psp added this pull request to the merge queue Oct 22, 2024
github-merge-queue bot pushed a commit that referenced this pull request Oct 22, 2024
@W95Psp
Merge pull request #533 from hacspec/rust-generic-printer
85edc16 
more principled generic printer
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Oct 22, 2024
@W95Psp W95Psp enabled auto-merge October 22, 2024 12:13
@W95Psp W95Psp added this pull request to the merge queue Oct 22, 2024
Merged via the queue into main with commit 1f6a973 Oct 22, 2024
13 checks passed
@W95Psp W95Psp deleted the rust-generic-printer branch October 22, 2024 12:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@cmester0 cmester0 cmester0 approved these changes

@franziskuskiefer franziskuskiefer franziskuskiefer left review comments

Assignees
No one assigned
Labels
None yet
Projects
No open projects
hax
Status: No status
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Generic printer: optionally output source maps
3 participants
@W95Psp @franziskuskiefer @cmester0