Julin S (Jul 08 2022 at 05:53): 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.
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.
Julin S (Jul 08 2022 at 06:55):I guess metacoq is not in nix.
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?
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?
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...
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 ];
}
Julin S said:
I guess metacoq is not in nix.
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.
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.)
Julin S (Jul 13 2022 at 03:55):And doing using the nix file that Cyril mentioned made mathcomp work as well.
Thanks!
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'.
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
Julin S (Jul 13 2022 at 04:00):And I'm using an old nix channel (21.11) maybe that's the reason?
Julin S (Jul 13 2022 at 04:02):But why isn't metacoq showing up at nix.search.org though? Even in unstable channel.
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.
Théo Zimmermann (Jul 13 2022 at 10:45): Théo Zimmermann (Jul 13 2022 at 10:46):However, this version is still available. You can get it by doing a package override.
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.
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: Jun 10 2023 at 23:01 UTC