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.

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

Merged
merged 1 commit into from Aug 3, 2019
Merged

framac: 18 -> 19 and update why3 #63494

merged 1 commit into from Aug 3, 2019

Conversation

jbaum98
Copy link
Contributor

@jbaum98 jbaum98 commented Jun 19, 2019

Motivation for this change

Update framac to 19 (being released this Friday), clean up why3 and make sure it works well with framac, and add why3WithProvers to automatically configure provers for why3.

Things done
  • Tested using sandboxing (nix.useSandbox on NixOS, or option sandbox in nix.conf on non-NixOS)
  • Built on platform(s)
    • NixOS
    • macOS
    • other Linux distributions
  • Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
  • Tested compilation of all pkgs that depend on this change using nix-shell -p nix-review --run "nix-review wip"
  • Tested execution of all binary files (usually in ./result/bin/)
  • Determined the impact on package closure size (by running nix path-info -S before and after)
  • Assured whether relevant documentation is up to date
  • Fits CONTRIBUTING.md.

@ofborg ofborg bot requested review from vbgl and thoughtpolice June 19, 2019 02:10
@jbaum98 jbaum98 changed the title WIP: framac: 18 -> 19 and update why3 [WIP] framac: 18 -> 19 and update why3 Jun 19, 2019
Copy link
Contributor

@bobot bobot left a 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

pkgs/applications/science/logic/why3/with_provers.nix Outdated Show resolved Hide resolved
@thoughtpolice
Copy link
Member

Looks pretty good at a first glance! I think investigating the plugin setupHook would also be very useful and easy to add, but feel free to follow up with a separate PR, etc for that, if you like.

@thoughtpolice thoughtpolice dismissed their stale review June 19, 2019 23:08

Convinced of the error of my ways

@jbaum98
Copy link
Contributor Author

jbaum98 commented Jun 20, 2019

@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.

@ofborg ofborg bot requested a review from thoughtpolice June 20, 2019 03:42
@bobot
Copy link
Contributor

bobot commented Jun 20, 2019

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?

@jbaum98
Copy link
Contributor Author

jbaum98 commented Jun 20, 2019

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?

@bobot
Copy link
Contributor

bobot commented Jun 20, 2019

We can hard-code their path in why3 config so that they are found even if they are not in the path.

@jbaum98
Copy link
Contributor Author

jbaum98 commented Jun 20, 2019

Right, but how do we get those hardcoded paths into the config file?

@thoughtpolice
Copy link
Member

I think whether you prefer to use substituteInPlace on the config file or write a bespoke config using pkgs.writeText and then wrap the executable with makeWrapper is up to you, honestly. If the configuration isn't especially complicated I'd probably use pkgs.writeText as it's a little less fragile, but you'd have to play with it.

One question is, can why3 load/merge multiple config files? I.e. if I point it to load provers.conf (containing a bunch of hardcoded absolute store paths), can I also load $HOME/.config/why3.conf (or whatever) too, and have the values merged? That would be the ideal case: we could just write out part of a config file that specifies the solver paths, and let other config options default/use what the user specifies.

@jbaum98
Copy link
Contributor Author

jbaum98 commented Jun 20, 2019

I think whether you prefer to use substituteInPlace on the config file or write a bespoke config using pkgs.writeText and then wrap the executable with makeWrapper is up to you, honestly. If the configuration isn't especially complicated I'd probably use pkgs.writeText as it's a little less fragile, but you'd have to play with it.

I agree. I really don't know enough about the why3 configuration language though, and how smart why config --detect-provers is. So I'll see if I can rig up something with pkgs.writeText, but I'm curious if you guys know more about why3 and have opinions about if that's feasible/robust or not.

One question is, can why3 load/merge multiple config files? I.e. if I point it to load provers.conf (containing a bunch of hardcoded absolute store paths), can I also load $HOME/.config/why3.conf (or whatever) too, and have the values merged? That would be the ideal case: we could just write out part of a config file that specifies the solver paths, and let other config options default/use what the user specifies.

I think that using the --extra-config argument, as François suggested, takes care of this. I haven't tested it with another config, but it gives the following reassuring message when I run why3:

[Config] reading extra configuration file /nix/store/...-why3-1.2.0-with-provers-conf/share/why3/why3.conf

@bobot
Copy link
Contributor

bobot commented Jun 20, 2019

Right, but how do we get those hardcoded paths into the config file?

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 --extra-config could be just to wrap why3-config with adding to the $PATH the hardcoded bin directory of each provers. The user still need to run why3 config --detect as usual, but nothing else fancy.

(NB: if you have ideas how why3 could be modified to help you, don't hesitate to describe the ways)

@jbaum98
Copy link
Contributor Author

jbaum98 commented Jun 20, 2019

The user still need to run why3 config --detect as usual, but nothing else fancy.

Hmm, one of my goals was to avoid having the user run why3 config --detect. This is because if you are installing different versions of why3, you run into problems if you forgot to delete and regenerate your config, and I wanted nix to handle that for you.

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.

Although I'd like to avoid it, we can still modify the why3 that is passed to us with some kind of patch that we generate, forcing it to be recompiled from source. In some ways that's actually cleaner.

@jbaum98 jbaum98 force-pushed the framac-why3 branch 2 times, most recently from 15dfec2 to b101d56 Compare June 24, 2019 18:19
@jbaum98
Copy link
Contributor Author

jbaum98 commented Jun 24, 2019

Okay, I think this is good to go. I managed to substitute for absolute paths in the why3 using a generated awk script, and I think it works, so now I don't have to install the provers. I've squashed everything into one commit.

Copy link
Contributor

@vbgl vbgl left a 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')

pkgs/applications/science/logic/why3/default.nix Outdated Show resolved Hide resolved
pkgs/top-level/all-packages.nix Outdated Show resolved Hide resolved
@jbaum98
Copy link
Contributor Author

jbaum98 commented Aug 1, 2019

@vbgl Sorry for the delay, I think I've addressed all of your comments.

@ofborg ofborg bot requested a review from vbgl August 1, 2019 05:43
@thoughtpolice thoughtpolice changed the title [WIP] framac: 18 -> 19 and update why3 framac: 18 -> 19 and update why3 Aug 2, 2019
@vbgl
Copy link
Contributor

vbgl commented Aug 3, 2019

@GrahamcOfBorg build framac

@vbgl vbgl merged commit 3ab32ee into NixOS:master Aug 3, 2019
@vbgl vbgl mentioned this pull request Aug 3, 2019
10 tasks
@jbaum98 jbaum98 deleted the framac-why3 branch August 3, 2019 16:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

5 participants