[CI] job testing coq-native

[gares]

Fix #1498

[gares]

@chdoc I'm trying to add a job here that warns (not fail) if a package is found to fail when coq-native is installed.
In order to test it I made a silly copy of your last package about graphs, thinking that it would fail, but it does not.
Can you remind me which package of yours break with coq-native?

[chdoc]

@gares. Yes, you got the right package and for me it is still failing as of 5 minutes ago: https://github.com/coq-community/graph-theory/runs/1531187774

[gares]

I think I found the problem. It's OCaml 4.05 + native. If you use an image based on ocaml 4.07 it works (even with native)

[chdoc]

Great! Thanks for the info! So the the world of coq-native now makes peoples "pure .v" developments sensitive to the underlying Version of OCaml. IIRC, this is precisely the thing that you said should not be the case and I tend to agree. 😞

[gares]

It may also be related to the (default) stack size on docker... we are still investigating.

[gares]

@ejgallego @erikmd I'm running out of ideas here. I'm trying to reproduce the failures that some users experienced using docker when the default image was including coq-native. I've added jobs to test things on 4.05, 4.07, 4.07+flambda, 4.09 and 4.09+flambda but I still have to see a single failure (even on gitlab's runners). I suppose I'm doing something wrong. It may be the configuration I'm testing (hence you in CC) or something else I miss.

I had plans to have coqbot suggest a message: [ "warning...blabla" { coq-native:installed & ocaml:version = xxx } ] opam stanza on failures, but I can't even get one :-/

[erikmd]

Hi @gares, thanks for your message and for your experiments.

I don't have many clues, but at least, I'm able to reproduce the issue in GitHub Actions with the following workflow:

  test:
    # the OS must be GNU/Linux to be able to use the docker-coq-action
    runs-on: ubuntu-latest
    strategy:
      matrix:
        image:
          - 'coqorg/coq:dev-native-ocaml-4.07'
      fail-fast: false
    steps:
      - uses: actions/checkout@v2
        with:
          repository: 'coq-community/graph-theory'
          ref: 'ec5f2f3e37ed4485108796f6a35037ce1c6e270f'
      - run: ls -Rhal
      - uses: coq-community/docker-coq-action@v1
        with:
          opam_file: 'coq-graph-theory.opam'
          custom_image: ${{ matrix.image }}

so, using coq.dev and ocaml 4.07 (without flambda) + coq-native

See the corresponding log:
https://github.com/erikmd/docker-coq-github-action-demo/runs/1550502552?check_suite_focus=true

I don't know if this is due to the stack size as ulimit -a indicates it is also 8192 kB:
https://github.com/erikmd/docker-coq-github-action-demo/runs/1550502505?check_suite_focus=true

So to figure out which parameter could trigger this failure, I guess the next step would be to try to reproduce that build locally (outside of GitHub Actions). I'll try this tonight and let you know…

[gares]

The stack (outside docker) is 8K and the memory is 7 GB, which is better than what gitlab gives us.
I guess you should run ulimit and free -m inside the docker container, just in case some silly setup trims them down.

[erikmd]

OK, so FYI @gares, the issue is reproducible locally.
Upside: this is not a GitHub Actions specific issue, so it is easier to debug.
Downside: this needs to be debugged.

...
- COQC theories/open_confluence.v
- Fatal error: exception Stack overflow
- Error: Native compiler exited with status 2
- 
- make[2]: *** [Makefile.coq:720: theories/reduction.vo] Error 1
- make[2]: *** Waiting for unfinished jobs....
- File "./theories/open_confluence.v", line 1580, characters 0-71:
- Warning: The default value for hint locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding hints outside of sections without
- specifying an explicit locality is therefore deprecated. It is recommended to
- use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
- File "./theories/open_confluence.v", line 1581, characters 0-70:
- Warning: The default value for hint locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding hints outside of sections without
- specifying an explicit locality is therefore deprecated. It is recommended to
- use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
- File "./theories/open_confluence.v", line 1582, characters 0-32:
- Warning: The default value for hint locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding hints outside of sections without
- specifying an explicit locality is therefore deprecated. It is recommended to
- use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
- make[1]: *** [Makefile.coq:343: all] Error 2
- make[1]: Leaving directory '/home/coq/.opam/4.07.1/.opam-switch/build/coq-graph-theory.dev'
- make: *** [Makefile:2: all] Error 2
[ERROR] The compilation of coq-graph-theory failed at "/usr/bin/make -j2".

#=== ERROR while compiling coq-graph-theory.dev ===============================#
# context     2.0.7 | linux/x86_64 | ocaml-base-compiler.4.07.1 | pinned(file:///home/coq/graph-theory)
# path        ~/.opam/4.07.1/.opam-switch/build/coq-graph-theory.dev
# command     /usr/bin/make -j2
# exit-code   2
# env-file    ~/.opam/log/coq-graph-theory-16800-05296d.env
# output-file ~/.opam/log/coq-graph-theory-16800-05296d.out
### output ###
# [...]
# release. For the time being, adding hints outside of sections without
# specifying an explicit locality is therefore deprecated. It is recommended to
# use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
# File "./theories/open_confluence.v", line 1582, characters 0-32:
# Warning: The default value for hint locality is currently "local" in a
# section and "global" otherwise, but is scheduled to change in a future
# release. For the time being, adding hints outside of sections without
# specifying an explicit locality is therefore deprecated. It is recommended to
# use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
# make[1]: *** [Makefile.coq:343: all] Error 2
# make[1]: Leaving directory '/home/coq/.opam/4.07.1/.opam-switch/build/coq-graph-theory.dev'
# make: *** [Makefile:2: all] Error 2



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-graph-theory dev
+- 
- No changes have been performed
'opam install -y -v -j 2 coq-graph-theory' failed.

[erikmd]

BTW @gares you might want to edit your initial post to add something like this?
Close https://github.com/coq/opam-coq-archive/issues/1498 or Close #1498

[chdoc]

Given that the error you managed to reproduce comes from our library, feel free to contact me if you think I can help. Admittedly, this is a somewhat ad-hoc corner of the library. 🤷‍♂️

[gares]

@erikmd done thanks.

I did some googling and you can pass to docker ulimit and ram caps on the command line, and I see none of these your entrypoint.sh. Maybe the defaults are just wrong?

[proux01]

@chdoc I had a look to graph-theory and indeed it doesn't compile with coq-native and the usual 8 mB stack but increasing it to 10 mB seems to be enough (at least with OCaml 4.05, this might be more with other versions).

So

ulimit -s 16384

within the docker image, before calling opam/make/... should suffice.