Building PeaCoq on NixOS

[Zimmi48]

Hi Valentin,

When I saw this today, I was quite happy:

PEACOQ: This seems to be NixOS, use nix-shell before calling setup.sh or set NIXSHELL

But to get there, I had to guess that I needed to call ./setup.sh before nix-shell. Indeed, shell.nix depends on peacoq-server/peacoq-server.nix but this file doesn't exist until we clone the appropriate repository, something that ./setup.sh does for us if we give it the chance (but since it appears later in the instructions, we don't immediately think to call it). So I think the instructions for building on NixOS could be improved a bit.

But my problems were not over...

I had to do opam init --comp 4.02.3 after nix-shell because this wasn't done automatically for me. (And to do so I had first to add unzip to the list of dependencies. This is apparently a run-time dependency of opam, maybe we should report this to NixOS/nixpkgs). I needed also ocamlfind but couldn't install it with opam for some reason, even after adding ncurses to shell.nix. I tried to add ocamlPackagess.findlib to shell.nix and this seemed to have solved the problem but later the build of Coq failed miserably with a cryptic error which is probably related to ocamlfind.

I also tried to give up opam and use Nix packages only (which is what I do when I'm hacking Coq). The problem that I found (and which is probably the reason you now use opam) is that SerAPI needs OCaml 4.02 but apparently, as you remarked, ocamlPackages.camlp5 needs OCaml 4.01.

Finally, a last remark: in setup.sh, check-and-clone "peacoq-plugin" should come before ./scripts/setup-coq.sh which is a symlink to a file in peacoq-plugin/.

[Zimmi48]

Digging a bit more I found a few pieces of info that seem to show that there is no point in using Opam with Nix: https://github.com/NixOS/nixpkgs/issues/14466 I'll make some tests and maybe submit a PR to make shell.nix not rely on Opam.

[Ptival]

Hey Théo,

A patch for this would be awesome. I haven't digged into it, but yeah, the less "setup" we need, the better it is.

[Zimmi48]

Still working on this: I have submitted a PR to add a missing OCaml package SerAPI depends on to nixpkgs (https://github.com/NixOS/nixpkgs/pull/20164). Once this is merged, I should be able to submit a PR listing all dependencies without Opam.

[Zimmi48]

By the way, I see that you have clones of various Haskell packages with Nix derivations. Is there a reason for not integrating these upstream (in nixpkgs)?

[Ptival]

Do you mean all the snap-framework-related packages?

At the time, I think I wanted to use the newer version (1.0) that was not yet released on hackage.

Then I don't remember but I encountered all sorts of errors with zlib, so I ended up not touching it as soon as it worked. I have to try upstream and see if I can remove all this crazy logic yeah... You can try if you want.

[Zimmi48]

Yes, this is what I mean. I have not much experience with Nix and Haskell but I might try (not next week though, I'm going to be too busy for that).

[Zimmi48]

So #42 is the promised PR replacing Opam with Nix.

I'm thinking that something similar could be achieved for npm as well, but we'll see.

Also, it could make sense to see if we can provide just a Nix derivation for SerAPI instead of cloning it and building it like setup.sh does currently. But I think it is safer to wait for https://github.com/ejgallego/coq-serapi/issues/25 to get closed first, and this is depending on 8.6beta1 getting out, which I hope will be in the beginning of next week.

Finally, let me mention that while I think my PR is fine, I am not too sure because I don't reach the point where I can execute and test PeaCoq yet. The compilation seems to be going fine. I even reach the point where .PeaCoqConfig.hs is created in my homedir, but there isn't any ./peacoq to execute so maybe something has failed that prevented that.

[Ptival]

Oh yeah, currently the server would be in peacoq-server/dist or something, it does not get symlinked to the top-level directory.

On my phone right now, will check in ~1 hour.

Thanks for the PR!

On Thu, Nov 10, 2016, 09:17 Théo Zimmermann [email protected] wrote:

So #42 https://github.com/Ptival/PeaCoq/pull/42 is the promised PR replacing Opam with Nix.

I'm thinking that something similar could be achieved for npm as well, but we'll see.

Also, it could make sense to see if we can provide just a Nix derivation for SerAPI instead of cloning it and building it like setup.sh does currently. But I think it is safer to wait for ejgallego/coq-serapi#25 https://github.com/ejgallego/coq-serapi/issues/25 to get closed first, and this is depending on 8.6beta1 getting out, which I hope will be in the beginning of next week.

Finally, let me mention that while I think my PR is fine, I am not too sure because I don't reach the point where I can execute and test PeaCoq yet. The compilation seems to be going fine. I even reach the point where .PeaCoqConfig.hs is created in my homedir, but there isn't any ./peacoq to execute so maybe something has failed that prevented that.

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/Ptival/PeaCoq/issues/38#issuecomment-259750561, or mute the thread https://github.com/notifications/unsubscribe-auth/AAdNjrrRXQj3mogLX1qKhwZvXzT4AA9Cks5q81GYgaJpZM4KdsqS .

[ejgallego]

@Zimmi48 , I'll be happy to provide a NiX derivation for SerAPI.

How is Coq installed with NiX ?

[Zimmi48]

@ejgallego Thanks for the interest ;)

Coq has its own Nix derivation, which would allow SerAPI's derivation to depend on it. Actually it has one distinct derivation per version (one for 8.3, one for 8.4, one for 8.5) and we would need to wait for the derivation for 8.6 to be added so that we can rely on it (but I'm guessing it will be added shortly after the beta-release as the maintainers of the Coq packages in nixpkgs are quite reactive.

[ejgallego]

@Zimmi48 ok, I'll add Nix support when Coq 8.6 makes into Nix.

[ejgallego]

For the shorter term, doing opam install coq-serapi will be working very soon.