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
framac: 18 -> 19 and update why3 #63494
Conversation
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.
Thank you for making maintaining the Frama-C package!
If your are interested here a setupHook
for allowing to load installed external Frama-C plugins:
setupHook = pkgs.writeText "setupHook.sh" ''
addFramaCPath () {
if test -d "''$1/lib/frama-c/plugins"; then
export FRAMAC_PLUGIN="''${FRAMAC_PLUGIN}''${FRAMAC_PLUGIN:+:}''$1/lib/frama-c/plugins"
export OCAMLPATH="''${OCAMLPATH}''${OCAMLPATH:+:}''$1/lib/frama-c/plugins"
fi
if test -d "''$1/lib/frama-c"; then
export OCAMLPATH="''${OCAMLPATH}''${OCAMLPATH:+:}''$1/lib/frama-c"
fi
if test -d "''$1/share/frama-c/"; then
export FRAMAC_EXTRA_SHARE="''${FRAMAC_EXTRA_SHARE}''${FRAMAC_EXTRA_SHARE:+:}''$1/share/frama-c"
fi
}
addEnvHooks "$targetOffset" addFramaCPath
'';
One strange point during the installation of frama-c plugins is:
installPhase = ''
make install prefix=$out
Looks pretty good at a first glance! I think investigating the plugin |
@bobot I'm not so familiar with external Frama-C plugins, but I'll take your word for it and throw it in. Not sure how to test it though. |
I can give you an empty plugin, but I'm checking if we have a real plugin ready to be released for the new version of Frama-C. It could more interesting. Just a question: Is the path to external programs such as coq, coqide and why3 hard-coded in the compiled frama-c for nix? Should it be? |
Right now it's not, but it feels like that's the right way to do it. Instead I just make sure to install the provers as well so they're in the path. How would we go about making why3 use absolute paths? I feel like we could either replace relative paths in the config or we could generate the config by hand. Thoughts? |
We can hard-code their path in |
Right, but how do we get those hardcoded paths into the config file? |
I think whether you prefer to use One question is, can why3 load/merge multiple config files? I.e. if I point it to load |
I agree. I really don't know enough about the
I think that using the
|
I would have put them directly in the why3-config binary (src/driver/autodetection.ml), but I forgot that why3 is just a dependency of the second package. Another possibility than (NB: if you have ideas how why3 could be modified to help you, don't hesitate to describe the ways) |
Hmm, one of my goals was to avoid having the user run
Although I'd like to avoid it, we can still modify the |
15dfec2
to
b101d56
Compare
Okay, I think this is good to go. I managed to substitute for absolute paths in the |
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.
Running frama-c-gui crashes with:
[kernel] User Error: [findlib] package 'num' not found (required by `why3')
@vbgl Sorry for the delay, I think I've addressed all of your comments. |
@GrahamcOfBorg build framac |
Motivation for this change
Update
framac
to 19 (being released this Friday), clean upwhy3
and make sure it works well withframac
, and addwhy3WithProvers
to automatically configure provers forwhy3
.Things done
sandbox
innix.conf
on non-NixOS)nix-shell -p nix-review --run "nix-review wip"
./result/bin/
)nix path-info -S
before and after)