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?
Yes, it is as simple as this. No, you do not need the Coq Nix Toolbox for such simple use cases.
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
You need to do From mathcomp.ssreflect Require Import all_ssreflect
.
But if that still doesn't work, then something else is going on.
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
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.
Editors like PG and VsCoq will use coqtop or coqidetop which is distributed via coq.
For them to pick up the correct binary, they have to be run via the nix-shell.
You can do this by starting code
, emacs
or whatever inside the interactive nix shell.
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.
I was using via coqtail in vim.
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..
(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?
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?
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.
Removed the global packages with nix-env --uninstall
. They no longer show up in nix-env -q
, but mathcomp still not being detected. :sick:
And nix-locate mathcomp
shows only the coq8.13 version even after entering the nix-shell coq coqPackages.mathcomp
.
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.
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...
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!
I'm still not sure what's causing the duplicate entries though..
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:
Well.. the nested shell wasn't the problem.
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?
Is COQPATH already defined when you are outside any nix-shell
?
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/
Sorry I hadn't seen the replies...
mathcomp wasn't loading here again.
But manually modifying COQPATH like earlier, makes mathcomp discoverable again.
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?
Yeah earlier there were duplicates. But I guess it was because I messed up in that shell because afterwards there was no duplication.
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?
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.
Only now am I realizing that there are a bunch of mathcomp nix packages...
:sweat_smile:
Julin S has marked this topic as resolved.
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?
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?
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
Actually, I could confirm this on my own machine as well.
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.
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