Stream: Nix toolbox devs & users

Topic: ✔ Importing "ring"

view this post on Zulip Pierre Jouvelot (Oct 03 2022 at 15:55):

I'm unable to run the following commands in PG, launched as emacs from nix-shell --arg withEmacs true --arg override '{coq = "8.15"; mathcomp = "1.13";}):

From mathcomp Require Import all_algebra.
From mathcomp.algebra_tactics Require Import ring.

The first line goes through as usual, but the second one gives an error message:

Error: Cannot find a physical path bound to logical path ring with prefix mathcomp.algebra_tactics.

How should I proceed? Thanks.

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 19:33):

not an expert but https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/coq-modules/mathcomp/default.nix does not claim to include
https://github.com/math-comp/algebra-tactics , and it doesn't seem included at all in nixpkgs?

view this post on Zulip Théo Zimmermann (Oct 04 2022 at 07:08):

Indeed, Paolo is right.

view this post on Zulip Théo Zimmermann (Oct 04 2022 at 07:09):

Note that the command you provide only shows that you are running the Coq Nix Toolbox with some version parameters, it doesn't show which mathcomp packages you will get in scope. This should be defined in your config.nix, so please provide a link to that.

view this post on Zulip Théo Zimmermann (Oct 04 2022 at 07:10):

The algebra-tactics repository uses an overlay: https://github.com/math-comp/algebra-tactics/blob/master/.nix/coq-overlays/algebra-tactics/default.nix
So it should be:

  1. easy to publish on nixpkgs
  2. easy to duplicate locally in order to get it available as a project dependency even more quickly

view this post on Zulip Pierre Jouvelot (Oct 04 2022 at 09:40):

Thanks @Paolo Giarrusso @Théo Zimmermann . I don't have access to this file right now, but will send a link to it asap. It's pretty much the default version of config.nix, if I remember correctly: nothing fancy.

view this post on Zulip Théo Zimmermann (Oct 04 2022 at 09:41):

Even if it's the default, it should set the value of attribute. This is what matters.

view this post on Zulip Théo Zimmermann (Oct 04 2022 at 09:42):

Then, the dependencies of the package defined by this attribute are the ones you get when running nix-shell.

view this post on Zulip Pierre Jouvelot (Oct 04 2022 at 15:53):

The config.nix file can be found in the .nix directory of the https://github.com/jouvelot/mech.v repo. I also put a copy in https://www.dropbox.com/s/pak83ggifd95vhn/config.nix?dl=0. Thanks for any help :smile:

config.nix

view this post on Zulip Théo Zimmermann (Oct 04 2022 at 17:45):

I'll open a PR with what you need.

view this post on Zulip Théo Zimmermann (Oct 04 2022 at 17:51):

https://github.com/jouvelot/mech.v/pull/3

view this post on Zulip Pierre Jouvelot (Oct 04 2022 at 21:39):

Thanks a lot @Théo Zimmermann . Merged and working :+1:

view this post on Zulip Notification Bot (Oct 04 2022 at 21:42):

Pierre Jouvelot has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC