iris/algebra/auth.vo has bad version number 81700 (expected 81601) for IRIS Coq

Question

Error:
File /home/kali/.opam/default/lib/coq/user-contrib/iris/algebra/auth.vo has
bad version number 81700 (expected 81601). It is corrupted or was compiled
with another version of Coq.

make[1]: *** [Makefile:793: learn2.vo] Error 1
make: *** [Makefile:409: all] Error 2

I have tried these three commands, but no avail

opam update
opam upgrade coq
opam upgrade coq-iris

Here is my coq file

From iris.algebra Require Import auth frac_auth numbers.
From iris.base_logic Require Import invariants.
From iris.heap_lang Require Import lang proofmode notation.
From iris.proofmode Require Import tactics.
From iris Require Import options.

(* Define the counter module *)
Module counter.
  Definition newcounter : val := λ: <>, ref #0.
  Definition inc : val := λ: "l", let: "n" := !"l" in CmpXchg "l" "n" ("n" + #1).
  Definition read : val := λ: "l", !"l".
End counter.

Section proof.
  Context `{!heapGS Σ}.
  Definition is_counter (l : loc) (n : Z) :=
    (l ↦ #n)%I.

  Lemma newcounter_spec :
    {{{ True }}}
      counter.newcounter #()
    {{{ l, RET #l; is_counter l 0 }}}.
  Proof.
    iIntros (Φ) "_ Hpost".
    wp_lam. wp_alloc l as "Hl".
    iApply "Hpost".
    iExact "Hl".
  Qed.

  Lemma inc_spec (l: loc) (n: Z) :
    {{{ is_counter l n }}}
      counter.inc #l
    {{{ RET #(); is_counter l (n + 1) }}}.
  Proof.
    iIntros (Φ) "Hl Hpost".
    wp_lam. wp_load. wp_pures.
    wp_bind (CmpXchg _ _ _).
    wp_cmpxchg_suc.
    iApply "Hpost". iFrame.
  Qed.

  Lemma read_spec (l: loc) (n: Z) :
    {{{ is_counter l n }}}
      counter.read #l
    {{{ RET #n; is_counter l n }}}.
  Proof.
    iIntros (Φ) "Hl Hpost".
    wp_lam. wp_load.
    iApply "Hpost". iFrame.
  Qed.
End proof.
```

Answer 1

This error means that you have an inconsistent state in your Coq installation, with the Iris library being compiled with Coq 8.17, but the Coq binary that you run being from Coq 8.16. Given that opam manages version constraints and should not lead you to this situation, the most likely explanation is that you have several concurrent installations of Coq that are interacting badly, or that opam got in a broken state after a partially unsuccessful upgrade.

Some pieces of advice for managing your Coq installation are usually:

• Pick only one way of installing Coq. E.g., if you are on Ubuntu, you can install Coq from sources using opam (including using the Coq Platform scripts), or pre-compiled binaries using Snap (official Coq Platform binaries) or using APT (Debian-maintained package). Choose just one and make sure you don't have concurrent installations. The opam way allows having several switches if you want concurrent installations of multiple versions of Coq.

• If you use opam manually, then it is generally recommended to pin the version of Coq that you want to have in your opam switch (see https://coq.inria.fr/opam-using.html).

• If you installed Coq using the Coq Platform scripts, then this pinning is not done. This means that you should avoid running opam upgrade. To install a new version of Coq with the Coq Platform scripts, you can run the updated Coq Platform scripts. They create a new switch. You can then remove your old switch if you don't need it anymore.

Besides these general pieces of advice, I can suggest running which coqc and coqc -v to confirm where the problem comes from. If there is a need for active interaction to debug this problem, then it may be more appropriate to ask for help on Coq's Zulip.