-
Notifications
You must be signed in to change notification settings - Fork 3
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Towards one-switch images and docker-coq based GitHub actions #4
Comments
We should also consider adding annotations for GitHub actions. I tried doing that https://github.com/JasonGross/fiat-crypto/blob/add-matcher/.github/coq.json , but I haven't figured out how to have annotations without making a separate actions repo. Also, do docker images work on Mac and Windows? If not, we should also provide actions templates for Mac and Windows |
Thanks @erikmd , note that you may want to target 4.09.1 , also support for 4.10 is ready so hopefully it should a matter of a couple of days it can be merged. |
@JasonGross thanks for your comment
I didn't have a look at this for the moment, but sounds interesting indeed!
according to https://help.github.com/en/actions/building-actions/about-actions#types-of-actions:
|
and the detail of the supported HW/OS by github.com actions is given in
|
BTW @ejgallego
do you know if that 4.10 release would address the performance issue you had noticed? as in this case, we might want to reconsider the OCaml versions supported in docker-coq, e.g.:
? and at first sight item 1. could be enough for most use cases, WDYT? |
Not yet, it improves performance in general so the impact is a bit less severe. Maybe 4.10.1 will see an improvement? I guess people has had other worries these days as to work on that a lot.... [Hope you folks are fine, myself I'm safely sheltered in the US very far from home which is not the worst case but it sucks as I'm out of home and have no idea when I'll be back] I'd say 2 should be the logical choice once Coq 8.11.1 is released. |
thanks @ejgallego. Take care. |
Good news, the docker-coq-action https://github.com/erikmd/docker-coq-action now works :) see this GitHub action build on a realistic small example installing
and the overall timing is 2'23" (which should be further reduced by using a one-switch Docker image) |
@erikmd The GitHub Action is a Docker Action providing an image with @JasonGross is there really a use case for building Coq projects under Windows and macOS? |
Fiat-Crypto had a bug in its build system (in particular, how we were dealing with line endings in |
These two cases look like edge cases to me in the sense that most projects should not roll their own build systems. This is already true today with |
The issues are that:
If all of these issues are fixed, then I believe we'll be able to drop most of the custom logic in fiat-crypto's Makefile |
Dune supports output tests pretty well though.
This seems like a bug. Has it been reported?
Dune should eventually solve this. Cf. ocaml/dune#2178. |
Including ignoring/accounting for differences that result from different handling of line endings on Windows vs Linux?
coq/coq#8649 and coq/coq#9148 are related but slightly distinct bug reports about this issue |
That's a good question. If that's not the case that certainly something that Dune developers would be interested to hear about given that they are committed to support Windows well. |
We've tried this quite a while ago, not so successful: https://github.com/coq-community/manifesto/wiki/To-Do#ci-explore-github-actions |
can you be more specific? |
You're right that hard-coding The overhead just amounts to downloading the
Actually the solution proposed in the docker-coq-action repo looks very promising, as it allows to:
|
Your solution: |
For comparison, CircleCI uses 1 min 37 sec. I'm happy to migrate to GitHub Actions if it matches CircleCI's convenience in step-level profiling and customization, which seems unavailable in current setup. |
Thanks @liyishuai ! |
Hi @liyishuai
it seems a pretty feature indeed; at first sight it is not directly provided by GitHub actions but I'll try to come up with a solution. stay tuned |
This link isn't enough for me to understand what feature is being pointed at. @liyishuai or @erikmd or someone else, can you explain? |
|
actually this can easily be emulated by defining GitHub-actions variables, then inserting them in your script by writing e.g.
and this one can be implemented by inserting at the beginning (and everywhere else) in your script a call of the bash command timediff() {
newtime=$(TZ=UTC+0 printf "%(%s)T\n" '-1')
if [ -n "$oldtime" ]; then TZ=UTC+0 printf "\u21b3%(%-Mm %-Ss)T\n" "$((newtime - oldtime))"; fi
oldtime=$newtime
} (inspired by this SO answer: https://stackoverflow.com/a/27442175/9164010) |
not exactly: GitHub actions does measure some timings, but not with the granularity you'd like |
CircleCI has a similar issue, but was solved by configuring the Bash environment upon startup to share with future steps. |
@JasonGross cf. https://dune.readthedocs.io/en/stable/concepts.html#diffing-and-promotion It says indeed that:
|
OK but just to clarify, what I meant in my comment was not just a matter of environment variables (as this point could be workarounded by using the This does not looks like an issue to me: the architecture of all the CI providers mentioned here is very different, but if we compare for example the current docker-coq-action user syntax w.r.t. that of the Travis CI template, the overall syntax of the docker action is much more convenient to use and customize (and also leads to a better timing w.r.t. Travis CI). But feel free to ask if you'd like we incorporate to the |
Indeed, that the different steps are run in different containers makes the "native" step control different from other platforms. I recall Travis CI used |
I have made a mostly-satisfactory problem matcher for Coq; it creates annotations like this (the duplication is due to it triggering in multiple jobs): The current version is {
"problemMatcher": [
{
"owner": "coq",
"pattern": [
{
"regexp": "^File \"([^ \"]+)\", line (\\d+), characters (\\d+-\\d+):",
"file": 1,
"line": 2,
"column": 3
},
{
"regexp": "^(Warning|Error): (.*)$",
"severity": 1,
"message": 2
}
]
}
]
} But I'm working on improving it Edit: Here's a slightly better matcher that also includes warning/error categories: {
"problemMatcher": [
{
"owner": "coq",
"pattern": [
{
"regexp": "^File \"([^ \"]+)\", line (\\d+), characters (\\d+-\\d+):",
"file": 1,
"line": 2,
"column": 3
},
{
"regexp": "^(Warning|Error): (.*?)(?:\\s*\\[(.*)\\])?$",
"severity": 1,
"message": 2,
"code": 3
}
]
}
]
} |
Yes: an equivalent to (although it is not documented in the main reference manual https://help.github.com/en/actions/reference/workflow-commands-for-github-actions) FYI I successfully implemented a |
@JasonGross that's very cool but please let's not parse human message errors; does the matching system support JSON for example? At the very least you should properly set the terminal width if you plan to use that. |
Btw, there's some documentation on problem-matchers here. It looks like the way you add a matcher is to copy the .json file to a path accessible from inside the docker image, and then run |
@ejgallego The matching system is very simplistic, and only supports regular expressions, as far as I can tell. But, indeed, having error messages not wrap would be quite nice. Is that a solution to coq/coq#11953 ? |
@ejgallego OTOH, though, if you emit the entire error message in one line in json, it's probably pretty easy to do dumb parsing of that with regular expressions (though we'll mess up quotation characters, if those appear, unfortunately |
@JasonGross indeed let me take care of that bug; in most of my own OCaml projects I always setup auto-configuration of terminal / width printing. |
Just FYI, the docker-coq-action is ready, its migration to coq-community is pending and I hope to release it by next Monday 27 April. I also Cc @clarus to let you know (sorry Guillaume, I had forgotten to @-mention you in my first post) BTW @JasonGross @ejgallego what is the status of the problem-matchers feature you mentioned in your comments?
would one of you like to open a PR in https://github.com/erikmd/docker-coq-action to configure github-action's problem-matchers for Coq? do you want me to do so? |
Problem matcher is working pretty well! I'd prefer if you make the PR, though I can also do it. |
It's not possible to use docker actions in conjunction with other actions (e.g., to install Haskell and upload artifacts), is it? |
OK thanks! I can have a look by Friday.
Good question, rather than replying "yes and no" 😃 let me just recap the underlying architecture:
|
FYI I updated the docker-coq wiki accordingly and submitted a PR (#26) in coq-community templates. |
Hi @liyishuai, BTW these new images are now documented in the README of the Docker Hub repo. |
I open this meta issue to keep track of the following three on-going, interrelated changes for the infrastructure of docker-coq / docker-mathcomp:
coqorg/coq
images with only one switch (4.05.0
,4.07.1+flambda
and4.09.0+flambda
) per image.The motivation of this change originated from the discussion in the issue Upgrade OCaml docker-base#4 created by @liyishuai
coqorg/coq
from Docker Hub to (GitHub +) GitLab CI.The motivation of this change is scalability: Docker Hub's single worker (1-CPU) wouldn't scale to build an increasing number of images at once.
Note that
coqorg/base
could stay a Docker Hub automated build though.I've created that repo to this aim: https://github.com/erikmd/docker-coq-action (but more tests are required before we undertake to move this repo in coq-community, for example).
I also Cc @ejgallego @palmskog @anton-trunov @SkySkimmer @CohenCyril @ybertot @proux01 @JasonGross FYI
The attached PDF (version 20200326.1), summarizes the current specification of
coqorg/coq
,mathcomp/mathcomp
andmathcomp/mathcomp-dev
images, and the envisioned specification after the on-going migration:recap-migration-docker-coq_20200326.1.pdf
The text was updated successfully, but these errors were encountered: