-
Notifications
You must be signed in to change notification settings - Fork 152
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
Allow bison parsers to be generated as libraries #3259
Conversation
525bb35
to
588890f
Compare
a944fd9
to
4fa4cbe
Compare
* llvm-backend/src/main/native/llvm-backend: f137e48 - Run on ephemeral runner (#709) * Sync flake inputs to submodules * llvm-backend/src/main/native/llvm-backend: 39a9043 - Write initial documentation for "backend as a library" (#707) * Sync flake inputs to submodules * llvm-backend/src/main/native/llvm-backend: e29384e - Duplicate dependabot PR #687 (#706) * Sync flake inputs to submodules * Update Nix lock files --------- Co-authored-by: rv-jenkins <devops@runtimeverification.com> Co-authored-by: Bruce Collie <brucecollie82@gmail.com>
4fa4cbe
to
305d03b
Compare
I'd like to review this, but I might not get to it until next week. Is this blocking anything currently? |
No, I'm only using it in the context of my own work on a blog post; I'm using |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A few questions.
Java part looks fine.
The C part I'm not that familiar with.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I went over the C code and the regression test and it all looks good to me.
This PR threads the new options from runtimeverification/k#3259 through `kbuild` and `Kompile`. --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
This PR threads the new options from #3259 through `kbuild` and `Kompile`. --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
This PR threads the new options from #3259 through `kbuild` and `Kompile`. --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
This PR threads the new options from #3259 through `kbuild` and `Kompile`. --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
This PR threads the new options from #3259 through `kbuild` and `Kompile`. --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
This PR threads the new options from #3259 through `kbuild` and `Kompile`. --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
Fixes #3258
This PR is related to my ongoing work towards documenting "K as a library" (i.e. using the LLVM backend to generate libraries users can use to build their own tools, rather than relying on the K scripts to run their programs. One missing link in the existing toolchain that I identified was generating KORE from a surface program; doing so currently would require the user to shell out to one of the bison-generated parsers. This PR makes a small improvement to that workflow by allowing the bison parsers to be generated as shared libraries rather than as executables; the parser libraries can then be shipped alongside the C bindings libraries for user definitions.
After this PR, users will be able to run something like:
to generate a pair of shared libraries (
libfoo.so
,libparse_KItem_TEST.so
) that provide an LLVM backend runtime and GLR Bison parser, respectively. These can then be embedded into an application.The changes in this PR are as follows:
writer
type; this lets us output to a file directly as before for best performance, but also to keep the parsed KORE in memory if required.char *parse_SORT(...)
as well as the existing bisonmain
entrypoint.