Circle CI #6400
Circle CI #6400
Conversation
Revert "CI: poc Circleci configuration" Committed on master by mistake. Clearly I'm too clumsy to be trusted with push rights. This reverts commit d606a85. CI: poc Circleci configuration Fixup Try minimising build for faster testing Various fixes Fixup: yaml identation Do not -j2: native compiler seems to take too much memory Revert "Do not -j2: native compiler seems to take too much memory" This reverts commit 4886151. Deactivate native compiler Fixup (how did this happen?) Do not call time (not install on docker images, will fix later) Fixup Fixup
VS gitlab: + fiat-crypto (Circle has 4GB RAM, gitlab 2GB) - caching opam (TODO) - publishing artefacts (TODO) * tests with -local, not installed VS travis: + reusing build products - flambda validate job (TODO?) - OSX jobs (TODO at least check if free OSX is possible) - linter (TODO?)
|
That's cool, thank you @SkySkimmer for doing this. The output looks better than on Travis. It is a shame that we have to log in to see it though. We should do more than just share the build of Coq. The builds of Bignums, Corn, Math-Classes and SSReflect should also be shared (although in the case of SSReflect I wonder what is the dependency today, given that the plugin was merged into Coq). For MacOS testing, CircleCI proposes the seed plan free for OSS project (provided we write to them) but it is limited to 500 max minutes/month. So that wouldn't fit with testing every PRs. That's too bad because I'm not happy with Travis for MacOS testing. Finally, using CircleCI for testing external developments is supposed to help reduce the CI backlog but I don't quite get why you want to test the 32-bits target or the OCaml 4.06 target over there as well. |
But it will require rewriting part of the CI logic, e.g. by moving the dependency declaration from the build script to |
Because it's a port of the gitlab stuff, everything that was on gitlab came with. |
|
@SkySkimmer Looks wonderful, thanks! Do you think you'd need to address the remaining TODOs, or we could start using that right away, and remove some of these jobs from Travis? |
| COQIDE_PACKAGES: &coqide-packages "libgtk2.0-dev libgtksourceview2.0-dev" | ||
| #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386" | ||
| COQIDE_OPAM: &coqide-opam "lablgtk-extras" | ||
| COQIDE_OPAM_BE: &coqide-opam-be "num lablgtk.2.18.6 lablgtk-extras.1.6" |
There was a problem hiding this comment.
In travis we also bound the range of lablgtk to {min..max} supported versions. You may not want to do that here thou.
.circleci/config.yml
Outdated
| opam switch ${COMPILER} | ||
| eval $(opam config env) | ||
| opam config list | ||
| opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM} |
.circleci/config.yml
Outdated
| source ~/.profile | ||
|
|
||
| echo 'start:coq.config' | ||
| ./configure -local -native-compiler no ${EXTRA_CONF} |
There was a problem hiding this comment.
We need to enable the native-compiler by default, it is a very important component for testing.
|
@maximedenes Even if we merged this right now, it would probably be better to wait a few days / weeks to see if we are happy with it before removing the corresponding jobs in Travis. @SkySkimmer How complex do you think it would be to also support sharing of the build of package dependencies, such as Bignums? Do you agree this would require stating dependencies in Makefile? |
I don't think it would be too hard. I don't think we need to put the dependencies in the makefile, although it may be cleaner than keeping them in the scripts. Mostly we just need the script for Currently with dependencies in scripts it should go like I don't know how easily we can tell whether something is installed, it may need to be done custom per development. Or maybe have dummy files CI_TARGETS = ...
.PHONY: $(CI_TARGETS)
$(CI_TARGETS): ci-%: _build_ci/.ci-%.done $(DEPS_%)
_build_ci/.ci-%.done:
dev/ci/ci-%.sh) |
|
I like the |
071886d to
4d11d6d
Compare
|
I seem to only have 3 parallel jobs now. I think the 4th was the free trial. |
|
What to do about install_ssreflect? Make those jobs depend on full mathcomp or have a small ci-ssreflect.sh? |
|
Now I have 4 jobs again. Maybe they had a bug. |
|
Now with longer dependency chain https://circleci.com/workflow-run/4348c189-7999-47ba-93d5-f14886566f8b |
|
I think that while the The current "system" [to call it something] is however intended to work in a different way. If you already have This also has problems. |
5e47be7 to
f83e437
Compare
test-suite/Makefile
Outdated
| @@ -176,7 +176,7 @@ summary.log: | |||
| # local build, and downloadable on GitLab) | |||
| report: summary.log | |||
| $(HIDE)bash save-logs.sh | |||
| $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi | |||
| $(HIDE)if [ "(" -n "${TRAVIS}" ")" -o "(" -n "${CIRCLECI}" ")" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi | |||
There was a problem hiding this comment.
I think you want to add this to the APPVEYOR one, or make a separate CIRCLECI one, unless CIRCLECI also uses travis_fold: (which I'm suspicious of).
There was a problem hiding this comment.
Right, I forgot the reason they're separate.
f83e437 to
81e0ef5
Compare
8aafb03 to
1053f88
Compare
1053f88 to
653df5a
Compare
|
I tried adding a badge, currently it shows as failing, let's wait for the latest build to finish. |
|
I'm not fond of the bullet points for the badges. Everything on the same line would look better and is more usual. |
|
Improving the CI situation is a priority, so I'll merge this and activate Circle CI. Refining which jobs stay on Travis will be done in a second step. |
|
I'm kind of wondering how this got merged without any testing on Travis, while it was clearly likely to affect Travis. Also, when I said "remove the badge", did you understand that my main reason for asking this was that the badge points to @SkySkimmer's fork? I guess you didn't and I should have made myself clearer, but this was difficult to shout over the room while a talk was starting. |
|
The new badges look very ugly and out of alignment |
Yep, I didn't realize, sorry about that.
Oh! Indeed I thought you meant just a cosmetic thing because you had written:
Anyway, let's quickly solve these problems and the CI situation should improve. |
I squashed all the @aspiwack commits into one then added mine separately.
Since we only get 4 jobs on circle we probably want to keep some stuff on travis.
Example run here https://circleci.com/workflow-run/f41442ca-c172-4067-8511-623ded2c768b (needs login, reload the link after login if it redirects to 404) (commits got squashed without change since that)
See #6347.