Some packages that don't have an official opam repository version don't need commit hashes -- InfSeqExt?

[brando90]

using commit didn't help (I think?): here is where I ran:

#
git clone git@github.com:DistributedComponents/InfSeqExt.git deps/InfSeqExt
(cd deps/InfSeqExt && opam install -y .)
# above worked, but leaving code bellow in case it's needed
git clone git@github.com:DistributedComponents/InfSeqExt.git deps/InfSeqExt
(cd deps/InfSeqExt && git checkout 91b2d9bdc580c7ccb5bf2f50fffb6ebabab2715c && git rev-parse HEAD)
(cd deps/InfSeqExt && opam install -y .)

output:

(iit_synthesis) brando9~/proverbot9001 $ (cd deps/InfSeqExt && opam install -y .)
[WARNING] Failed checks on coq-inf-seq-ext package definition from source at
          git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/InfSeqExt#HEAD:
  warning 62: License doesn't adhere to the SPDX standard, see https://spdx.org/licenses/: "Unknown"
[NOTE] Package coq-inf-seq-ext is currently pinned to git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/InfSeqExt#master (version dev).
coq-inf-seq-ext is now pinned to git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/InfSeqExt#HEAD (version dev)
[coq-inf-seq-ext.dev] synchronised (git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/InfSeqExt#HEAD)
[WARNING] Failed checks in opam file from upstream of coq-inf-seq-ext:
  warning 62: License doesn't adhere to the SPDX standard, see https://spdx.org/licenses/: "Unknown"
The following actions will be performed:
  ↻ recompile coq-inf-seq-ext dev*

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  2/4: [coq-inf-seq-ext: dune build]
⊘ removed   coq-inf-seq-ext.dev
∗ installed coq-inf-seq-ext.dev
Done.

maybe developers will help? https://github.com/DistributedComponents/InfSeqExt/issues/7

[HazardousPeach]

I'm not sure what you're question is. That's a successful install. opam install doesn't need a version or url here because it's using the path specifier ".", which says to pick up the .opam file in the current directory.

[brando90]

Got it. I think the warnings confused me.

I am documenting the explicit commits here in case they break for anyone else later: For co1 8.12

# Create the coq 8.12 switch
opam switch create coq-8.12 4.07.1
eval $(opam env --switch=coq-8.12 --set-switch)
opam pin add -y coq 8.12.2

# Install the packages that can be installed directly through opam
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
...
# Some packages that don't have an official opam repository version don't need commit hashes?
git clone git@github.com:DistributedComponents/InfSeqExt.git deps/InfSeqExt
(cd deps/InfSeqExt && opam install -y .)
# above worked but bellow might have not, but leaving code bellow in case it's needed ref: https://github.com/UCSD-PL/proverbot9001/issues/91
#git clone git@github.com:DistributedComponents/InfSeqExt.git deps/InfSeqExt
#(cd deps/InfSeqExt && git checkout 91b2d9bdc580c7ccb5bf2f50fffb6ebabab2715c && git rev-parse HEAD)
#(cd deps/InfSeqExt && opam install -y .)

and for coq 8.10

# - Create the 8.10.2 switch
opam switch create coq-8.10 4.07.1
eval $(opam env --switch=coq-8.10 --set-switch)
opam pin add -y coq 8.10.2
# - Install dependency packages for 8.10
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
# We don't need it in all opam switches due to incompatabilities: Run `opam repository add <coq-proj> --all-switches|--set-default' to use it in all existing switches, or in newly created switches, respectively. cmd: opam repository add coq-extra-dev --all-switches
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add psl-opam-repository https://github.com/uds-psl/psl-opam-repository.git

...

opam install -y coq-inf-seq-ext
# dev seems to work but providing the bottom just in case, bellow seems to work but some warning appear
#opam pin add -y coq-inf-seq-ext git+https://github.com/DistributedComponents/InfSeqExt.git#19f6359e65ecb872d49208f60bf8951fb76fe091

[brando90]

double checked 8.10:

(metalearning_gpu) brando9~/proverbot9001/deps/StructTact $ eval $(opam env --switch=coq-8.10 --set-switch)
(metalearning_gpu) brando9~/proverbot9001/deps/StructTact $
(metalearning_gpu) brando9~/proverbot9001/deps/StructTact $
(metalearning_gpu) brando9~/proverbot9001/deps/StructTact $ opam pin add -y coq-inf-seq-ext git+https://github.com/DistributedComponents/InfSeqExt.git#19f6359e65ecb872d49208f60bf8951fb76fe091

\[NOTE] Package coq-inf-seq-ext is already pinned to git+https://github.com/DistributedComponents/InfSeqExt.git#19f6359e65ecb872d49208f60bf8951fb76fe091
       (version dev).
[coq-inf-seq-ext.dev] synchronised (no changes)
[WARNING] Failed checks on coq-inf-seq-ext package definition from source at
          git+https://github.com/DistributedComponents/InfSeqExt.git#19f6359e65ecb872d49208f60bf8951fb76fe091:
  warning 62: License doesn't adhere to the SPDX standard, see https://spdx.org/licenses/: "Proprietary"
coq-inf-seq-ext is now pinned to git+https://github.com/DistributedComponents/InfSeqExt.git#19f6359e65ecb872d49208f60bf8951fb76fe091 (version dev)

Already up-to-date.
Nothing to do.
(metalearning_gpu) brando9~/proverbot9001/deps/StructTact $