Stream: CUDW 2020

Topic: WG: coq-community


view this post on Zulip Karl Palmskog (Nov 22 2020 at 22:47):

I think we should have a dedicated coq-community working group, where we discuss and work on coq-community issues that are not addressed in other working groups: https://github.com/coq-community/manifesto/issues

view this post on Zulip Karl Palmskog (Nov 30 2020 at 13:44):

@Théo Zimmermann @Erik Martin-Dorel any ideas for how to handle dependent packages better than this? https://github.com/coq-community/chapar/pull/19/files --- essentially I have to repeat package names twice in the actions yml file...

view this post on Zulip Erik Martin-Dorel (Nov 30 2020 at 13:52):

Hi @Karl Palmskog (I guess I'll only be able to attend the video-call on tomorrow morning... but I saw your ping so here is a quick reply :)

To sum up, I see two working solutions, the easy one (the more concise) being:

replacing opam_file: … with opam_file: "."

    runs-on: ubuntu-latest
    strategy:
      matrix:
        image:
          - 'coqorg/coq:dev'
          - 'coqorg/coq:8.12'
          - 'coqorg/coq:8.11'
          - 'coqorg/coq:8.10'
      fail-fast: false
    steps:
      - uses: actions/checkout@v2
      - uses: coq-community/docker-coq-action@v1
        with:
          opam_file: "."
          custom_image: ${{ matrix.image }}

which should work out-of-the box to compile the 2 opam packages, as there is exactly 2 .opam files in the branch https://github.com/coq-community/chapar/tree/stores-ci (i.e., there is no extra .opam file in the branch that you wouldn't want to compile)

(anyway, let me know if after testing you dislike that solution (e.g., if you'd like to be more "explicit" regarding the naming of the packages))

view this post on Zulip Karl Palmskog (Nov 30 2020 at 13:54):

@Erik Martin-Dorel thanks, but the problem with that solution is that one doesn't get a separate job for each package.

view this post on Zulip Erik Martin-Dorel (Nov 30 2020 at 13:56):

OK but why do you want a separate job? to make the build parallel? which could't be done anyway IIUC, because the packages are mutually dependent…

view this post on Zulip Karl Palmskog (Nov 30 2020 at 13:56):

the idea is that packages often fail differently. For example, one might have 2 Coq packages, and then 3 OCaml packages using extracted Coq code

view this post on Zulip Karl Palmskog (Nov 30 2020 at 13:57):

then it saves me a ton of time debugging if I see that all Coq packages build fine through CI greenlight, and the error is with one of the OCaml packages

view this post on Zulip Erik Martin-Dorel (Nov 30 2020 at 13:57):

but is your question only related to that repo (with two dependent packages) or do you plan to focus on "monorepos", with totally independent packages?

view this post on Zulip Erik Martin-Dorel (Nov 30 2020 at 13:58):

because if you focus on that repo, I guess you could have the following two jobs:

one with opam_file: "coq-chapar.opam"
one with opam_file: "." (to check that everything compile)

view this post on Zulip Karl Palmskog (Nov 30 2020 at 13:58):

I mainly work with packages in the same repo that depend on each other in complex ways, not monorepos with independent packages.

view this post on Zulip Erik Martin-Dorel (Nov 30 2020 at 13:59):

so does this solution would work for you?

Erik Martin-Dorel said:

because if you focus on that repo, I guess you could have the following two jobs:

one with opam_file: "coq-chapar.opam"
one with opam_file: "." (to check that everything compile)

view this post on Zulip Erik Martin-Dorel (Nov 30 2020 at 14:01):

but I agree that if you'd have 3 dependent .opam files, that solution would not be applicable to build just the "intermediate layer" (with 2 .opam packages installed); if yes you might want to open a feature request in docker-coq-action :)

view this post on Zulip Karl Palmskog (Nov 30 2020 at 14:01):

it's better than what I have now, so I will probably use that, but it mixes together the installation for the Coq project and the OCaml project

view this post on Zulip Erik Martin-Dorel (Nov 30 2020 at 14:07):

OK @Karl Palmskog, anyway maybe we could discuss this a bit more in the week (but if docker-coq-action has to be further extended, I'd say it should be done in a generic way; otherwise the better solution could just be to customize the custom_script, see e.g. this repo where we have a similar use case with OCaml deps: https://github.com/validsdp/validsdp/blob/e329be44394b125cc7dc0c73f3943cc76e7978d4/.github/workflows/coq-action.yml#L27-L62)

view this post on Zulip Karl Palmskog (Nov 30 2020 at 14:09):

sure, am open for discussing this, but in that case [if there's no obvious generic extension] I'm probably going to write some template to generate the custom_script


Last updated: Oct 16 2021 at 09:07 UTC