Remove dynlink and findlib dependencies from goblint-cil library #170
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Are there ambitions to merge this? It looks like it breaks OS X support? |
|
I'll re-run the CI to see what the issue was, perhaps just some MacOS CI problem. I think this should be done because it's silly for (parts of) the OCaml compiler be included when using goblint-cil. But this PR shouldn't be part of the SV-COMP-equivalent release anyway. |
michael-schwarz
approved these changes
Dec 24, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
In ocsigen/js_of_ocaml#1641 it was pointed out that Gobview is trying to link dynamic library linking (
Dynlink), which can (besides that issue) also increase Gobview size becauseDynlinksomehow includes OCaml compiler libraries.This is completely unnecessary: the goblint-cil library doesn't use dynlink and findlib at all. Only some CIL executable uses those to detect
Features at runtime (as opposed to linking them in with-linkalllike we do). This PR splits theFeaturemodule to avoid these dependencies.