search

coq-community / docker-coq-action

GitHub Action using Docker-Coq [maintainers=@erikmd,@Zimmi48]
MIT License
12 stars 4 forks source link

before_install and matrix builds #64

Open jjhugues opened 3 years ago

jjhugues commented 3 years ago

Hi,

I followed recommendations from #22 and used before_install to add opam repositories to my build. I build for two versions of Coq, but it seems the before_install part is considered only for the second build, not the first one. Any idea what could go wrong?

See https://github.com/Oqarina/oqarina/blob/main/.github/workflows/main.yml and https://github.com/Oqarina/oqarina/runs/3612797755?check_suite_focus=true

For the failed log, it is apparent it did not add any additional repository Thanks,

jjhugues commented 3 years ago

The documentation for coq-json was misleading, and the 8.13 and dev docker images have different repositories settings, hence this issue.

erikmd commented 3 years ago

Hi @jjhugues, thanks for your report, and sorry I've just seen your comment.

Reopening this issue because maybe there's something to document better in this repo and/or in the docker-coq repo.

So I'll try have a look at the next docs-checking-time when preparing a new release.

yoogx commented 3 years ago

Hi,

Thanks for your interest. Actually I got confused by multiple facts unrelated to your project. Yet some points could be discussed either here or in docker-coq

1/ coq-json was not properly listing its opam repo, hence my initial confusion: the maintainer quickly fixed this one per https://github.com/liyishuai/coq-json/issues/1 -> my GitHub workflow should add the right opam repo

I got confused because my workflow worked with the -dev image, but not with the 8.13 image. I initially incriminated the before_script since I got inconsistant results for opam repo list (see 3 below), but I was wrong. It is the reason why I closed the issue.

2/ then I got another issue reported here ( https://github.com/coq-community/docker-coq/issues/30 ) when I tried to install coq-io -> my workflow should use the right Ocaml version or docker-coq uses a more recent Ocaml version. I understand this is a larger topic than my small project.

3/ finally I got stuck by this error https://github.com/Oqarina/oqarina/runs/3614110040?check_suite_focus=true when using the coq-dev docker

+ (script @ line 5) $ opam repo add --all-switches --set-default coq-extra-dev https://coq.inria.fr/opam/extra-dev/
222
Error:  Repository coq-extra-dev is already set up and points to https://coq.inria.fr/opam/extra-dev. To change that, use 'opam repository set-url'.

In other words, docker-coq images for 8.13 and -dev do not have the same opam repo installed. An examination of https://github.com/coq-community/docker-coq/blob/master/coq/dev/Dockerfile and https://github.com/coq-community/docker-coq/blob/master/coq/stable/Dockerfile confirms this.

I could change the before_script based on the version used, or dig opam doc to work around this but I got distracted by other activities. I now test only with 8.13.

In terms of documentation, you could decide to make the list of installed repo more visible in the README in both docker-coq and docker-coq-action. As a user, I did not intially expect to have different repo configured for these images, in retrospect I understand why they could be but this was confusing.

Hope this helps

erikmd commented 3 years ago

Thanks a lot Jerome for your feedback!

Indeed, I agree we'll need to make it explicit, in both docker-coq and docker-coq-action docs, that:

Regarding your use case, it was indeed a good idea to extend before_install, and note that even without using any opam-specific code, you could write either:

jjhugues commented 3 years ago

Thanks for the hint. I always forget any shell script works. I updated my workflow.