Stream: Nix toolbox devs & users

Topic: ✔ mathcomp via nix


view this post on Zulip Julin S (Feb 26 2023 at 06:22):

Hi. How can I have mathcomp via nix?

Is it as simple as:

nix-shell -p coqPackages.mathcomp coq

view this post on Zulip Julin S (Feb 26 2023 at 06:23):

Or is the coq-nix-toolbox a pre-requisite?

view this post on Zulip Théo Zimmermann (Feb 26 2023 at 10:31):

Yes, it is as simple as this. No, you do not need the Coq Nix Toolbox for such simple use cases.

view this post on Zulip Julin S (Feb 26 2023 at 18:49):

Yeah, but even after entering this nix-shell, I got error upon trying to import mathlib..

From mathcomp Require Import all_ssreflect.
(*
Cannot find a physical path bound to logical path
all_ssreflect with prefix mathcomp.
 *)

Any idea what I might've missed?

Coq version is 8.15

view this post on Zulip Ali Caglayan (Feb 26 2023 at 19:12):

You need to do From mathcomp.ssreflect Require Import all_ssreflect.

view this post on Zulip Ali Caglayan (Feb 26 2023 at 19:12):

But if that still doesn't work, then something else is going on.

view this post on Zulip Paolo Giarrusso (Feb 26 2023 at 19:21):

Shouldn't From mathcomp Require... just work? At least it works on the platform, and used to work with Nix (ages ago, around Coq 8.6): https://stackoverflow.com/a/43997482/53974

view this post on Zulip Ali Caglayan (Feb 26 2023 at 19:36):

Yes @Paolo Giarrusso you are right. I tried this myself, and it appears that it works fine. What I would guess @Julin S is that you are not actually using the correct coqc. Which editor are you running this in? For example, you example works when I do:

nix-shell -p coqPackages.mathcomp coqPackages.coqide coq --command coqide

view this post on Zulip Ali Caglayan (Feb 26 2023 at 19:37):

Editors like coqide are not smart enough to work with other versions of Coq and are tied to their intended Coq version.

view this post on Zulip Ali Caglayan (Feb 26 2023 at 19:37):

Editors like PG and VsCoq will use coqtop or coqidetop which is distributed via coq.

view this post on Zulip Ali Caglayan (Feb 26 2023 at 19:37):

For them to pick up the correct binary, they have to be run via the nix-shell.

view this post on Zulip Ali Caglayan (Feb 26 2023 at 19:38):

You can do this by starting code, emacs or whatever inside the interactive nix shell.

view this post on Zulip Paolo Giarrusso (Feb 26 2023 at 20:16):

also beware: both emacs and code can be configured to find a Coq version that is not the one on the PATH.

So as a first test, maybe try coqc your_file.v inside the Nix shell to confirm that coqc is indeed working.

view this post on Zulip Julin S (Feb 27 2023 at 02:50):

I was using via coqtail in vim.

view this post on Zulip Julin S (Feb 27 2023 at 02:51):

But still not working.. Not sure what's going on..

This is what I got:

julin:~$ nix-shell -p coq coqPackages.mathcomp --command coqtop
Welcome to Coq 8.15.2

Coq < From mathcomp Require Import all_ssreflect.
Toplevel input, characters 0-43:
> From mathcomp Require Import all_ssreflect.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Cannot find a physical path bound to logical path
all_ssreflect with prefix mathcomp.

Coq < From mathcomp.ssreflect Require Import all_ssreflect.
Toplevel input, characters 0-53:
> From mathcomp.ssreflect Require Import all_ssreflect.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Cannot find a physical path bound to logical path
all_ssreflect with prefix mathcomp.ssreflect.

view this post on Zulip Julin S (Feb 27 2023 at 02:53):

opam is there as well. Maybe there's something that can interfere there? opam list shows nothing about coq though..

view this post on Zulip Paolo Giarrusso (Feb 27 2023 at 04:30):

(low confidence) Maybe try to get a bash shell (drop --command coqtop?) and use which coqtop to confirm it is using a binary from nix?

view this post on Zulip Julin S (Feb 27 2023 at 06:03):

Looks like it's the one from nix:

[nix-shell:~]$ which coqtop
/nix/store/7vzbhhdjlhr5akg1h48041lyyl1546ip-coq-8.15.2/bin/coqtop

[nix-shell:~]$ which coqc
/nix/store/7vzbhhdjlhr5akg1h48041lyyl1546ip-coq-8.15.2/bin/coqc

Could there be a way to check location of mathcomp as well?

view this post on Zulip Julin S (Feb 27 2023 at 06:08):

Oh... Could this be the problem?

[nix-shell:~]$ nix-env -q | grep coq
coq8.13-compcert-3.9
coq8.13-mathcomp-all-1.14.0

[nix-shell:~]$ coqc --version
The Coq Proof Assistant, version 8.15.2
compiled with OCaml 4.12.1

I had coq-8.13 installed 'globally'. Let me try removing that.

view this post on Zulip Julin S (Feb 27 2023 at 06:10):

Removed the global packages with nix-env --uninstall. They no longer show up in nix-env -q, but mathcomp still not being detected. :sick:

view this post on Zulip Julin S (Feb 27 2023 at 06:16):

And nix-locate mathcomp shows only the coq8.13 version even after entering the nix-shell coq coqPackages.mathcomp.

view this post on Zulip Théo Zimmermann (Feb 27 2023 at 13:48):

Once you are into nix-shell -p coq coqPackages.mathcomp, the variable $COQPATH should be defined and should point to the location of mathcomp, which is how Coq will locate it. So you could try to run echo $COQPATH to check for this.

view this post on Zulip Julin S (Feb 27 2023 at 14:29):

Looks like something about mathcomp does end up being in $COQPATH for me.

[nix-shell:~/]$ echo $COQPATH
/nix/store/v1mczj04vm4zlp875wrw0cbprxp1sp90-coq8.15-mathcomp-all-1.14.0/lib/coq/8.15/user-contrib/:/nix/store/w0cxv4bpsx5z1prassrpnj2wlnbfx0a3-coq8.15-coq-ext-lib-0.11.6/lib/coq/8.15/user-contrib/:/nix/store/zxqk8drk0rvzd4xn249r6silgf24a7cm-coq8.15-QuickChick-1.6.2/lib/coq/8.15/user-contrib/:/nix/store/k9ahvja82jf026w8gbivr6gp8fb88k20-coq8.15-mathcomp-ssreflect-1.14.0/lib/coq/8.15/user-contrib/:/nix/store/p7iz3ddgaqjvllwahp7y72mmpi62ikgk-coq8.15-simple-io-1.7.0/lib/coq/8.15/user-contrib/:/nix/store/v1mczj04vm4zlp875wrw0cbprxp1sp90-coq8.15-mathcomp-all-1.14.0/lib/coq/8.15/user-contrib/:/nix/store/w0cxv4bpsx5z1prassrpnj2wlnbfx0a3-coq8.15-coq-ext-lib-0.11.6/lib/coq/8.15/user-contrib/:/nix/store/zxqk8drk0rvzd4xn249r6silgf24a7cm-coq8.15-QuickChick-1.6.2/lib/coq/8.15/user-contrib/:/nix/store/k9ahvja82jf026w8gbivr6gp8fb88k20-coq8.15-mathcomp-ssreflect-1.14.0/lib/coq/8.15/user-contrib/:/nix/store/p7iz3ddgaqjvllwahp7y72mmpi62ikgk-coq8.15-simple-io-1.7.0/lib/coq/8.15/user-contrib/

view this post on Zulip Julin S (Feb 27 2023 at 14:32):

Like this:

/nix/store/zxqk8drk0rvzd4xn249r6silgf24a7cm coq8.15-QuickChick-1.6.2/lib/coq/8.15/user-contrib/
/nix/store/zxqk8drk0rvzd4xn249r6silgf24a7cm coq8.15-QuickChick-1.6.2/lib/coq/8.15/user-contrib/
/nix/store/w0cxv4bpsx5z1prassrpnj2wlnbfx0a3 coq8.15-coq-ext-lib-0.11.6/lib/coq/8.15/user-contrib/
/nix/store/w0cxv4bpsx5z1prassrpnj2wlnbfx0a3 coq8.15-coq-ext-lib-0.11.6/lib/coq/8.15/user-contrib/
/nix/store/v1mczj04vm4zlp875wrw0cbprxp1sp90 coq8.15-mathcomp-all-1.14.0/lib/coq/8.15/user-contrib/
/nix/store/v1mczj04vm4zlp875wrw0cbprxp1sp90 coq8.15-mathcomp-all-1.14.0/lib/coq/8.15/user-contrib/
/nix/store/k9ahvja82jf026w8gbivr6gp8fb88k20 coq8.15-mathcomp-ssreflect-1.14.0/lib/coq/8.15/user-contrib/
/nix/store/k9ahvja82jf026w8gbivr6gp8fb88k20 coq8.15-mathcomp-ssreflect-1.14.0/lib/coq/8.15/user-contrib/
/nix/store/p7iz3ddgaqjvllwahp7y72mmpi62ikgk coq8.15-simple-io-1.7.0/lib/coq/8.15/user-contrib/
/nix/store/p7iz3ddgaqjvllwahp7y72mmpi62ikgk coq8.15-simple-io-1.7.0/lib/coq/8.15/user-contrib/

There is a duplicate entry in each case...

view this post on Zulip Julin S (Feb 27 2023 at 15:51):

Well... I modified COQPATH to remove the duplicates and it now works!

COQPATH=/nix/store/zxqk8drk0rvzd4xn249r6silgf24a7cm-coq8.15-QuickChick-1.6.2/lib/coq/8.15/user-contrib/:/nix/store/w0cxv4bpsx5z1prassrpnj2wlnbfx0a3-coq8.15-coq-ext-lib-0.11.6/lib/coq/8.15/user-contrib/:/nix/store/v1mczj04vm4zlp875wrw0cbprxp1sp90-coq8.15-mathcomp-all-1.14.0/lib/coq/8.15/user-contrib/:/nix/store/k9ahvja82jf026w8gbivr6gp8fb88k20-coq8.15-mathcomp-ssreflect-1.14.0/lib/coq/8.15/user-contrib/:/nix/store/p7iz3ddgaqjvllwahp7y72mmpi62ikgk-coq8.15-simple-io-1.7.0/lib/coq/8.15/user-contrib/

view this post on Zulip Julin S (Feb 27 2023 at 15:51):

Thanks!

view this post on Zulip Julin S (Feb 27 2023 at 15:51):

I'm still not sure what's causing the duplicate entries though..

view this post on Zulip Julin S (Feb 27 2023 at 15:54):

Oh.. I think I got the reason. I was on a nested nix-shell. Had done a nix-shell while within a nix-shell with coq... :woozy_face:

view this post on Zulip Julin S (Feb 27 2023 at 15:56):

Well.. the nested shell wasn't the problem.

view this post on Zulip Vincent Laporte (Feb 28 2023 at 05:06):

It’s surprising that you have all of these directories in the COQPATH: mathcomp is not supposed to bring QuickChick & co. in scope, is it?

view this post on Zulip Théo Zimmermann (Feb 28 2023 at 10:15):

Is COQPATH already defined when you are outside any nix-shell?

view this post on Zulip Julin S (Mar 02 2023 at 19:42):

Vincent Laporte said:

It’s surprising that you have all of these directories in the COQPATH: mathcomp is not supposed to bring QuickChick & co. in scope, is it?

Sorry, I also had quickchick inside earlier.

Here is a fresh one:

~/$ :echo $COQPATH

~/$ nix-shell -p coq coqPackages.mathcomp coqPackages.coq-elpi

[nix-shell:~/]$ echo $COQPATH
/nix/store/v1mczj04vm4zlp875wrw0cbprxp1sp90-coq8.15-mathcomp-all-1.14.0/lib/coq/8.15/user-contrib/:/nix/store/varn9kzpqqh6c1h3ra0m2b2cynav3jzd-coq8.15-elpi-1.13.0/lib/coq/8.15/user-contrib/

view this post on Zulip Julin S (Mar 02 2023 at 19:43):

Sorry I hadn't seen the replies...

view this post on Zulip Julin S (Mar 02 2023 at 19:44):

mathcomp wasn't loading here again.

view this post on Zulip Julin S (Mar 02 2023 at 19:44):

But manually modifying COQPATH like earlier, makes mathcomp discoverable again.

view this post on Zulip Théo Zimmermann (Mar 03 2023 at 09:00):

Julin S said:

But manually modifying COQPATH like earlier, makes mathcomp discoverable again.

I don't understand. You say modifying COQPATH like earlier, but earlier there were duplicates and you modified the variable to remove duplicates. Here there are no duplicates, so what did you modify?

view this post on Zulip Julin S (Mar 03 2023 at 14:54):

Yeah earlier there were duplicates. But I guess it was because I messed up in that shell because afterwards there was no duplication.

view this post on Zulip Julin S (Mar 03 2023 at 14:56):

I did this to get mathcomp active:

COQPATH=/nix/store/v1mczj04vm4zlp875wrw0cbprxp1sp90-coq8.15-mathcomp-all-1.14.0/lib/coq/8.15/user-contrib/:/nix/store/k9ahvja82jf026w8gbivr6gp8fb88k20-coq8.15-mathcomp-ssreflect-1.14.0/lib/coq/8.15/user-contrib/

view this post on Zulip Julin S (Mar 03 2023 at 14:56):

Afterwards (but not before) this went through okay:

From mathcomp Require Import all_ssreflect.

view this post on Zulip Julin S (Mar 03 2023 at 14:57):

Is ssreflect another package that I have to activate or something?

view this post on Zulip Julin S (Mar 03 2023 at 14:58):

Earlier COQPATH was just:

[nix-shell:~/]$ echo $COQPATH
/nix/store/v1mczj04vm4zlp875wrw0cbprxp1sp90-coq8.15-mathcomp-all-1.14.0/lib/coq/8.15/user-contrib/

view this post on Zulip Julin S (Mar 03 2023 at 16:16):

I think got what I was missing.

This worked:

$ nix-shell -p coq coqPackages.mathcomp coqPackages.mathcomp-ssreflect

Needed the mathcomp-ssreflect package as well.

view this post on Zulip Julin S (Mar 03 2023 at 16:20):

Only now am I realizing that there are a bunch of mathcomp nix packages...

view this post on Zulip Julin S (Mar 03 2023 at 16:20):

:sweat_smile:

view this post on Zulip Notification Bot (Mar 03 2023 at 16:20):

Julin S has marked this topic as resolved.

view this post on Zulip Théo Zimmermann (Mar 03 2023 at 17:55):

Indeed, there are a bunch of mathcomp Nix packages. However, I would have expected coqPackages.mathcomp to bring everything in scope. @Cyril Cohen is this behaving as expected or not?

view this post on Zulip Cyril Cohen (Mar 03 2023 at 17:58):

On my machine, if I try

nix-shell -p coq coqPackages.mathcomp
echo $COQPATH

I do get everything, which is the expected behaviour

/nix/store/53rqp8vlp19d51v80ylmgxqlq0cv4j6h-coq8.16-mathcomp-all-1.15.0/lib/coq/8.16/user-contrib/:/nix/store/f694d4k721qc3zba68xqm3mx3ff7wr4q-coq8.16-mathcomp-ssreflect-1.15.0/lib/coq/8.16/user-contrib/:/nix/store/2q3p9wgir58dx689i3jwd4gqmzfsm7zf-coq8.16-mathcomp-fingroup-1.15.0/lib/coq/8.16/user-contrib/:/nix/store/gc8fnk1iqw0can0i60adsv63yja403lm-coq8.16-mathcomp-algebra-1.15.0/lib/coq/8.16/user-contrib/:/nix/store/gmj2qnvmwn0s2381ah524fkdkkqhnb22-coq8.16-mathcomp-solvable-1.15.0/lib/coq/8.16/user-contrib/:/nix/store/g3hj2lq2wpz9q17r85k0q7fwgb2962i4-coq8.16-mathcomp-field-1.15.0/lib/coq/8.16/user-contrib/:/nix/store/w6c63ya63xlr6i3fd88sc193ymgh4rja-coq8.16-mathcomp-character-1.15.0/lib/coq/8.16/user-contrib/

view this post on Zulip Théo Zimmermann (Mar 03 2023 at 18:01):

OK, so the difference might be due to the nixpkgs version. I assume that you are on a recent nixpkgs-unstable, Cyril?

view this post on Zulip Cyril Cohen (Mar 03 2023 at 18:02):

Théo Zimmermann said:

OK, so the difference might be due to the nixpkgs version. I assume that you are on a recent nixpkgs-unstable, Cyril?

Yes, the most recent one existing a minute ago

view this post on Zulip Théo Zimmermann (Mar 03 2023 at 18:02):

Actually, I could confirm this on my own machine as well.

view this post on Zulip Théo Zimmermann (Mar 03 2023 at 18:03):

Then, @Julin S, maybe you need to update your nixpkgs channel. This seems to be confirmed by the fact that you are currently getting Coq 8.15 as the default version.

view this post on Zulip Julin S (Mar 12 2023 at 06:15):

Then, Julin S, maybe you need to update your nixpkgs channel. This seems to be confirmed by the fact that you are currently getting Coq 8.15 as the default version.

Thanks! I updated nix channel and it seems to be okay now.


Last updated: Dec 07 2023 at 09:01 UTC