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

Conversation

@jbaum98
Copy link
Contributor

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.

@jbaum98 jbaum98 force-pushed the jbaum98:framac-why3 branch from 41950e7 to 1c5b69a Jun 19, 2019

@ofborg ofborg bot requested review from vbgl and thoughtpolice Jun 19, 2019

@jbaum98 jbaum98 changed the title WIP: framac: 18 -> 19 and update why3 [WIP] framac: 18 -> 19 and update why3 Jun 19, 2019

@bobot
Copy link

left a comment

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

This comment has been minimized.

Copy link
Member

commented Jun 19, 2019

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.

Convinced of the error of my ways

@jbaum98 jbaum98 force-pushed the jbaum98:framac-why3 branch from 1c5b69a to 86da5df Jun 20, 2019

@jbaum98

This comment has been minimized.

Copy link
Contributor Author

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 Jun 20, 2019

@bobot

This comment has been minimized.

Copy link

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

This comment has been minimized.

Copy link
Contributor Author

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

This comment has been minimized.

Copy link

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

This comment has been minimized.

Copy link
Contributor Author

commented Jun 20, 2019

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

@thoughtpolice

This comment has been minimized.

Copy link
Member

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.

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

This comment has been minimized.

Copy link
Contributor Author

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

This comment has been minimized.

Copy link

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

This comment has been minimized.

Copy link
Contributor Author

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 jbaum98:framac-why3 branch 2 times, most recently from 15dfec2 to b101d56 Jun 24, 2019

@jbaum98

This comment has been minimized.

Copy link
Contributor Author

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.

@vbgl
Copy link
Contributor

left a comment

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 jbaum98 force-pushed the jbaum98:framac-why3 branch from b101d56 to d82a0f2 Aug 1, 2019

@jbaum98

This comment has been minimized.

Copy link
Contributor Author

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 Aug 1, 2019

@thoughtpolice thoughtpolice changed the title [WIP] framac: 18 -> 19 and update why3 framac: 18 -> 19 and update why3 Aug 2, 2019

@vbgl

This comment has been minimized.

Copy link
Contributor

commented Aug 3, 2019

@GrahamcOfBorg build framac

@vbgl
vbgl approved these changes Aug 3, 2019

@vbgl vbgl merged commit 3ab32ee into NixOS:master Aug 3, 2019

16 checks passed

Evaluation Performance Report Evaluator Performance Report
Details
framac on aarch64-linux Success
Details
framac on x86_64-darwin Success
Details
framac on x86_64-linux Success
Details
grahamcofborg-eval ^.^!
Details
grahamcofborg-eval-check-maintainers matching changed paths to changed attrs...
Details
grahamcofborg-eval-check-meta config.nix: checkMeta = true
Details
grahamcofborg-eval-darwin nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="ofborg"; } ./pkgs/top-level/release.nix -A darwin-tested
Details
grahamcofborg-eval-nixos nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="ofborg"; } ./nixos/release-combined.nix -A tested
Details
grahamcofborg-eval-nixos-manual nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="ofborg"; } ./nixos/release.nix -A manual
Details
grahamcofborg-eval-nixos-options nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="ofborg"; } ./nixos/release.nix -A options
Details
grahamcofborg-eval-nixpkgs-manual nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="ofborg"; } ./pkgs/top-level/release.nix -A manual
Details
grahamcofborg-eval-nixpkgs-tarball nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="ofborg"; } ./pkgs/top-level/release.nix -A tarball
Details
grahamcofborg-eval-nixpkgs-unstable-jobset nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="ofborg"; } ./pkgs/top-level/release.nix -A unstable
Details
grahamcofborg-eval-package-list nix-env -qa --json --file .
Details
grahamcofborg-eval-package-list-no-aliases nix-env -qa --json --file . --arg config { allowAliases = false; }
Details
@vbgl vbgl referenced this pull request Aug 3, 2019
3 of 10 tasks complete

@jbaum98 jbaum98 deleted the jbaum98:framac-why3 branch Aug 3, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
5 participants
You can’t perform that action at this time.