Julin S (Feb 26 2023 at 06:22): 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
Or is the coq-nix-toolbox a pre-requisite?
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.
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
Ali Caglayan (Feb 26 2023 at 19:12):You need to do From mathcomp.ssreflect Require Import all_ssreflect.
Ali Caglayan (Feb 26 2023 at 19:12):But if that still doesn't work, then something else is going on.
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
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
Editors like coqide are not smart enough to work with other versions of Coq and are tied to their intended Coq version.
Ali Caglayan (Feb 26 2023 at 19:37):Editors like PG and VsCoq will use coqtop or coqidetop which is distributed via coq.
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.
Ali Caglayan (Feb 26 2023 at 19:38):You can do this by starting code, emacs or whatever inside the interactive nix shell.
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.
Julin S (Feb 27 2023 at 02:50):I was using via coqtail in vim.
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.
opam is there as well. Maybe there's something that can interfere there? opam list shows nothing about coq though..
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?
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?
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.
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:
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.
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.
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/
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...
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/
Thanks!
Julin S (Feb 27 2023 at 15:51):I'm still not sure what's causing the duplicate entries though..
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:
Julin S (Feb 27 2023 at 15:56):Well.. the nested shell wasn't the problem.
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?
Théo Zimmermann (Feb 28 2023 at 10:15):Is COQPATH already defined when you are outside any nix-shell?
Julin S (Mar 02 2023 at 19:42):Vincent Laporte said:
It’s surprising that you have all of these directories in the
COQPATH:mathcompis 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/
Sorry I hadn't seen the replies...
Julin S (Mar 02 2023 at 19:44):mathcomp wasn't loading here again.
Julin S (Mar 02 2023 at 19:44):But manually modifying COQPATH like earlier, makes mathcomp discoverable again.
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?
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.
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/
Afterwards (but not before) this went through okay:
From mathcomp Require Import all_ssreflect.
Is ssreflect another package that I have to activate or something?
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/
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.
Julin S (Mar 03 2023 at 16:20):Only now am I realizing that there are a bunch of mathcomp nix packages...
Julin S (Mar 03 2023 at 16:20)::sweat_smile:
Notification Bot (Mar 03 2023 at 16:20):Julin S has marked this topic as resolved.
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?
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/
OK, so the difference might be due to the nixpkgs version. I assume that you are on a recent nixpkgs-unstable, Cyril?
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
Théo Zimmermann (Mar 03 2023 at 18:02):Actually, I could confirm this on my own machine as well.
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.
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