Opam publish fails - Githubissues

DmxLarchey commented 2 years ago

Hi @jjhugues,

I would like to publish this repo using opam publish but this fails. Here is a trace of what happens. Any ideas? I am using opam publish 2.1.0.

elza Kruskal-Trees % opam publish 

The following will be published:
  - coq-kruskal-trees version 1.0 with opam file at /users/larchey/GitHub/Kruskal-Trees/coq-kruskal-trees.opam
    archive at https://github.com/DmxLarchey/Kruskal-Trees/archive/1.0.tar.gz

You will be shown the patch before submitting.
Please confirm the above data. Continue ?  [Y/n] Y
Please generate a Github token at https://github.com/settings/tokens/new to allow access.
The "public_repo" scope is required ("repo" if submitting to a private opam repository).

Please enter your GitHub personal access token: 
[ERROR] HTTP Error 400 Bad Request
        Headers:
        Server: GitHub.com
        Date: Tue, 08 Nov 2022 14:58:06 GMT
        Transfer-Encoding: chunked
        Vary: Accept-Encoding, Accept, X-Requested-With
        X-GitHub-Request-Id: E77A:CE9D:22150A8:2293847:636A6E7E

        Body:

Seems there have been troubles with GitHub token API in the past. Is opam publish not the way to proceed ?

DmxLarchey commented 2 years ago

The problem is that I now need Kruskal-Trees to be published for the CI of Kruskal-reboot to run. Can I add an opam dependency on a private repository?

jjhugues commented 2 years ago

Publishing is not necessary, you can also do this (this is what I did for my own project)

add opam pin add -n -y coq-kruskal-trees https://github.com/DmxLarchey/Kruskal-Trees.git

to the workflow file (see before_install in https://github.com/Oqarina/oqarina/blob/main/.github/workflows/main.yml)

then either add an explicit opam install coq-kruskal-trees in the makefile, or you let the CI do it. By default it will run opam install --deps-only .. If the dependency is listed in the .opam file, and the repo pinned, it will find it (again, see https://github.com/Oqarina/oqarina/blob/main/coq-oqarina.opam).

Adding a dependency to a private repo will be complicated. The CI will need to authenticate first. Not impossible, but you'll have to play with tokens.

DmxLarchey commented 2 years ago

@jjhugues Thanks for the opam pin tip which allow (seemingly) to locally enrich the opam library. However, I am still failing to publish the Kruskal-Trees library on opam.

Problems with access tokens and then strange failure on git fetch, see issue (https://github.com/ocaml-opam/opam-publish/issues/86) on opam-publish. But the PR (https://github.com/ocaml/opam-repository/pull/22473) has been create on opam finally !!

DmxLarchey commented 2 years ago

I also realized that I should publish not under (https://github.com/ocaml/opam-repository) but under (https://github.com/coq/opam-coq-archive) instead ... dumb of me.

jjhugues commented 2 years ago

No worry, the Coq team will redirect you to the right repo when they process your request. Note I would recommend you keep the pinned repo for Kruksal-reboot, this will ensure any subsequent build will be based on the most recent code base, and not a release.

DmxLarchey commented 2 years ago

Tried under (https://github.com/coq/opam-coq-archive/pull/2377) but the integrated CI failed ...

jjhugues commented 2 years ago

Tried under (coq/opam-coq-archive#2377) but the integrated CI failed ...

Indeed, the error messages is clear:

# coq_makefile -f _CoqProject -o Makefile.coq
# make[1]: coq_makefile: No such file or directory

Looking at other packages, they also specify ocaml and ocamlfind as dependencies. I think the maintainers will point to the missing bits.

DmxLarchey commented 2 years ago

I did update the opam file directly on the PR to include ocaml and ocamlfind and limit further coq to exclude dev.

DmxLarchey commented 2 years ago

That is it. coq-kruskal-trees 1.0 is now part of (https://coq.inria.fr/opam/released).

jjhugues commented 2 years ago

This is great news! Do you want to extend the README with installation instructions? See for instance https://github.com/liyishuai/coq-json for an example

DmxLarchey commented 2 years ago

Copy the remark from PR #2 about possible documentation:

Perhaps illustration on how to use induction on ltree X or else what can be done with ltree_fall : X -> list (ltree X) -> Prop to manipulate Σ-types { t | ltree_fall P t } with ltree_fall_rect instead of a combination of ltree_rect and ltree_fall_fix. Possibly, the design of a tailored induction principle for the Σ-type { t | ltree_fall P t } ?

DmxLarchey commented 9 months ago

I am now proceeding via the GH interface to push PR in coq-opam and I had no more credential problems. I am closing this issue.

DmxLarchey / Kruskal-Trees

Opam publish fails #1