Cannot find a physical path bound to logical path pred with prefix pcm.

[chan-bing]

I have run the following command：

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-fcsl-pcm  .

However, the following error is still encountered when running "From pcm Require Import pred.": Error: Cannot find a physical path bound to logical path pred with prefix pcm. I dont know that is why

[clayrat]

What does opam list say, what is the installed version of the library?

[chan-bing]

zhang@zhang-virtual-machine:~$ opam list
# Packages matching: installed
# Name                 # Installed # Synopsis
base-bigarray          base
base-threads           base
base-unix              base
conf-findutils         1           Virtual package relying on findutils
conf-gmp               4           Virtual package relying on a GMP lib system i
coq                    8.16.1      Formal proof management system
coq-fcsl-pcm           dev         Partial Commutative Monoids
coq-mathcomp-ssreflect dev         Small Scale Reflection
dune                   3.7.0       Fast, portable, and opinionated build system
ocaml                  4.13.1      The OCaml compiler (virtual package)
ocaml-config           2           OCaml Switch Configuration
ocaml-system           4.13.1      The OCaml compiler (system version, from outs
ocamlfind              1.9.5       A library manager for OCaml
zarith                 1.12        Implements arithmetic and logical operations

[clayrat]

Oh right, you're installing it from the sources. When did you clone the repo? It seems you have an old version, the pcm namespace was introduced in November.

[chan-bing]

emm, several hours ago? And what should i do to run From pcm Require Import pred. correctly. ^_^

[clayrat]

What does git log -3 say if you run it from the fcsl-pcm repo root?

[chan-bing]

zhang@zhang-virtual-machine:~/.opam/default/.opam-switch/sources/coq-fcsl-pcm.dev$ git log -3
commit a654207feab3c08150ae79ac929883fd04ef0191 (HEAD -> master, tag: v1.7.0, tag: v.1.7.0, opam-ref-master)
Author: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date:   Fri Nov 11 11:38:49 2022 +0100

    refactor seqext

commit d35feb9d562812ac11e1f8ff3c764b9fd0a7061f
Author: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date:   Fri Nov 11 03:23:02 2022 +0100

    find/index_last theory

commit 85f3f641364568c260a84f62ba352fd786140148
Author: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date:   Thu Nov 10 22:00:21 2022 +0100

    reorganize seq lemmas

that is the result of git log -3

[clayrat]

Hm, that looks correct. Do other libraries work, e.g. can you run From mathcomp Require Import ssreflect ssrbool ssrfun seq. ?

[chan-bing]

yes, From mathcomp Require Import ssreflect ssrbool ssrfun seq. succeed.

[clayrat]

Can you try using the released version of PCM lib, i.e. run opam pin coq-fcsl-pcm 1.7.0 and try the import again?

[chan-bing]

zhang@zhang-virtual-machine:~$ opam pin coq-fcsl-pcm 1.7.0
coq-fcsl-pcm is now pinned to version 1.7.0

The following actions will be performed:
  ↘ downgrade coq-fcsl-pcm dev to 1.7.0*
Do you want to continue? [Y/n] y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] Failed to get sources of coq-fcsl-pcm.1.7.0: Download command failed

#=== ERROR while fetching sources for coq-fcsl-pcm.1.7.0 ======================#
OpamSolution.Fetch_fail("https://github.com/imdea-software/fcsl-pcm/archive/v1.7.0.tar.gz (Download command failed: \"/usr/bin/wget --content-disposition -t 3 -O /home/zhang/.opam/default/.opam-switch/sources/coq-fcsl-pcm/v1.7.0.tar.gz.part -U opam/2.1.2 -- https://github.com/imdea-software/fcsl-pcm/archive/v1.7.0.tar.gz\" exited with code 4)")

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ ⬇ fetch coq-fcsl-pcm 1.7.0
└─ 
╶─ No changes have been performed
[NOTE] Pinning command successful, but your installed packages may be out of
       sync.

emm, it is failed

[clayrat]

"Code 4" for wget means there's a network error, so it looks like your VM is misconfigured in some way.

[chan-bing]

Now, i succeed change the version to 1.7.0, but the problem still be there.

[clayrat]

What do opam switch and ls -1fRX ~/.opam/default/lib/coq/user-contrib/pcm/ say?

[chan-bing]

zhang@zhang-virtual-machine:~$ opam switch
#  switch   compiler      description
→  default  ocaml.4.13.1  default
zhang@zhang-virtual-machine:~$ ls -1fRX ~/.opam/default/lib/coq/user-contrib/pcm/
/home/zhang/.opam/default/lib/coq/user-contrib/pcm/:
core
pcm
.
..
options.glob
options.v
options.vo

/home/zhang/.opam/default/lib/coq/user-contrib/pcm/core:
.
..
auto.glob
axioms.glob
finmap.glob
ordtype.glob
pred.glob
prelude.glob
rtc.glob
seqext.glob
seqint.glob
seqperm.glob
auto.v
axioms.v
finmap.v
ordtype.v
pred.v
prelude.v
rtc.v
seqext.v
seqint.v
seqperm.v
auto.vo
axioms.vo
finmap.vo
ordtype.vo
pred.vo
prelude.vo
rtc.vo
seqext.vo
seqint.vo
seqperm.vo

/home/zhang/.opam/default/lib/coq/user-contrib/pcm/pcm:
.
..
automap.glob
autopcm.glob
heap.glob
invertible.glob
lift.glob
morphism.glob
mutex.glob
natmap.glob
pcm.glob
unionmap.glob
automap.v
autopcm.v
heap.v
invertible.v
lift.v
morphism.v
mutex.v
natmap.v
pcm.v
unionmap.v
automap.vo
autopcm.vo
heap.vo
invertible.vo
lift.vo
morphism.vo
mutex.vo
natmap.vo
pcm.vo
unionmap.vo

emm

[chan-bing]

Ok, thank you very much for your reply. I'm sorry to bother you for a long time. ^^

[clayrat]

Sorry I didn't scroll your output properly, you do seem to have the library installed fully. Nevertheless I still don't really know what to do from here on. One final hypothesis I can make is that the file permissions could be set up wrong somehow. Maybe try running both

ls -la ~/.opam/default/lib/coq/user-contrib/pcm/core/
ls -la ~/.opam/default/lib/coq/user-contrib/mathcomp/ssreflect/

and see if there's something off?

[chan-bing]

zhang@zhang-virtual-machine:~$ ls -la ~/.opam/default/lib/coq/user-contrib/pcm/core/
总用量 4348
drwxr-xr-x 2 zhang zhang   4096  2月 22 22:16 .
drwxr-xr-x 4 zhang zhang   4096  2月 22 22:16 ..
-rw-r--r-- 1 zhang zhang   6466  2月 22 22:16 auto.glob
-rw-r--r-- 1 zhang zhang   3941  2月 22 22:16 auto.v
-rw-r--r-- 1 zhang zhang  27459  2月 22 22:16 auto.vo
-rw-r--r-- 1 zhang zhang  12842  2月 22 22:16 axioms.glob
-rw-r--r-- 1 zhang zhang   4597  2月 22 22:16 axioms.v
-rw-r--r-- 1 zhang zhang  26876  2月 22 22:16 axioms.vo
-rw-r--r-- 1 zhang zhang 263683  2月 22 22:16 finmap.glob
-rw-r--r-- 1 zhang zhang  44953  2月 22 22:16 finmap.v
-rw-r--r-- 1 zhang zhang 452127  2月 22 22:16 finmap.vo
-rw-r--r-- 1 zhang zhang  45554  2月 22 22:16 ordtype.glob
-rw-r--r-- 1 zhang zhang  11195  2月 22 22:16 ordtype.v
-rw-r--r-- 1 zhang zhang  78107  2月 22 22:16 ordtype.vo
-rw-r--r-- 1 zhang zhang 191815  2月 22 22:16 pred.glob
-rw-r--r-- 1 zhang zhang  45570  2月 22 22:16 pred.v
-rw-r--r-- 1 zhang zhang 248213  2月 22 22:16 pred.vo
-rw-r--r-- 1 zhang zhang 191495  2月 22 22:16 prelude.glob
-rw-r--r-- 1 zhang zhang  36435  2月 22 22:16 prelude.v
-rw-r--r-- 1 zhang zhang 388899  2月 22 22:16 prelude.vo
-rw-r--r-- 1 zhang zhang  48822  2月 22 22:16 rtc.glob
-rw-r--r-- 1 zhang zhang   9831  2月 22 22:16 rtc.v
-rw-r--r-- 1 zhang zhang  99373  2月 22 22:16 rtc.vo
-rw-r--r-- 1 zhang zhang 284462  2月 22 22:16 seqext.glob
-rw-r--r-- 1 zhang zhang  33549  2月 22 22:16 seqext.v
-rw-r--r-- 1 zhang zhang 274102  2月 22 22:16 seqext.vo
-rw-r--r-- 1 zhang zhang 746294  2月 22 22:16 seqint.glob
-rw-r--r-- 1 zhang zhang  90096  2月 22 22:16 seqint.v
-rw-r--r-- 1 zhang zhang 599060  2月 22 22:16 seqint.vo
-rw-r--r-- 1 zhang zhang  42680  2月 22 22:16 seqperm.glob
-rw-r--r-- 1 zhang zhang   7758  2月 22 22:16 seqperm.v
-rw-r--r-- 1 zhang zhang  70102  2月 22 22:16 seqperm.vo
zhang@zhang-virtual-machine:~$ ls -la ~/.opam/default/lib/coq/user-contrib/mathcomp/ssreflect/
总用量 18108
drwxr-xr-x 2 zhang zhang    4096  2月 22 16:00 .
drwxr-xr-x 3 zhang zhang    4096  2月 22 16:00 ..
-rw-r--r-- 1 zhang zhang     972  2月 22 16:00 all_ssreflect.glob
-rw-r--r-- 1 zhang zhang     466  2月 22 16:00 all_ssreflect.v
-rw-r--r-- 1 zhang zhang   17208  2月 22 16:00 all_ssreflect.vo
-rw-r--r-- 1 zhang zhang 1079177  2月 22 16:00 bigop.glob
-rw-r--r-- 1 zhang zhang  109724  2月 22 16:00 bigop.v
-rw-r--r-- 1 zhang zhang  611942  2月 22 16:00 bigop.vo
-rw-r--r-- 1 zhang zhang  235565  2月 22 16:00 binomial.glob
-rw-r--r-- 1 zhang zhang   24446  2月 22 16:00 binomial.v
-rw-r--r-- 1 zhang zhang  239954  2月 22 16:00 binomial.vo
-rw-r--r-- 1 zhang zhang  109275  2月 22 16:00 choice.glob
-rw-r--r-- 1 zhang zhang   29026  2月 22 16:00 choice.v
-rw-r--r-- 1 zhang zhang  137577  2月 22 16:00 choice.vo
-rw-r--r-- 1 zhang zhang  357237  2月 22 16:00 div.glob
-rw-r--r-- 1 zhang zhang   38784  2月 22 16:00 div.v
-rw-r--r-- 1 zhang zhang  249243  2月 22 16:00 div.vo
-rw-r--r-- 1 zhang zhang  175196  2月 22 16:00 eqtype.glob
-rw-r--r-- 1 zhang zhang   38525  2月 22 16:00 eqtype.v
-rw-r--r-- 1 zhang zhang  137541  2月 22 16:00 eqtype.vo
-rw-r--r-- 1 zhang zhang   88912  2月 22 16:00 finfun.glob
-rw-r--r-- 1 zhang zhang   20241  2月 22 16:00 finfun.v
-rw-r--r-- 1 zhang zhang  126022  2月 22 16:00 finfun.vo
-rw-r--r-- 1 zhang zhang  264586  2月 22 16:00 fingraph.glob
-rw-r--r-- 1 zhang zhang   37858  2月 22 16:00 fingraph.v
-rw-r--r-- 1 zhang zhang  258521  2月 22 16:00 fingraph.vo
-rw-r--r-- 1 zhang zhang  801982  2月 22 16:00 finset.glob
-rw-r--r-- 1 zhang zhang   97076  2月 22 16:00 finset.v
-rw-r--r-- 1 zhang zhang  633620  2月 22 16:00 finset.vo
-rw-r--r-- 1 zhang zhang  536080  2月 22 16:00 fintype.glob
-rw-r--r-- 1 zhang zhang   89488  2月 22 16:00 fintype.v
-rw-r--r-- 1 zhang zhang  434481  2月 22 16:00 fintype.vo
-rw-r--r-- 1 zhang zhang  112884  2月 22 16:00 generic_quotient.glob
-rw-r--r-- 1 zhang zhang   27494  2月 22 16:00 generic_quotient.v
-rw-r--r-- 1 zhang zhang  116994  2月 22 16:00 generic_quotient.vo
-rw-r--r-- 1 zhang zhang 2439669  2月 22 16:00 order.glob
-rw-r--r-- 1 zhang zhang  335600  2月 22 16:00 order.v
-rw-r--r-- 1 zhang zhang 1899668  2月 22 16:00 order.vo
-rw-r--r-- 1 zhang zhang  478861  2月 22 16:00 path.glob
-rw-r--r-- 1 zhang zhang   65530  2月 22 16:00 path.v
-rw-r--r-- 1 zhang zhang  449391  2月 22 16:00 path.vo
-rw-r--r-- 1 zhang zhang  548480  2月 22 16:00 prime.glob
-rw-r--r-- 1 zhang zhang   65029  2月 22 16:00 prime.v
-rw-r--r-- 1 zhang zhang  480328  2月 22 16:00 prime.vo
-rw-r--r-- 1 zhang zhang 1214791  2月 22 16:00 seq.glob
-rw-r--r-- 1 zhang zhang  171623  2月 22 16:00 seq.v
-rw-r--r-- 1 zhang zhang 1333551  2月 22 16:00 seq.vo
-rw-r--r-- 1 zhang zhang   34474  2月 22 16:00 ssrAC.glob
-rw-r--r-- 1 zhang zhang   10813  2月 22 16:00 ssrAC.v
-rw-r--r-- 1 zhang zhang   66933  2月 22 16:00 ssrAC.vo
-rw-r--r-- 1 zhang zhang  102850  2月 22 16:00 ssrbool.glob
-rw-r--r-- 1 zhang zhang   13118  2月 22 16:00 ssrbool.v
-rw-r--r-- 1 zhang zhang   55501  2月 22 16:00 ssrbool.vo
-rw-r--r-- 1 zhang zhang     789  2月 22 16:00 ssreflect.glob
-rw-r--r-- 1 zhang zhang    2229  2月 22 16:00 ssreflect.v
-rw-r--r-- 1 zhang zhang    4363  2月 22 16:00 ssreflect.vo
-rw-r--r-- 1 zhang zhang   12207  2月 22 16:00 ssrfun.glob
-rw-r--r-- 1 zhang zhang    2309  2月 22 16:00 ssrfun.v
-rw-r--r-- 1 zhang zhang   14760  2月 22 16:00 ssrfun.vo
-rw-r--r-- 1 zhang zhang     117  2月 22 16:00 ssrmatching.glob
-rw-r--r-- 1 zhang zhang      37  2月 22 16:00 ssrmatching.v
-rw-r--r-- 1 zhang zhang    1798  2月 22 16:00 ssrmatching.vo
-rw-r--r-- 1 zhang zhang  586725  2月 22 16:00 ssrnat.glob
-rw-r--r-- 1 zhang zhang   77714  2月 22 16:00 ssrnat.v
-rw-r--r-- 1 zhang zhang  351461  2月 22 16:00 ssrnat.vo
-rw-r--r-- 1 zhang zhang      73  2月 22 16:00 ssrnotations.glob
-rw-r--r-- 1 zhang zhang    6272  2月 22 16:00 ssrnotations.v
-rw-r--r-- 1 zhang zhang    8331  2月 22 16:00 ssrnotations.vo
-rw-r--r-- 1 zhang zhang  147935  2月 22 16:00 tuple.glob
-rw-r--r-- 1 zhang zhang   26021  2月 22 16:00 tuple.v
-rw-r--r-- 1 zhang zhang  154846  2月 22 16:00 tuple.vo

that is the outputs.

[chan-bing]

I finally found problem: the wrong BIN PATH of coqtop caused the above problem. Finally, I corrected the BIN PATH of my coqtop and successfully imported the fcsl library. I'm sorry to bother you for a long time because of my carelessness and stupid.

[clayrat]

I see, well, enjoy using the library!