opam does not remove stale files on upgrade

[RalfJung]

If your issue concerns a package not building, please report to https://github.com/ocaml/opam-repository/issues or to the package maintainer unless you are confident it is an issue in the opam tool itself.

I just upgraded the coq-iris package from dev.2020-11-03.3.4cd21e62 to dev.2020-11-05.3.7f8b01a9 (all versions are in this repository). In the newer version, the file lib/coq/user-contrib/iris/bi/tactics.vo does not exist any more. However, even after the update, the file exists in my opam switch. Shouldn't opam cleanly remove the files of the old version during the upgrade?

(I have not yet tried to reproduce this.)

# opam config report
# opam-version      2.0.7 
# self-upgrade      no
# system            arch=x86_64 os=linux os-distribution=debian os-version=testing
# solver            builtin-mccs+glpk
# install-criteria  -removed,-count[version-lag,request],-count[version-lag,changed],-changed
# upgrade-criteria  -removed,-count[version-lag,solution],-new
# jobs              8
# repositories      4 (http), 3 (local), 2 (version-controlled) (default repo at 609e1435)
# pinned            6 (rsync)
# current-switch    /home/r/Dokumente/Unisachen/iris/coq-users/examples

[rjbou]

It should indeed. Is it the same issues than #4207?

[RalfJung]

Quite possible -- I have no clue about the underlying cause, but the symptoms are the same.

Is there a way to ask opam which files it thinks are part of a package, to make it easier to check if something went wrong there?

[rjbou]

The command opam show --list-files <pkg> gives you that information.

[RalfJung]

Hm, that looks as expected for a few random things that I just checked.

[RalfJung]

I also tried the same upgrade again and this time the file was removed correctly.

But sometimes opam seems to lose track of the files it installed, and of course I only notice this waaay later when there is an update which actually removes a file (which is rare for these packages).

[RalfJung]

I just had the problem again:

The following actions will be performed:
  ↗ upgrade coq-stdpp         dev.2020-10-30.0.402f2d6a to dev.2020-11-11.2.6385b547 [required by coq-iris]
  ∗ install coq-iris          dev.2020-11-26.2.03b317f4                              [required by coq-iron-builddep]
  ↗ upgrade coq-orc11         dev.2020-10-30.0.b186bfe1 to dev.2020-11-12.1.2d9dd724 [uses coq-stdpp]
  ∗ install coq-iron-builddep ~dev*

coq-iris wasn't even installed (it seems it got uninstalled some time ago, not sure when), but stale files still existed that I had to delete manually:

rm /home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/iris/heap_lang -rf

This is using a local switch that is symlinked into a whole bunch of directories, maybe that is part of the problem?

[RalfJung]

The command opam show --list-files gives you that information.

I still don't know how to reproduce this, but when this just occurred again for the "coq-iris" package, I did a quick test with the "coq-stdpp" package:

$ opam show --list-files coq-stdpp
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/base.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/base.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/base.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/binders.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/binders.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/binders.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/boolset.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/boolset.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/boolset.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/coGset.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/coGset.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/coGset.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/coPset.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/coPset.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/coPset.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/countable.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/countable.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/countable.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/decidable.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/decidable.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/decidable.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/fin.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/fin.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/fin.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/fin_map_dom.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/fin_map_dom.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/fin_map_dom.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/fin_maps.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/fin_maps.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/fin_maps.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/fin_sets.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/fin_sets.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/fin_sets.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/finite.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/finite.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/finite.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/functions.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/functions.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/functions.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/gmap.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/gmap.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/gmap.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/gmultiset.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/gmultiset.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/gmultiset.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/hashset.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/hashset.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/hashset.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/hlist.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/hlist.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/hlist.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/infinite.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/infinite.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/infinite.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/lexico.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/lexico.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/lexico.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/list.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/list.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/list.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/list_numbers.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/list_numbers.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/list_numbers.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/listset.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/listset.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/listset.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/listset_nodup.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/listset_nodup.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/listset_nodup.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/mapset.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/mapset.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/mapset.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/namespaces.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/namespaces.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/namespaces.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/nat_cancel.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/nat_cancel.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/nat_cancel.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/natmap.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/natmap.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/natmap.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/nmap.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/nmap.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/nmap.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/numbers.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/numbers.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/numbers.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/option.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/option.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/option.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/options.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/options.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/options.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/orders.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/orders.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/orders.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/pmap.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/pmap.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/pmap.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/prelude.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/prelude.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/prelude.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/pretty.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/pretty.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/pretty.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/proof_irrel.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/proof_irrel.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/proof_irrel.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/propset.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/propset.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/propset.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/relations.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/relations.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/relations.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/sets.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/sets.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/sets.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/sorting.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/sorting.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/sorting.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/streams.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/streams.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/streams.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/stringmap.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/stringmap.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/stringmap.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/strings.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/strings.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/strings.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/tactics.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/tactics.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/tactics.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/telescopes.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/telescopes.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/telescopes.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/vector.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/vector.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/vector.vo
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/zmap.glob
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/zmap.v
/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq/user-contrib/stdpp/zmap.vo

So, opam does know that all these files belong to stdpp. Then I did opam uninstall coq-stdpp, followed by

$ ls -l _opam/lib/coq/user-contrib/stdpp/
total 13508
-rw-r--r-- 1 r r  187734  1. Feb 13:08 base.glob
-rw-r--r-- 1 r r   58939  1. Feb 13:08 base.v
-rw-r--r-- 1 r r  321627  1. Feb 13:08 base.vo
-rw-r--r-- 1 r r   19455  1. Feb 13:08 binders.glob
-rw-r--r-- 1 r r    4613  1. Feb 13:08 binders.v
-rw-r--r-- 1 r r   83109  1. Feb 13:08 binders.vo
-rw-r--r-- 1 r r    7590  1. Feb 13:08 boolset.glob
-rw-r--r-- 1 r r    1789  1. Feb 13:08 boolset.v
-rw-r--r-- 1 r r   55946  1. Feb 13:08 boolset.vo
-rw-r--r-- 1 r r   29865  1. Feb 13:08 coGset.glob
-rw-r--r-- 1 r r    7775  1. Feb 13:08 coGset.v
-rw-r--r-- 1 r r  115401  1. Feb 13:08 coGset.vo
-rw-r--r-- 1 r r  142048  1. Feb 13:08 coPset.glob
-rw-r--r-- 1 r r   18952  1. Feb 13:08 coPset.v
-rw-r--r-- 1 r r  190885  1. Feb 13:08 coPset.vo
-rw-r--r-- 1 r r   63415  1. Feb 13:08 countable.glob
-rw-r--r-- 1 r r   12504  1. Feb 13:08 countable.v
-rw-r--r-- 1 r r  148933  1. Feb 13:08 countable.vo
-rw-r--r-- 1 r r   33125  1. Feb 13:08 decidable.glob
-rw-r--r-- 1 r r   10245  1. Feb 13:08 decidable.v
-rw-r--r-- 1 r r   74643  1. Feb 13:08 decidable.vo
-rw-r--r-- 1 r r   16055  1. Feb 13:08 fin.glob
-rw-r--r-- 1 r r   68669  1. Feb 13:08 finite.glob
-rw-r--r-- 1 r r   15688  1. Feb 13:08 finite.v
-rw-r--r-- 1 r r  183933  1. Feb 13:08 finite.vo
-rw-r--r-- 1 r r  100958  1. Feb 13:08 fin_map_dom.glob
-rw-r--r-- 1 r r   12274  1. Feb 13:08 fin_map_dom.v
-rw-r--r-- 1 r r  215812  1. Feb 13:08 fin_map_dom.vo
-rw-r--r-- 1 r r  807968  1. Feb 13:08 fin_maps.glob
-rw-r--r-- 1 r r  113731  1. Feb 13:08 fin_maps.v
-rw-r--r-- 1 r r 1093488  1. Feb 13:08 fin_maps.vo
-rw-r--r-- 1 r r  104241  1. Feb 13:08 fin_sets.glob
-rw-r--r-- 1 r r   18477  1. Feb 13:08 fin_sets.v
-rw-r--r-- 1 r r  218316  1. Feb 13:08 fin_sets.vo
-rw-r--r-- 1 r r    4405  1. Feb 13:08 fin.v
-rw-r--r-- 1 r r   55629  1. Feb 13:08 fin.vo
-rw-r--r-- 1 r r    7784  1. Feb 13:08 functions.glob
-rw-r--r-- 1 r r    1307  1. Feb 13:08 functions.v
-rw-r--r-- 1 r r   40564  1. Feb 13:08 functions.vo
-rw-r--r-- 1 r r   68925  1. Feb 13:08 gmap.glob
-rw-r--r-- 1 r r   14617  1. Feb 13:08 gmap.v
-rw-r--r-- 1 r r  190439  1. Feb 13:08 gmap.vo
-rw-r--r-- 1 r r  114467  1. Feb 13:08 gmultiset.glob
-rw-r--r-- 1 r r   25937  1. Feb 13:08 gmultiset.v
-rw-r--r-- 1 r r  252836  1. Feb 13:08 gmultiset.vo
-rw-r--r-- 1 r r   54126  1. Feb 13:08 hashset.glob
-rw-r--r-- 1 r r    7311  1. Feb 13:08 hashset.v
-rw-r--r-- 1 r r  117382  1. Feb 13:08 hashset.vo
-rw-r--r-- 1 r r   10382  1. Feb 13:08 hlist.glob
-rw-r--r-- 1 r r    2186  1. Feb 13:08 hlist.v
-rw-r--r-- 1 r r   54259  1. Feb 13:08 hlist.vo
-rw-r--r-- 1 r r   20808  1. Feb 13:08 infinite.glob
-rw-r--r-- 1 r r    6393  1. Feb 13:08 infinite.v
-rw-r--r-- 1 r r  106593  1. Feb 13:08 infinite.vo
-rw-r--r-- 1 r r   36303  1. Feb 13:08 lexico.glob
-rw-r--r-- 1 r r    6046  1. Feb 13:08 lexico.v
-rw-r--r-- 1 r r   91575  1. Feb 13:08 lexico.vo
-rw-r--r-- 1 r r 1147692  1. Feb 13:08 list.glob
-rw-r--r-- 1 r r   42213  1. Feb 13:08 list_numbers.glob
-rw-r--r-- 1 r r    7500  1. Feb 13:08 list_numbers.v
-rw-r--r-- 1 r r   92653  1. Feb 13:08 list_numbers.vo
-rw-r--r-- 1 r r   11050  1. Feb 13:08 listset.glob
-rw-r--r-- 1 r r    5641  1. Feb 13:08 listset_nodup.glob
-rw-r--r-- 1 r r    1852  1. Feb 13:08 listset_nodup.v
-rw-r--r-- 1 r r   54943  1. Feb 13:08 listset_nodup.vo
-rw-r--r-- 1 r r    2932  1. Feb 13:08 listset.v
-rw-r--r-- 1 r r   66951  1. Feb 13:08 listset.vo
-rw-r--r-- 1 r r  206050  1. Feb 13:08 list.v
-rw-r--r-- 1 r r 1703212  1. Feb 13:08 list.vo
-rw-r--r-- 1 r r   24471  1. Feb 13:08 mapset.glob
-rw-r--r-- 1 r r    5808  1. Feb 13:08 mapset.v
-rw-r--r-- 1 r r  104335  1. Feb 13:08 mapset.vo
-rw-r--r-- 1 r r   12115  1. Feb 13:08 namespaces.glob
-rw-r--r-- 1 r r    4670  1. Feb 13:08 namespaces.v
-rw-r--r-- 1 r r   71923  1. Feb 13:08 namespaces.vo
-rw-r--r-- 1 r r   12837  1. Feb 13:08 nat_cancel.glob
-rw-r--r-- 1 r r    4608  1. Feb 13:08 nat_cancel.v
-rw-r--r-- 1 r r   63491  1. Feb 13:08 nat_cancel.vo
-rw-r--r-- 1 r r   80456  1. Feb 13:08 natmap.glob
-rw-r--r-- 1 r r   15952  1. Feb 13:08 natmap.v
-rw-r--r-- 1 r r  177136  1. Feb 13:08 natmap.vo
-rw-r--r-- 1 r r   11745  1. Feb 13:08 nmap.glob
-rw-r--r-- 1 r r    3385  1. Feb 13:08 nmap.v
-rw-r--r-- 1 r r   81687  1. Feb 13:08 nmap.vo
-rw-r--r-- 1 r r  258990  1. Feb 13:08 numbers.glob
-rw-r--r-- 1 r r   50978  1. Feb 13:08 numbers.v
-rw-r--r-- 1 r r  287496  1. Feb 13:08 numbers.vo
-rw-r--r-- 1 r r   88598  1. Feb 13:08 option.glob
-rw-r--r-- 1 r r      55  1. Feb 13:08 options.glob
-rw-r--r-- 1 r r     551  1. Feb 13:08 options.v
-rw-r--r-- 1 r r    1790  1. Feb 13:08 options.vo
-rw-r--r-- 1 r r   19743  1. Feb 13:08 option.v
-rw-r--r-- 1 r r  167196  1. Feb 13:08 option.vo
-rw-r--r-- 1 r r   14159  1. Feb 13:08 orders.glob
-rw-r--r-- 1 r r    3726  1. Feb 13:08 orders.v
-rw-r--r-- 1 r r   54270  1. Feb 13:08 orders.vo
-rw-r--r-- 1 r r   65499  1. Feb 13:08 pmap.glob
-rw-r--r-- 1 r r   14124  1. Feb 13:08 pmap.v
-rw-r--r-- 1 r r  174971  1. Feb 13:08 pmap.vo
-rw-r--r-- 1 r r     496  1. Feb 13:08 prelude.glob
-rw-r--r-- 1 r r     187  1. Feb 13:08 prelude.v
-rw-r--r-- 1 r r   44588  1. Feb 13:08 prelude.vo
-rw-r--r-- 1 r r   23715  1. Feb 13:08 pretty.glob
-rw-r--r-- 1 r r    5028  1. Feb 13:08 pretty.v
-rw-r--r-- 1 r r  160062  1. Feb 13:08 pretty.vo
-rw-r--r-- 1 r r    7750  1. Feb 13:08 proof_irrel.glob
-rw-r--r-- 1 r r    1884  1. Feb 13:08 proof_irrel.v
-rw-r--r-- 1 r r   26215  1. Feb 13:08 proof_irrel.vo
-rw-r--r-- 1 r r   13756  1. Feb 13:08 propset.glob
-rw-r--r-- 1 r r    2527  1. Feb 13:08 propset.v
-rw-r--r-- 1 r r   61541  1. Feb 13:08 propset.vo
-rw-r--r-- 1 r r  101348  1. Feb 13:08 relations.glob
-rw-r--r-- 1 r r   17976  1. Feb 13:08 relations.v
-rw-r--r-- 1 r r  131550  1. Feb 13:08 relations.vo
-rw-r--r-- 1 r r  268363  1. Feb 13:08 sets.glob
-rw-r--r-- 1 r r   54828  1. Feb 13:08 sets.v
-rw-r--r-- 1 r r  487699  1. Feb 13:08 sets.vo
-rw-r--r-- 1 r r   45306  1. Feb 13:08 sorting.glob
-rw-r--r-- 1 r r    9906  1. Feb 13:08 sorting.v
-rw-r--r-- 1 r r  110224  1. Feb 13:08 sorting.vo
-rw-r--r-- 1 r r    7686  1. Feb 13:08 streams.glob
-rw-r--r-- 1 r r    2184  1. Feb 13:08 streams.v
-rw-r--r-- 1 r r   46427  1. Feb 13:08 streams.vo
-rw-r--r-- 1 r r    9510  1. Feb 13:08 stringmap.glob
-rw-r--r-- 1 r r    2639  1. Feb 13:08 stringmap.v
-rw-r--r-- 1 r r   68244  1. Feb 13:08 stringmap.vo
-rw-r--r-- 1 r r   12289  1. Feb 13:08 strings.glob
-rw-r--r-- 1 r r    4189  1. Feb 13:08 strings.v
-rw-r--r-- 1 r r  160601  1. Feb 13:08 strings.vo
-rw-r--r-- 1 r r   22771  1. Feb 13:08 tactics.glob
-rw-r--r-- 1 r r   27717  1. Feb 13:08 tactics.v
-rw-r--r-- 1 r r  117327  1. Feb 13:08 tactics.vo
-rw-r--r-- 1 r r   28156  1. Feb 13:08 telescopes.glob
-rw-r--r-- 1 r r    7241  1. Feb 13:08 telescopes.v
-rw-r--r-- 1 r r   65650  1. Feb 13:08 telescopes.vo
-rw-r--r-- 1 r r   63138  1. Feb 13:08 vector.glob
-rw-r--r-- 1 r r   13922  1. Feb 13:08 vector.v
-rw-r--r-- 1 r r  127403  1. Feb 13:08 vector.vo
-rw-r--r-- 1 r r   17611  1. Feb 13:08 zmap.glob
-rw-r--r-- 1 r r    4201  1. Feb 13:08 zmap.v
-rw-r--r-- 1 r r   93996  1. Feb 13:08 zmap.vo

So, even though opam knew about these files, it still did not uninstall them.

[kit-ty-kate]

is this in a docker container by any chance? I've tried it locally and every files and directories were successfully removed

[RalfJung]

No, it's directly on my Debian testing system, no docker or other kind of container involved.

[rjbou]

Is it possible that another package changes those files ?

[RalfJung]

Well, it's hard to definitely answer "no" to such a question^^. No other package should do that.

I could imagine that deinstalling or reinstalling coq could clean the user-contrib folder. But coq-stdpp depends on coq so it will usually be deinstalled first anyway, right? Not sure what to test to check this hypothesis.

[RalfJung]

I just had this again. What should I do to figure out more about what is happening? To reiterate, I have an opam prefix in a state where opam show --list-files PACKAGE lists some files but opam uninstall PACKAGE will not uninstall those files.

I can snapshot the prefix into a tarball and upload it somewhere for you to investigate, but I fear that might affect the results -- at least, after I unpacked the tarball elsewhere on my local system, opam show --list-files PACKAGE looks different than before. It now says (modified since) for each file, which it did not originally.

[RalfJung]

Yeah, I have here an affected _opam folder that, when I cp -a it elsewhere, still shows the problem, but when I tar and then untar it, opam somehow notices that. How can I send you that folder?

[RalfJung]

It seems like with --acl, enough is preserved. I have uploaded a tarball; with that, the issues is reproducible as follows:

tar -xzf opam-bug-4419.tar.gz
opam show --list-files coq-stdpp # notice the files are listed as expected
ls _opam/lib/coq/user-contrib/stdpp # and they exist here
opam uninstall coq-stdpp -y
ls _opam/lib/coq/user-contrib/stdpp # but now they still exist!

[RalfJung]

@rjbou you added the "can't reproduce" label a while ago. Three months ago I provided detailed instructions to reproduce the problem. Could you have a look and maybe remove the label? :)

[mattam82]

Could it be that opam is confused because the parent directory (user-contrib) gets modified by other Coq contribs?

[dra27]

@RalfJung - thanks for the reproduction case, but we've all been rather busy with opam 2.1, which by 10 Mar was "frozen" for anything other than regressions as we were moving towards release candidate. The second, and hopefully final, release candidate was tagged yesterday, so I'm sure this issue will being dealt with as we finalise plans for opam 2.2.0.

[rjbou]

Taking a look to changes file, we can see that opam marked the changes made by coq-stdpp as changing content instead of adding it.

$ head -n 4 opam-4419/.opam-switch/install/coq-stdpp.changes 
contents-changed: [
  "lib/coq/user-contrib/stdpp/base.glob" {"F:S187734T1615210369.72"}
  "lib/coq/user-contrib/stdpp/base.v" {"F:S58939T1615210369.57"}
  "lib/coq/user-contrib/stdpp/base.vo" {"F:S311977T1615210369.42"}
$ head -n 4 _opam/.opam-switch/install/coq-stdpp.changes # local testing to add/remove/upgrade coq-stdpp
added: [
  "lib/coq/user-contrib/stdpp" {"D"}
  "lib/coq/user-contrib/stdpp/base.glob" {"F:S187734T1628178523.15"}
  "lib/coq/user-contrib/stdpp/base.v" {"F:S58939T1628178522.99"}

In fact, in you switch, you are in a state where no package have the information to delete lib/coq/user-contrib nor lib/coq/user-contrib/stdpp.

$ cd opam-4419/.opam-switch/install
$ grep contents-changed *.changes
coq-stdpp.changes:contents-changed: [

Only coq-stdpp doesn't "own" its files, they are marked as modifying the existent

$ grep '{"D"}' *.changes | grep user-contrib
coq.changes:  "lib/coq/user-contrib/Ltac2" {"D"}

The only package that creates a directory is coq, and it doesn't set as it created lib/coq/user-contrib before as it should be. On my try-to-reproduce switch I have

$ grep '{"D"}' _opam/.opam-switch/install/*.changes | grep user-contrib
_opam/.opam-switch/install/coq.changes:  "lib/coq/user-contrib" {"D"}
_opam/.opam-switch/install/coq.changes:  "lib/coq/user-contrib/Ltac2" {"D"}
_opam/.opam-switch/install/coq-stdpp.changes:  "lib/coq/user-contrib/stdpp" {"D"}

That is the explanation on why you keep stale files. But how you end up with that switch state is still a mystery.

[RalfJung]

That is the explanation on why you keep stale files. But how you end up with that switch state is still a mystery.

My guess would be that at an earlier time, opam failed to remove those files, and then the next time I installed coq-stdpp opam was like "ah those files already exist, so I guess I will record coq-stdpp as changing those files". The way the system seems to work, if opam ever gets it wrong it will not be able to ever recover this switch.

FWIW after updating to opam 2.1 I am now fighting with "fun" errors like

# ocamlfind install -destdir "/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib" zarith META zarith.cma libzarith.a z.cmi q.cmi big_int_Z.cmi zarith_top.cma z.mli zarith.cmxa z.cmx q.cmx big_int_Z.cmx zarith.cmxs zarith.h q.mli big_int_Z.mli zarith.a z.cmti q.cmti big_int_Z.cmti -optional dllzarith.so
# ocamlfind: Package zarith is already installed
[...]
# [ERROR] It appears that the num library was previously installed to your system
#         compiler's lib directory, probably by a faulty opam package.
#         You will need to remove arith_flags.*, arith_status.*, big_int.*,
#         int_misc.*, nat.*, num.*, ratio.*, nums.*, libnums.* and
#         stublibs/dllnums.* from /usr/lib/ocaml.

I suspect this is the same problem -- zarith files were not properly deleted when it got uninstalled for an update. (The error at the end is totally wrong, I never run opam as root so it definitely did not ever put anything into /usr/lib/ocaml. It is asking me to delete files that were installed by apt/dpkg, which is super dangerous. I had to delete things from this switch instead, and most of the files it lists do not exist -- and I had to remove stublibs/dllzarith.so which is not listed as needing removal.)

I assume I have to give up on all my switches and re-create them all from scratch. :(

[rjbou]

That's the mystery, why opam failed to remove those files in the first place. See PR #4917, it adds an option to opam clean that removes remaining files not referenced by installed packages. If you want to test.

[RalfJung]

FWIW I just had this happen again in a switch that I just recently created after updating to opam 2.1 (since as mentioned above, the automatic upgrade entirely failed): a file was removed in a package upgrade, but the file still exists in the opam switch.

Is it possible that this has something to do with the fact that this is a local (per-directory) switch that is associated with several directories by symlinking the _opam directory?

[RalfJung]

I thought this might have to do with me using system ocaml (which has caused trouble in the past), but I just saw the same problem in a switch that does not use system ocaml. I had recently pinned an already installed package to a git repository, and now as part of updating the pin opam decided it had to reinstall everything ("upstream or system changes" in ocaml-variants), and then when it uninstalled that pinned package all its files were left behind.

[na4zagin3]

@RalfJung then the problem may be the same one as I described at https://github.com/ocaml/opam/issues/5132 OPAM accidentally wipes out .changes files at some point before uninstalling packages. I found 1) it wipes out the files with specifying option --dry-run (#5132) 2) even without specifying option --dry-run, it wiped out the files by some condition (https://github.com/ocaml/opam/issues/5132#issuecomment-1118218497).