Upgrading coq with Nix · Nix toolbox devs & users

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";
}

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.

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!

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

From mathcomp Require Import all_ssreflect.

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).

Pierre Jouvelot (Mar 15 2022 at 15:23):

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?

Théo Zimmermann (Mar 15 2022 at 17:25):

Théo Zimmermann (Mar 15 2022 at 17:26):

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 :)

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

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 ;) )?

Pierre Jouvelot (Mar 19 2022 at 15:49):

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.

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.

Pierre Jouvelot (Mar 28 2022 at 18:38):

@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?

Karl Palmskog (Mar 28 2022 at 18:44):

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

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.

Pierre Jouvelot (Mar 29 2022 at 09:43):

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

Cyril Cohen (Mar 29 2022 at 11:06):

Emilio Jesús Gallego Arias (Mar 29 2022 at 16:22):

Pierre Jouvelot (Mar 29 2022 at 18:35):

@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).

Stream: Nix toolbox devs & users

Topic: Upgrading coq with Nix

Pierre Jouvelot (Mar 15 2022 at 09:19):