Port CI from Travis to GH Actions #237

JasonGross · 2021-04-15T18:25:01Z

@ejgallego How important is it that it's libgmp-dev:i386 rather than libgmp-dev? The former doesn't seem to exist on the GH Actions runners.

Currently still working on getting this building, but I figured I'd submit it as a draft since I don't have much more time to work on it, and I think it's nearly ready.

JasonGross · 2021-04-15T18:54:51Z

Oh, nevermind, I forgot to call eval $(opam env)

JasonGross · 2021-04-15T19:17:14Z

I think fixing the action is beyond the scope of my expertise, the 4.07.1+32bit, js-dune build is failing with

Error:  The compilation of zarith failed at "/home/runner/.opam/opam-init/hooks/sandbox.sh build make".
#=== ERROR while compiling zarith.1.12 ========================================#
# context              2.0.8 | linux/x86_64 | ocaml-variants.4.07.1+32bit | git+https://github.com/ocaml/opam-repository.git
# path                 ~/.opam/4.07.1+32bit/.opam-switch/build/zarith.1.12
# command              ~/.opam/opam-init/hooks/sandbox.sh build make
# exit-code            2
# env-file             ~/.opam/log/zarith-32854-65c165.env
# output-file          ~/.opam/log/zarith-32854-65c165.out
### output ###
# [...]
# ocamlc -I +compiler-libs -bin-annot  -c z.ml
# ocamlc -I +compiler-libs -bin-annot  -c q.mli
# ocamlc -I +compiler-libs -bin-annot  -c q.ml
# ocamlc -I +compiler-libs -bin-annot  -c big_int_Z.mli
# ocamlc -I +compiler-libs -bin-annot  -c big_int_Z.ml
# ocamlmklib -failsafe -o zarith zarith_version.cmo z.cmo q.cmo big_int_Z.cmo -lgmp
# ocamlc -ccopt "-I/home/runner/.opam/4.07.1+32bit/lib/ocaml  -DZ_OCAML_LEGACY_CUSTOM_OPERATIONS -DHAS_GMP  -O3 -Wall -Wextra " -c caml_z.c
# caml_z.c:32:10: fatal error: gmp.h: No such file or directory
#    32 | #include <gmp.h>
#       |          ^~~~~~~
# compilation terminated.
# make: *** [project.mak:141: caml_z.o] Error 2

ejgallego · 2021-04-15T21:43:59Z

Thanks a lot @JasonGross , this is super useful!

Indeed the 32-bit version of gmp is needed for the js_of_ocaml build [as JS cannot efficiently represent 64 bit ints] , but actually it is very likely that the only thing the runners need is sudo dpkg --add-architecture i386 && sudo apt update

JasonGross · 2021-04-15T23:12:23Z

Glad to help! Indeed, I eventually stumbled on that and things now build: https://github.com/JasonGross/coq-serapi/actions/runs/753193729

Let me squash the commits.

Btw, do you have a preference between doing eval $(opam env) before each step (environment variables don't persist across them) vs doing opam env | sed "s/'//g; s/; export .*//g" >> $GITHUB_ENV right after installing opam? (cf ocaml/setup-ocaml#70 (comment))

JasonGross · 2021-04-15T23:14:44Z

Should be ready for merge now

ejgallego · 2021-04-17T16:48:50Z

Should be ready for merge now

Thanks a lot @JasonGross ; I'm gonna do a review but feel free to merge yourself!

One question tho: shouldn't the CI display the checks in this PR? Is there something else we need to activate?

ejgallego · 2021-04-17T16:50:10Z

.github/workflows/ci.yml

+    - v8.10
+    - v8.11
+    - v8.12
+    - v8.13


Actually this was added to the travis file to avoid double-building of pull requests that live in this particular repos, not sure this is still a problem with github actions.

I think in fact PRs would get double-built, but I'm also not sure that's such a problem? What's the bad thing that happens if they get double-built?

Nothing bad, just a waste of runners (for Travis these were quite limited), so keeping the branch then sounds good.

ejgallego · 2021-04-17T16:52:59Z

.github/workflows/ci.yml

+          extra-opam: coq.8.13.0 js_of_ocaml js_of_ocaml-lwt zarith_stubs_js
+        - ocaml-version: 4.11.1
+          test-target: test
+          extra-opam: dune


Shouldn't this be captured by the opam install --deps-only below?

Idk, I was just copying the Travis script

Ok, I'll revisit once the checks actually run.

ejgallego · 2021-04-17T16:55:30Z

.github/workflows/ci.yml

+          pushd math-comp/mathcomp/ssreflect
+          make
+          make install
+          popd


Note: this will likely stop working soon if math-comp is updated to use hiearchy-builder, as it will then require a huge dep chain that is not feasible to manage by hand. So if that happens we will have to either split the math-comp tests, or maybe just use the Coq dev package so we can install everything using opam; when this script was first developed there were some issues with opam, I dunno if things are better now.

JasonGross · 2021-04-17T18:45:14Z

One question tho: shouldn't the CI display the checks in this PR? Is there something else we need to activate?

You need GH actions the base branch (or main branch?) to enable GH actions on PRs to the repo. Seems like a reasonable security principle, though I'm not sure it's necessary. You can check the actions tab on my fork, where I synced this branch to v8.13

JasonGross · 2021-04-17T18:48:22Z

I'm gonna do a review but feel free to merge yourself!

I'm inclined to merge this as-is and let you improve the script in future commits, if that sounds good to you? (I'm a bit short on time to improve it currently.)

ejgallego · 2021-04-17T19:05:47Z

I'm inclined to merge this as-is and let you improve the script in future commits, if that sounds good to you? (I'm a bit short on time to improve it currently.)

Sounds good, thanks a lot @JasonGross this saved me a huge amount of time.

This comment has been minimized.

Sign in to view

JasonGross force-pushed the gh-actions branch from 54d371f to 19a0647 Compare April 15, 2021 19:00

Port CI from Travis to GH Actions

b3246d9

JasonGross force-pushed the gh-actions branch from cdefaf8 to b3246d9 Compare April 15, 2021 23:14

JasonGross marked this pull request as ready for review April 15, 2021 23:14

ejgallego added the kind: infrastructure label Apr 17, 2021

ejgallego added this to the 0.13.1 milestone Apr 17, 2021

ejgallego reviewed Apr 17, 2021

View reviewed changes

JasonGross merged commit c5a609d into rocq-archive:v8.13 Apr 17, 2021

JasonGross deleted the gh-actions branch April 17, 2021 19:23

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Port CI from Travis to GH Actions #237

Port CI from Travis to GH Actions #237

JasonGross commented Apr 15, 2021

This comment has been minimized.

JasonGross commented Apr 15, 2021

JasonGross commented Apr 15, 2021

ejgallego commented Apr 15, 2021 •

edited

Loading

JasonGross commented Apr 15, 2021

JasonGross commented Apr 15, 2021

ejgallego commented Apr 17, 2021

ejgallego Apr 17, 2021

JasonGross Apr 17, 2021

ejgallego Apr 17, 2021

ejgallego Apr 17, 2021

JasonGross Apr 17, 2021

ejgallego Apr 17, 2021 •

edited

Loading

ejgallego Apr 17, 2021

JasonGross commented Apr 17, 2021

JasonGross commented Apr 17, 2021

ejgallego commented Apr 17, 2021

Port CI from Travis to GH Actions #237

Port CI from Travis to GH Actions #237

Conversation

JasonGross commented Apr 15, 2021

This comment has been minimized.

JasonGross commented Apr 15, 2021

JasonGross commented Apr 15, 2021

ejgallego commented Apr 15, 2021 • edited Loading

JasonGross commented Apr 15, 2021

JasonGross commented Apr 15, 2021

ejgallego commented Apr 17, 2021

ejgallego Apr 17, 2021

Choose a reason for hiding this comment

JasonGross Apr 17, 2021

Choose a reason for hiding this comment

ejgallego Apr 17, 2021

Choose a reason for hiding this comment

ejgallego Apr 17, 2021

Choose a reason for hiding this comment

JasonGross Apr 17, 2021

Choose a reason for hiding this comment

ejgallego Apr 17, 2021 • edited Loading

Choose a reason for hiding this comment

ejgallego Apr 17, 2021

Choose a reason for hiding this comment

JasonGross commented Apr 17, 2021

JasonGross commented Apr 17, 2021

ejgallego commented Apr 17, 2021

ejgallego commented Apr 15, 2021 •

edited

Loading

ejgallego Apr 17, 2021 •

edited

Loading