[CI] job testing coq-native #1504

gares · 2020-12-10T11:16:11Z

gares · 2020-12-10T13:32:35Z

@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 · 2020-12-10T14:45:12Z

@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 · 2020-12-10T15:00:51Z

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 · 2020-12-10T15:08:47Z

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 · 2020-12-10T15:10:51Z

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

gares · 2020-12-14T12:18:32Z

@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 · 2020-12-14T13:55:46Z

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 · 2020-12-14T15:27:34Z

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 · 2020-12-15T01:09:04Z

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 · 2020-12-15T01:11:01Z

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 · 2020-12-15T09:40:02Z

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 · 2020-12-15T10:48:33Z

@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 · 2021-06-03T09:33:46Z

@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.

gares force-pushed the test-coq-native branch from b094f63 to ff29817 Compare December 10, 2020 12:43

gares force-pushed the test-coq-native branch 2 times, most recently from 84a27df to eb5c8c2 Compare December 11, 2020 15:36

gares added 4 commits December 14, 2020 10:47

allowed to fail job testing coq-native

79164cf

improve the script to print installed files

b1caa09

hack to rebuild unimath

0bff4bc

hack recompile fiat parser

a1d8e0c

gares force-pushed the test-coq-native branch from 5dac11f to a1d8e0c Compare December 14, 2020 09:47

erikmd mentioned this pull request Sep 28, 2021

feat: Take advantage of the coq-native package (CEP 048, item 3) #1835

Merged

palmskog mentioned this pull request Nov 8, 2021

[coq.dev] New upstream split package setup. #1923

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[CI] job testing coq-native #1504

[CI] job testing coq-native #1504

gares commented Dec 10, 2020 •

edited

Loading

gares commented Dec 10, 2020 •

edited

Loading

chdoc commented Dec 10, 2020

gares commented Dec 10, 2020

chdoc commented Dec 10, 2020

gares commented Dec 10, 2020 •

edited

Loading

gares commented Dec 14, 2020

erikmd commented Dec 14, 2020 •

edited

Loading

gares commented Dec 14, 2020

erikmd commented Dec 15, 2020

erikmd commented Dec 15, 2020 •

edited

Loading

chdoc commented Dec 15, 2020

gares commented Dec 15, 2020 •

edited

Loading

proux01 commented Jun 3, 2021

[CI] job testing coq-native #1504

Are you sure you want to change the base?

[CI] job testing coq-native #1504

Conversation

gares commented Dec 10, 2020 • edited Loading

gares commented Dec 10, 2020 • edited Loading

chdoc commented Dec 10, 2020

gares commented Dec 10, 2020

chdoc commented Dec 10, 2020

gares commented Dec 10, 2020 • edited Loading

gares commented Dec 14, 2020

erikmd commented Dec 14, 2020 • edited Loading

gares commented Dec 14, 2020

erikmd commented Dec 15, 2020

erikmd commented Dec 15, 2020 • edited Loading

chdoc commented Dec 15, 2020

gares commented Dec 15, 2020 • edited Loading

proux01 commented Jun 3, 2021

gares commented Dec 10, 2020 •

edited

Loading

gares commented Dec 10, 2020 •

edited

Loading

gares commented Dec 10, 2020 •

edited

Loading

erikmd commented Dec 14, 2020 •

edited

Loading

erikmd commented Dec 15, 2020 •

edited

Loading

gares commented Dec 15, 2020 •

edited

Loading