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

Jump to bottom

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 •
edited

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 commented Oct 19, 2020

Does this change the closure size?

vbgl
vbgl reviewed Oct 19, 2020
View reviewed changes
pkgs/applications/science/logic/coq/default.nix
propagatedBuildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib ]
++ stdenv.lib.optional (versionAtLeast "8.12") ocamlPackages.num;

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 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 commented Oct 21, 2020

@GrahamcOfBorg build framac satallax

@vbgl vbgl merged commit 5d0e2de into NixOS:master Oct 21, 2020
@vbgl
Copy link
Contributor

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 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 commented Oct 21, 2020

OK, thanks!

Zimmi48 added a commit to Zimmi48/coq that referenced this pull request Oct 22, 2020
@Zimmi48
[default.nix] Propagate OCaml and findlib to user env.
a2ee2a6 
This allows native_compute to work and is the same fix that was
applied to the nixpkgs repo in NixOS/nixpkgs#101058.
@Zimmi48 Zimmi48 mentioned this pull request Oct 22, 2020
Merged
@Zimmi48 Zimmi48 deleted the fix-34657 branch October 22, 2020 11:47
@vbgl
Copy link
Contributor

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

@vbgl vbgl mentioned this pull request Oct 28, 2020
Merged
10 tasks
@Zimmi48 Zimmi48 mentioned this pull request Oct 31, 2020
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@vbgl vbgl vbgl left review comments

@roconnor roconnor Awaiting requested review from roconnor

@thoughtpolice thoughtpolice Awaiting requested review from thoughtpolice

Assignees
No one assigned
Labels
10.rebuild-darwin: 11-100 10.rebuild-linux: 11-100 11.by: package-maintainer
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Coq native_compute not working under NixOS
2 participants
@Zimmi48 @vbgl