How does one install a opam coq package that has been successfully install previously?

Question

I know this has been installed before becuase the proverbot9001 project has used it before. So how do I go about finding what exactly is the issue in my set up that doesn't let me install it? Any install is fine I suppose

(iit_synthesis) brando9~/proverbot9001 $ opam install -y coq-ext-lib

The following actions will be performed:
  ∗ install coq-ext-lib dev

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⬇ retrieved coq-ext-lib.dev  (git+https://github.com/coq-community/coq-ext-lib#master)
[ERROR] The compilation of coq-ext-lib.dev failed at "make -j127 theories".

#=== ERROR while compiling coq-ext-lib.dev ====================================#
# context     2.1.3 | linux/x86_64 | ocaml-base-compiler.4.07.1 | https://coq.inria.fr/opam/extra-dev#2022-12-06 09:40
# path        ~/.opam/coq-8.10/.opam-switch/build/coq-ext-lib.dev
# command     /usr/bin/make -j127 theories
# exit-code   2
# env-file    ~/.opam/log/coq-ext-lib-1328047-92e9b2.env
# output-file ~/.opam/log/coq-ext-lib-1328047-92e9b2.out
### output ###
# [...]
# make[2]: *** [Makefile.coq:658: theories/Tactics/BoolTac.vo] Error 1
# make[2]: *** Waiting for unfinished jobs....
# File "./theories/Programming/With.v", line 59, characters 0-39:
# Warning: Declaring a scope implicitly is deprecated; use in advance an
# explicit "Declare Scope struct_scope.". [undeclared-scope,deprecated]
# File "./theories/Data/ListFirstnSkipn.v", line 51, characters 0-101:
# Error: This command does not support this attribute: global.
#
# make[2]: *** [Makefile.coq:658: theories/Data/ListFirstnSkipn.vo] Error 1
# make[1]: *** [Makefile.coq:321: all] Error 2
# make[1]: Leaving directory '/lfs/ampere4/0/brando9/.opam/coq-8.10/.opam-switch/build/coq-ext-lib.dev'
# make: *** [Makefile:7: theories] Error 2



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build coq-ext-lib dev
└─
╶─ No changes have been performed

my set up:

(iit_synthesis) brando9~/proverbot9001 $ opam switch
#  switch                                                  compiler                       description
→  coq-8.10                                                ocaml-base-compiler.4.07.1     coq-8.10
   coq-8.12                                                ocaml-base-compiler.4.07.1     coq-8.12
   coq-8.14                                                ocaml-base-compiler.4.07.1     coq-8.14
   ocaml-variants.4.07.1+flambda_coq-serapi.8.11.0+0.11.1  ocaml-variants.4.07.1+flambda  ocaml-variants.4.07.1+flambda_coq-serapi.8.11.0+0.11.1

[NOTE] Current switch is set locally through the OPAMSWITCH variable.
       The current global system switch is coq-8.14.
(iit_synthesis) brando9~/proverbot9001 $ opam list
# Packages matching: installed
# Name                   # Installed  # Synopsis
base                     v0.14.0      Full standard library replacement for OCaml
base-bigarray            base
base-threads             base
base-unix                base
cmdliner                 1.0.4        Declarative definition of command line interfaces for OCaml
conf-findutils           1            Virtual package relying on findutils
coq                      8.10.2       pinned to version 8.10.2
coq-fcsl-pcm             1.2.0        Partial Commutative Monoids
coq-inf-seq-ext          dev          Coq library for reasoning inductively and coinductively on infinite sequences
coq-int-map              8.10.0       Maps indexed by binary integers : IntMap
coq-mathcomp-algebra     1.11.0       Mathematical Components Library on Algebra
coq-mathcomp-bigenough   dev          A small library to do epsilon - N reasonning
coq-mathcomp-fingroup    1.11.0       Mathematical Components Library on finite groups
coq-mathcomp-ssreflect   1.11.0       Small Scale Reflection
coq-pocklington          dev          Pocklington's criterion for primality in Coq
coq-serapi               8.10.0+0.7.2 Serialization library and protocol for machine interaction with the Coq proof assistant
coq-smpl                 8.10.2       Smpl: An Extensible Tactic for Coq
coq-struct-tact          dev          Coq library of structural tactics and utility lemmas about lists and finite types
cppo                     1.6.9        Code preprocessor like cpp for OCaml
csexp                    1.5.1        Parsing and printing of S-expressions in Canonical form
dune                     3.6.1        Fast, portable, and opinionated build system
dune-configurator        3.6.1        Helper library for gathering system configuration
num                      1.4          The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml                    4.07.1       The OCaml compiler (virtual package)
ocaml-base-compiler      4.07.1       Official release 4.07.1
ocaml-compiler-libs      v0.12.4      OCaml compiler libraries repackaged
ocaml-config             1            OCaml Switch Configuration
ocaml-secondary-compiler 4.08.1-1     OCaml 4.08.1 Secondary Switch Compiler
ocamlfind                1.9.1        A library manager for OCaml
ocamlfind-secondary      1.9.1        Adds support for ocaml-secondary-compiler to ocamlfind
parsexp                  v0.14.2      S-expression parsing library
ppx_derivers             1.2.1        Shared [@@deriving] plugin registry
ppx_deriving             5.2.1        Type-driven code generation for OCaml
ppx_deriving_yojson      3.6.1        JSON codec generator for OCaml
ppx_import               1.9.1        A syntax extension for importing declarations from interface files
ppx_sexp_conv            v0.14.3      [@@deriving] plugin to generate S-expression conversion functions
ppxlib                   0.25.1       Standard library for ppx rewriters
result                   1.5          Compatibility Result module
seq                      base         Compatibility package for OCaml's standard iterator type starting from 4.07.
sexplib                  v0.14.0      Library for serializing OCaml values to and from S-expressions
sexplib0                 v0.14.0      Library containing the definition of S-expressions and some base converters
stdlib-shims             0.3.0        Backport some of the new stdlib features to older compiler
yojson                   2.0.2        Yojson is an optimized parsing and printing library for the JSON format

related:

• https://github.com/coq-community/coq-ext-lib/issues/131
• https://github.com/UCSD-PL/proverbot9001/issues/56

Answer 1

coq-ext-lib dev uses the current main branch on github as source for the code. If you go and look there, you will see that the opam file states explicitely that the version of coq for which the sources work go from 8.8 to any 8.9, and then to any version above 8.11. This means that the version 8.10 is explictely ruled out.

Either you have to choose to work with a version of coq that is not 8.10, or you have to choose to work with a numbered version of coq-ext-lib that is compatible with coq-8.10. I suggest coq-ext-lib.0.11.6 (looking at the opam file this is one is compatible) because the latest one coq-ext-lib.0.11.7 is not (again you can look at the opam file).