WG: coq-community · CUDW 2020 · Zulip Chat Archive

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

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...

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:

    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))

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.

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…

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

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

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?

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)

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.

Erik Martin-Dorel (Nov 30 2020 at 13:59):

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 :)

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

Erik Martin-Dorel (Nov 30 2020 at 14:07):

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

Stream: CUDW 2020

Topic: WG: coq-community

Karl Palmskog (Nov 22 2020 at 22:47):