Skip to content

Install and commit for coq 8.12, InfSeqExt #7

@brando90

Description

@brando90

I tried:

git clone [email protected]:DistributedComponents/InfSeqExt.git deps/InfSeqExt
(cd deps/InfSeqExt && git checkout 91b2d9bdc580c7ccb5bf2f50fffb6ebabab2715c && git rev-parse HEAD)
(cd deps/InfSeqExt && opam install -y .)

but seems fishy, is this the recommended way to install it for coq 8.12?

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.

note one soln could be to push different version as you are developing to opam repo and not overwrite them.


related: UCSD-PL/proverbot9001#91

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions