Stream: Nix toolbox devs & users

Topic: Upgrading coq with Nix


view this post on Zulip Pierre Jouvelot (Mar 15 2022 at 09:19):

I'd like to move my use of nix-shell to the latest version of Coq/mathcomp. How should I update the default.nix file in my project folder, which was cooked up for me by Emilio? I tried to play with the version numbers of the packages but went nowhere; I probably need a new tarball, but I don't know which and where to get it. The current file is given below (using macOS Big Sur):

{
  pkgs ? import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/5c7a370a208d93d458193fc05ed84ced0ba7f387.tar.gz") {}
}:
pkgs.stdenv.mkDerivation rec {

  name = "coq-vcg";
  version = "0.0.1";

  # EJGA: There is a way to make the install from the binary cache,
  # but I don't know enough nix to make this work.
  buildInputs = [
    pkgs.dune_2
    # This seems very heavy too.
    # pkgs.ocaml-ng.ocamlPackages_4_11.ocaml
    pkgs.coqPackages_8_13.coq
    # This will recompile math-comp :S, see above note
    pkgs.coqPackages_8_13.mathcomp
  ];

  src =
    with builtins; filterSource
      (path: _:
        !elem (baseNameOf path) [".git" "_build" "nix"]) ./.;

  # This call make all
  buildFlags = "all";

  # Not working needs a bit more work
  # installTargets = "install";
}

view this post on Zulip Vincent Laporte (Mar 15 2022 at 12:24):

If you want bleeding-edge stuff, you can look there: https://channels.nixos.org/nixpkgs-unstable
The git commit that you’ll find there can be used to update the URL argument to fetchTarball.
Then you’ll be able to change the 8_13 that appear around line 15 to 8_15.

view this post on Zulip Pierre Jouvelot (Mar 15 2022 at 14:04):

Well, I updated my default. nix file by changing the fetchTarball name of the .tar.gz filename with the one given in git-revision, changed the 8_13 with 8_15, launched nix-shell, saw it compile tons of programs, including coq 8_15, which looked good. I then ran a make clean in my project directory to get rid of the .vo files and then make all (which launches a dune build). I got a bunch of warnings such as

    coqdep FP.v.d
*** Warning: in file FP.v, library all_ssreflect is required from root mathcomp and has not been found in the loadpath!
*** Warning: in file FP.v, library perm is required from root mathcomp.fingroup and has not been found in the loadpath!
*** Warning: in file FP.v, library ssrsearch is required from root Coq and has not been found in the loadpath!

followed by

File "./lib.v", line 11, characters 0-43:
Error: Cannot find a physical path bound to logical path
all_ssreflect with prefix mathcomp.

make: *** [Makefile:8: all] Error 1

The first line of the lib.v file is

From mathcomp Require Import all_ssreflect.

Any suggestion on what I did wrong?

view this post on Zulip Vincent Laporte (Mar 15 2022 at 14:36):

You did nothing wrong. Just try adding to the buildInputs list the missing dependencies (coqPackages_8_15.ssreflect, etc).

view this post on Zulip Pierre Jouvelot (Mar 15 2022 at 15:23):

Vincent Laporte said:

You did nothing wrong. Just try adding to the buildInputs list the missing dependencies (coqPackages_8_15.ssreflect, etc).

I'm not sure why I didn't need to add those dependencies in my previous version of the nix/coq default.nix file, but this is working great now: thanks a lot, @Vincent Laporte .

Now, I'd like to add the withEmacs argument to default.nix, a mode that is working great with the default.nix I see in the mathcomp repo I cloned. However, the syntax looks different from the one of my current version of default.nix. I tried some "natural" changes, but this didn't work, and the emacs command is always "not found" when launching nix-shell --arg withEmacs true. Any suggestion on how to add this argument to my default.nix?

view this post on Zulip Théo Zimmermann (Mar 15 2022 at 17:25):

The simplest way to get the withEmacs mode working would be to start using the Coq Nix Toolbox (like MathComp does). See https://github.com/coq-community/coq-nix-toolbox.

view this post on Zulip Théo Zimmermann (Mar 15 2022 at 17:26):

Is this for a project that's publicly available? We could help set this up.

view this post on Zulip Pierre Jouvelot (Mar 15 2022 at 18:18):

@Théo Zimmermann : thanks a lot for the offer to help; this is quite appreciated. This a project that I will make public, then. Since Emilio Gallego Arias, who's part of it, would like also to see how the nix stuff works, it would be better to wait a couple of days to help us, so that he can participate too, once his current obligations are over. Thanks again :)

view this post on Zulip Pierre Jouvelot (Mar 19 2022 at 14:32):

Following up on Théo's suggestion, I tried to install Coq Nix Toolbox on MacOS Big Sur, and the command

nix-env -iA nixpkgs.cachix && cachix use coq && cachix use coq-community && cachix use math-comp

failed with:

ld: file not found: /System/Library/Frameworks/Security.framework/Versions/A/Security for architecture x86_64
clang-7: error: linker command failed with exit code 1 (use -v to see invocation)
make: *** [mk/lib.mk:104: src/libmain/libnixmain.dylib] Error 1

I couldn't find anything meaningful via google, although some people mentioned issues regarding clang on this platform. Any suggestion on how to proceed?

BTW, what's the best way to get rid of all the added stuff (a lot, apparently!) that Coq Nix Toolbox added to my machine, if I ever wanted to stop using it (once it works ;) )?

view this post on Zulip Pierre Jouvelot (Mar 19 2022 at 15:49):

Pierre Jouvelot said:

Following up on Théo's suggestion, I tried to install Coq Nix Toolbox on MacOS Big Sur, and the command

nix-env -iA nixpkgs.cachix && cachix use coq && cachix use coq-community && cachix use math-comp

failed with:

ld: file not found: /System/Library/Frameworks/Security.framework/Versions/A/Security for architecture x86_64
clang-7: error: linker command failed with exit code 1 (use -v to see invocation)
make: *** [mk/lib.mk:104: src/libmain/libnixmain.dylib] Error 1

Answering my own question, it seems that doing a nix upgrade via nix-channel --update; nix-env -iA nixpkgs.nix nixpkgs.cacertwas enough to fix the issue; the initial nix-envran (very quickly, which is a bit disturbing) to its successful end.

view this post on Zulip Théo Zimmermann (Mar 20 2022 at 19:21):

Note that you install Nix on your machine, but you install the Coq Nix Toolbox on a given project. So to uninstall the Coq Nix Toolbox on a project, you remove the stuff added when installing (.nix/, default.nix and possibly some auto-generated GitHub workflows). To uninstall Nix on your machine, the answer used to be rm -rf /nix but it seems that things have gotten more complex. See https://iohk.zendesk.com/hc/en-us/articles/4415830650265-Uninstall-nix-on-MacOS for what seems to be an up-to-date answer.

view this post on Zulip Pierre Jouvelot (Mar 28 2022 at 18:38):

Théo Zimmermann said:

Is this for a project that's publicly available? We could help set this up.

@Théo Zimmermann , I made our repo public under https://github.com/jouvelot/mech.v. Would you be available to show us how to set it properly with Nix, as you offered, next week? Emilio and I would be available Monday 4, between 2 or 4 PM. Or what other date/time would be good for you, if you're busy at that time?

view this post on Zulip Karl Palmskog (Mar 28 2022 at 18:44):

@Pierre Jouvelot during the hackathon, Cyril Cohen kindly set up the Nix toolbox for the Huffman project as a demonstration, you can see his commit here, which may be helpful: https://github.com/coq-community/huffman/commit/1cec7c34f5f808cf0c5e1b4efc0774ffb6623db3

view this post on Zulip Karl Palmskog (Mar 28 2022 at 18:45):

I'm not saying to emulate the additions (they should be generated by the toolbox), but should give an idea of what you are supposed to check into version control. From what I remember, the main file Cyril edited manually was .nix/coq-overlays/huffman/default.nix and possibly .nix/config.nix

view this post on Zulip Théo Zimmermann (Mar 29 2022 at 09:06):

I won't be available at the proposed time, but I could be available anytime on Tuesday 5.

view this post on Zulip Pierre Jouvelot (Mar 29 2022 at 09:43):

Théo Zimmermann said:

I won't be available at the proposed time, but I could be available anytime on Tuesday 5.

Thanks a lot, Théo. @Emilio Jesús Gallego Arias would Tuesday 5, at 2PM be ok with you? Or later?

view this post on Zulip Cyril Cohen (Mar 29 2022 at 11:06):

BTW, I added a coq-overlay generator: https://github.com/coq-community/coq-nix-toolbox/pull/103

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2022 at 16:22):

@Pierre Jouvelot tueday would have to be after 4pm

view this post on Zulip Pierre Jouvelot (Mar 29 2022 at 18:35):

Emilio Jesús Gallego Arias said:

Pierre Jouvelot tueday would have to be after 4pm

@Emilio Jesús Gallego Arias @Théo Zimmermann Great, so let's say Tuesday April 5, at 4:30 PM, allowing for some slack. I can generate a Zoom link, and send it to both of you (Théo, please send me your email address at mailto:pierre.jouvelot@minesparis.psl.eu).


Last updated: Jan 29 2023 at 15:02 UTC