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

coq: also install ocaml and findlib #101058

Merged
merged 1 commit into from Oct 21, 2020
Merged

coq: also install ocaml and findlib #101058

merged 1 commit into from Oct 21, 2020

Conversation

@Zimmi48
Copy link
Member

@Zimmi48 Zimmi48 commented Oct 19, 2020

Motivation for this change

Fix #34657.

native_compute does not work without OCaml and findlib being installed in the user environment.
By installing more packages, this may create installation conflicts, but I argued (in #34657) that these conflicts are fine because if a user has an incompatible OCaml version in scope, they may face even more surprising issues when trying to use native_compute or to build a plugin.

Things done
  • Tested using sandboxing (nix.useSandbox on NixOS, or option sandbox in nix.conf on non-NixOS linux)
  • 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 nixpkgs-review --run "nixpkgs-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)
  • Ensured that relevant documentation is up to date
  • Fits CONTRIBUTING.md.
@vbgl
Copy link
Contributor

@vbgl vbgl commented Oct 19, 2020

Does this change the closure size?

propagatedBuildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib ]
++ stdenv.lib.optional (versionAtLeast "8.12") ocamlPackages.num;

propagatedUserEnvPkgs = [ ocamlPackages.ocaml ocamlPackages.findlib ];
Copy link
Contributor

@vbgl vbgl Oct 19, 2020

Where is this attribute documented? What’s the relation to propagatedBuildInputs? Why is its value different?

Copy link
Member Author

@Zimmi48 Zimmi48 Oct 19, 2020

I didn't know about this attribute, it is a suggestion from @dtzWill in #34657. I also needed to extend propagatedBuildInput to resolve the issue inside a nix-shell -p coq and not just when people install Coq. I don't know if there will be limitations due to num not being installed but it is well known that Nix-installed libraries do not work outside a nix-shell anyway, so there is really no reason to include num in propagatedUserEnvPkgs.

@Zimmi48
Copy link
Member Author

@Zimmi48 Zimmi48 commented Oct 19, 2020

Closure-size after:

$ nix path-info . -S coq
/nix/store/a8zxmd6fn0mbnp5lafikk78yryw4nlz4-coq-8.11.2	 1307429840

Before:

$ nix path-info . -S coq
/nix/store/xsjvvm0y8gswllhb6z8h4w366h0xfwq4-coq-8.11.2	 1307429136

@vbgl
Copy link
Contributor

@vbgl vbgl commented Oct 21, 2020

@GrahamcOfBorg build framac satallax

@vbgl vbgl merged commit 5d0e2de into NixOS:master Oct 21, 2020
19 of 20 checks passed
@vbgl
Copy link
Contributor

@vbgl vbgl commented Oct 21, 2020

As this is a fix, should it be ported to 20.09? (I can do it).

@Zimmi48
Copy link
Member Author

@Zimmi48 Zimmi48 commented Oct 21, 2020

It is a fix, yes, but it introduces a slight incompatibility, so I would say no. (It is easy to workaround the problem anyway.)

@vbgl
Copy link
Contributor

@vbgl vbgl commented Oct 21, 2020

OK, thanks!

Zimmi48 added a commit to Zimmi48/coq that referenced this issue Oct 22, 2020
This allows native_compute to work and is the same fix that was
applied to the nixpkgs repo in NixOS/nixpkgs#101058.
@Zimmi48 Zimmi48 deleted the fix-34657 branch Oct 22, 2020
@vbgl
Copy link
Contributor

@vbgl vbgl commented Oct 28, 2020

I would like to revert this.

Use case: develop a program in OCaml with some modules extracted from a Coq development. You cannot have in the same (nix) environment the tools to develop both Coq & OCaml parts due to conflicting versions of OCaml: the one propagated from Coq (that you don’t want to change because of the binary cache) and the one for your local development (that you want to change, e.g., to test compatibility with different versions, to enable flamdba or other goodies).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked issues

Successfully merging this pull request may close these issues.

2 participants