Coq native_compute not working under NixOS

mgttlinger commented 6 years ago

Issue description

When evaluating Coq expressions using the native executor it fails do compile. Likely due to some executable or dependency not being found at runtime. See https://github.com/coq/coq/issues/6699

Steps to reproduce

nix-shell -p coq --run "echo 'Eval native_compute in (1+1).' > test.v ; coqc test.v"

Technical details

Coq 8.7.1

system: "x86_64-linux"
host os: Linux 4.9.76, NixOS, 17.09.2862.dab46ac5e2f (Hummingbird)
multi-user?: yes
sandbox: yes
version: nix-env (Nix) 1.11.16
channels(merlin): ""
channels(root): "nixos-17.09.2862.dab46ac5e2f, nixos-unstable-18.03pre123130.1bc288591ea"
nixpkgs: /nix/var/nix/profiles/per-user/root/channels/nixos/nixpkgs

dtzWill commented 6 years ago

strace and find out what tools/libs it wants but can't find?

mgttlinger commented 6 years ago

Interesting. In the nix-shell it uses coq version 8.6.1 and is missing ocamlfind (seems to be looking for it in path). In my local installation from unstable it seems to find ocamlfind but then fails because some file in tmp is missing. This is interresting because at compile time it saves the paths of its executable which (at least in my installation) contains the correct paths in the nix store.

Zimmi48 commented 6 years ago

A dumb fix would consist in just propagating the ocaml and findlib build inputs. I just tested it to confirm it solved the issue.

Zimmi48 commented 6 years ago

I could reproduce your problem using the default.nix provided in the master branch of the Coq repository:

$(nix-build --arg pkgs "import <unstable> {}" --arg doCheck false --no-out-link)/bin/coqc test.v

gives:

File "/tmp/Coq_native4d641c.native", line 1:
Error: /nix/store/zm1nwr84j07wbldsshbfmc3ikrf6kp7n-coq/lib/coq/kernel/nativevalues.cmi
is not a compiled interface for this version of OCaml.
It seems to be for an older version of OCaml.
File "test.v", line 1, characters 0-29:
Warning: Native compiler exited with status 2
[native-compiler-failed,native-compiler]
File "test.v", line 1, characters 0-29:
Error: Anomaly "Compilation failure."
Please report at http://coq.inria.fr/bugs/.

EDIT: and in this case, moving ocaml and findlib from buildInputs to propagatedBuildInputs doesn't fix it.

dtzWill commented 6 years ago

propagatedBuildInputs only come into play when building things that use the current derivation as a buildInput. So they won't be "propagated" anywhere when installing, but for "reasons" would be available in the nix-shell command posted at the top.

Note that directly invoking paths from the nix-store as you do there ($(nix-build ...)/bin/command) is often not going to work, although usually it does. The primary supported way to run things is to install them with nix-env or enter a shell with them as inputs.

Possible solutions:

Indicate to coq at build-time where it can find these tools. If that's not easily done/supported, a commonly used approach is using makeWrapper to wrap things with scripts that set PATH appropriately (other variables, such as LD_LIBRARY_PATH, are sometimes set). Wrapped tools are "self-contained".
Use propagatedUserEnvPkgs--this is a bit of a last resort but is straightforward as it basically says "install these packages when installing this". The reason this is "last resort" is that it causes conflicts that otherwise wouldn't exist if things were properly self-contained.

vbgl commented 6 years ago

I believe that native_compute does work on NixOS. It only depends, at run-time, on coq.ocaml (aka the version of OCaml that has been used to build Coq).

There are indeed two ways to make the user experience less surprising: either wrap the Coq binaries (coqtop, coqc, coqtop.byte, etc.) to ensure that the right OCaml tools can be found; or fix the way these tools are searched (e.g., as is done for csdp).

Quick work-around: add coq.ocaml in your shell (nix-shell -p coq coq.ocaml …).

Zimmi48 commented 6 years ago

I tried patching the code to put the absolute path to the OCaml compiler but it just failed with:

sh: as : commande introuvable
File "/tmp/Coq_native17312b.native", line 1:
Error: Assembler error, input left in file /tmp/camlasm709f2d.s

so knowing where the OCaml tools are is not enough.

Moreover, the native compiler is not the only thing failing because it cannot find OCaml. The command Extraction TestCompile fails in the same way, although it may be less surprising to the user that it does.

stale[bot] commented 4 years ago

Thank you for your contributions.

This has been automatically marked as stale because it has had no activity for 180 days.

If this is still important to you, we ask that you leave a comment below. Your comment can be as simple as "still important to me". This lets people see that at least one person still cares about this. Someone will have to do this at most twice a year if there is no other activity.

Here are suggestions that might help resolve this more quickly:

Search for maintainers and people that previously touched the related code and @ mention them in a comment.
Ask on the NixOS Discourse.
Ask on the #nixos channel on irc.freenode.net.

mgttlinger commented 4 years ago

Given that the issue is still present, I would leave the issue open.

Zimmi48 commented 4 years ago

I suggest applying the propagatedUserEnvPkg solution. The conflicts that it creates make complete sense. If you let people install any version of Coq with any version of OCaml in the same environment, you are letting the users get into trouble anyway (e.g. trying to build a plugin without realizing that they need to use coq.ocaml, etc.). See also: https://github.com/coq/coq/blob/master/INSTALL.md#ocaml-toolchain-advisory

Zimmi48 commented 3 years ago

The fix has been reverted. See https://github.com/NixOS/nixpkgs/pull/101058#issuecomment-718045405 for the reason.

stale[bot] commented 3 years ago

I marked this as stale due to inactivity. → More info

mgttlinger commented 3 years ago

Given that the fix was reverted I'd say the issue should at least stay for reference

NixOS / nixpkgs