Stream: Nix toolbox devs & users

Topic: Coq with nix


view this post on Zulip Julin S (Jul 08 2022 at 05:53):

HI. I had been trying use coq via nix.

But I had got it installed with nix-env and saw at https://nixos.org/guides/nix-pills/developing-with-nix-shell.html that it is not the best way.

Which other way would be good?

I am a total novice at nix, but had been using it without really knowing what is happening underneath. It worked okay till I tried install mathcomp library. But it wouldn't show up even when coq is there.

view this post on Zulip Julin S (Jul 08 2022 at 05:55):

Found the stuff at https://github.com/coq-community/coq-nix-toolbox/ but had been hoping to have something more basic that we ourselves write. So that we would be in a position to at least attempt to fix it when something goes wrong.

view this post on Zulip Julin S (Jul 08 2022 at 06:55):

I guess metacoq is not in nix.

view this post on Zulip Julin S (Jul 08 2022 at 07:11):


I tried this as shell.nix:

{ pkgs ? import <nixpkgs> {} }:
  pkgs.mkShell {
    nativeBuildInputs = [
      pkgs.coq_8_13
      pkgs.coqPackages.mathcomp
    ];
}

and did nix-shell default.nix.

The resulting shell has coqc v8.13 but it can't get mathcomp:

[nix-shell:~]$ coqtop
Welcome to Coq 8.13.2 (January 1980)

Coq < From mathcomp Require Import all_ssreflect.
Toplevel input, characters 29-42:
> From mathcomp Require Import all_ssreflect.
>                              ^^^^^^^^^^^^^
Error: Cannot find a physical path bound to logical path matching suffix
<> and prefix mathcomp.

Any idea why this is happening?

view this post on Zulip Julin S (Jul 08 2022 at 07:38):

I haven't got any opam package installations now, but can opam installations and nix packages work together?

view this post on Zulip Cyril Cohen (Jul 08 2022 at 11:01):

pkgs.coqPackages might not be the one for 8.13. (I cannot remember what is the default at the current master or unstable version of nixpkgs)
You should either do:

{ pkgs ? import <nixpkgs> {} }:
  pkgs.mkShell {
    nativeBuildInputs = [
      pkgs.coq
      pkgs.coqPackages.mathcomp
    ];
}

or

{ pkgs ? import <nixpkgs> {} }:
  pkgs.mkShell {
    nativeBuildInputs = [
      pkgs.coq_8_13
      pkgs.coqPackages_8_13.mathcomp
    ];
}

But not mix versions...

view this post on Zulip Cyril Cohen (Jul 08 2022 at 11:02):

Another way to write it in a more "uniform way" is:

{ pkgs ? import <nixpkgs> {} }:
  pkgs.mkShell {
    nativeBuildInputs = with pkgs.coqPackages; [ coq mathcomp ];
}

view this post on Zulip Cyril Cohen (Jul 08 2022 at 11:37):

Julin S said:

I guess metacoq is not in nix.

It is: https://github.com/NixOS/nixpkgs/blob/f59089e254e45b509509cf3eeb9334006c00db6b/pkgs/top-level/coq-packages.nix#L83

view this post on Zulip Théo Zimmermann (Jul 08 2022 at 18:43):

You don't even need a shell.nix. You can just do nix-shell -p coq_8_13 coqPackages_8_13.mathcomp and it should work.

view this post on Zulip Julin S (Jul 13 2022 at 03:49):

I wonder why the metacoq package is not showing up in search.nixos.org?

I searched 'metacoq' but it said 'no packages found'.

(Sorry had to be away for a few days.)

view this post on Zulip Julin S (Jul 13 2022 at 03:55):

And doing using the nix file that Cyril mentioned made mathcomp work as well.
Thanks!

view this post on Zulip Julin S (Jul 13 2022 at 03:57):

How would we install metacoq via nix though?

I tried this:

{ pkgs ? import <nixpkgs> {} }:
  pkgs.mkShell {
    nativeBuildInputs = [
      pkgs.coq_8_13
      pkgs.coqPackages_8_13.mathcomp
      pkgs.coqPackages_8_13.metacoq
    ];
}

But that said 'attribute metacoq missing'.

view this post on Zulip Julin S (Jul 13 2022 at 04:00):

Oh I see that metacoq was a recent addition to nix: https://github.com/NixOS/nixpkgs/pull/162639

view this post on Zulip Julin S (Jul 13 2022 at 04:00):

And I'm using an old nix channel (21.11) maybe that's the reason?

view this post on Zulip Julin S (Jul 13 2022 at 04:02):

But why isn't metacoq showing up at nix.search.org though? Even in unstable channel.

view this post on Zulip Théo Zimmermann (Jul 13 2022 at 10:45):

No, that's not the actually reason. The reason is that the version of metacoq compatible with Coq 8.13 is not activated in coqPackages by default.

view this post on Zulip Théo Zimmermann (Jul 13 2022 at 10:45):

See https://github.com/NixOS/nixpkgs/blob/f59089e254e45b509509cf3eeb9334006c00db6b/pkgs/development/coq-modules/metacoq/default.nix#L11-L12

view this post on Zulip Théo Zimmermann (Jul 13 2022 at 10:46):

However, this version is still available. You can get it by doing a package override.

view this post on Zulip Théo Zimmermann (Jul 13 2022 at 10:50):

Though, you also need to override the equations version according to this comment, and I'm not completely sure how to do this without relying on the Coq Nix Toolbox.

view this post on Zulip Théo Zimmermann (Jul 13 2022 at 10:53):

Another solution would be to add versions 1.0 for Coq 8.14 and 8.15. This would avoid having to override the Equations version.


Last updated: Dec 05 2023 at 04:01 UTC