[build] Add support for code coverage by ejgallego · Pull Request #12259 · rocq-prover/rocq

ejgallego · 2020-05-06T11:30:48Z

This PR went into a few iterations due to build system changes; it is in final form now. A couple of notes:

the instrumentation support we use requires Dune 2.7, I don't think this is a problem [2.8 is]
when the instrumentation is not enabled, the whole of it is a no-op

Integration with some coverage tool so we can actually see progress among releases, and extended weekly builds is desired, but not necessary to do here.

ejgallego · 2020-05-06T16:07:03Z

Example artifact: https://coq.gitlab.io/-/coq/-/jobs/541070076/artifacts/_build/coq-coverage/index.html

SkySkimmer · 2020-05-06T16:58:10Z

What's the perf impact of running the coverage? Is it small enough to activate it for the 3rd party jobs (fiat-crypto etc)?

ejgallego · 2020-05-06T17:04:49Z

What's the perf impact of running the coverage? Is it small enough to activate it for the 3rd party jobs (fiat-crypto etc)?

I think it is around 2x / 3x time.

ejgallego · 2020-05-07T09:58:16Z

@SkySkimmer certainly at every commit this could be too much, but we could run a weekly deeper coverage testing run indeed.

aantron · 2020-05-11T06:21:31Z

I think it is around 2x / 3x time.

Is this based on a measurement? I would not have expected the impact to be such, though I suppose it's plausible for very CPU-bound work.

JasonGross · 2020-05-11T10:41:20Z

I'd be quite interested in seeing the code coverage diff between, say, all of the current CI vs all of the current CI + fiat-crypto-legacy (which I've been maintaining compatible with master for, even though it's been removed from the CI). If there's any diff, we might be able to extract some useful new test-cases.

aantron · 2020-05-11T12:37:37Z

We would probably need to restore the old "combine expressions" for this (arithmetic/diffs on coverage output). If there is indeed interest in this, I can add them to Bisect_ppx.

ejgallego · 2020-05-11T12:58:45Z

Is this based on a measurement? I would not have expected the impact to be such, though I suppose it's plausible for very CPU-bound work.

@aantron it is based on CI timings, bisect job: 73 mins, regular job ~ 40 mins.

@JasonGross hopefully we do indeed start doing stuff like that once the setup is more stable.

aantron · 2020-05-11T13:15:23Z

it is based on CI timings, bisect job: 73 mins, regular job ~ 40 mins.

Ok. Just want to note: that difference would not be only from the instrumentation inserted into the code, but also due to the time taken to generate the report at the end.

ejgallego · 2020-05-11T13:20:35Z

Ok. Just want to note: that difference would not be only from the instrumentation inserted into the code, but also due to the time taken to generate the report at the end.

Indeed; I was maybe a bit pessimistic but also note that in the above job OCaml compilation time itself is a significant part so the current numbers are around a bit more than 2x ; Coq is likely worst case in this sense as some instrumented code paths are called dozens of millions of times as they are in critical loops [such as conversion]

Would we tweak the instrumentation to leave out these hot paths, I'd bet the slowdown would be much less severe.

jfehrle · 2020-07-15T16:19:44Z

@ejgallego The example artifact is long gone. Perhaps you could rerun the build for the PR so I can look at the output? I'd like to see how usable the output is for parser statistics as you suggested on the Coq call. I expect the 2x-3x overhead to run code coverage is far more expensive than generating the parser statistics in my PR, which should have a negligible effect on run time.

ejgallego · 2023-06-27T13:10:40Z

Rebased in case someone wants to have a look.

aantron · 2023-06-27T15:07:02Z

Does this need help from Bisect upstream?

ejgallego · 2023-06-28T11:31:32Z

Does this need help from Bisect upstream?

Thanks a lot @aantron , for now we are stuck on the coverage data upload (some problems with tokens in our CI setup)

We are having a look, will let you know if we have feedback for upstream (maybe documenting our setup could be useful for others, so we may do a doc PR)

coqbot-app · 2023-07-31T02:17:34Z

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

coqbot-app · 2023-08-30T02:08:29Z

This PR was not rebased after 30 days despite the warning, it is now closed.

ejgallego · 2024-03-19T18:18:29Z

Reopened after the discussion in today's call, maybe we can debug / discuss what's missing here on Zulip?

JasonGross · 2024-03-19T23:46:46Z

+    - chmod +x codecov
+    - ./codecov -t ${CODECOV_TOKEN} -f coverage.json
+    # Bah bisect-ppx doesn't support gitlab CI
+    # - bisect-ppx-report send-to --source-path=_build/coverage --coverage-path=_build/coverage Codecov


Should this be uncommented to test?

I think the line just above ./codecov .... should do the same trick, but I forgot about how the process looks like.

Maybe we should check if the bisect-ppx-report has support for gitlab CI already in the newer version.

It looks like not https://github.com/aantron/bisect_ppx/blob/e30265643e77bcf2c9eba7322429c779122106fc/src/report/coveralls.ml#L148-L152

But it also shouldn't be too hard to add, it's just a matter of figuring out what variables live where. Or you can spoof it by setting variables appropriately

@aantron is there any obstacle to supporting gitlab upstream?

I've made aantron/bisect_ppx#436

What about doing

Suggested change

# - bisect-ppx-report send-to --source-path=_build/coverage --coverage-path=_build/coverage Codecov

- bisect-ppx-report send-to --source-path=_build/coverage --coverage-path=_build/coverage Codecov --git --service-name="github" --service-pull-request="${CI_COMMIT_BRANCH#pr-}" --service-job-id="$CI_JOB_ID"

- bisect-ppx-report send-to --source-path=_build/coverage --coverage-path=_build/coverage Coveralls --git --service-name="github" --service-pull-request="${CI_COMMIT_BRANCH#pr-}" --service-job-id="$CI_JOB_ID"

?

ejgallego · 2024-03-20T07:43:31Z

Hi folks, a few points:

this needs a new assignee, I think @maximedenes won't have time to handle this PR (I understand, feel free to correct me if I'm wrong.
I wonder if we should merge this without uploading the coverage data to some service, just generating the artifact with the report and leaving the upload to future work. Unfortunately, that doesn't allow us to check what the delta between coverage, which is the most important.
The real nice coverage data would be data that is generated for all of the CI, I wonder how to handle this. In my computer I was able to do using the ci-all make target. We could have a weekly run that does that (or combines the coverage artifacts from all jobs)

Unfortunately I have limited time to work on this in the upcoming weeks, but I'm happy to do my best to help if someone would like to try.

SkySkimmer · 2024-03-20T10:53:57Z

I wonder if we should merge this without uploading the coverage data to some service, just generating the artifact with the report and leaving the upload to future work.

I think we should, it would at least reduce rebase pain when working on the rest.

ejgallego · 2024-03-20T13:51:49Z

@SkySkimmer I'll prepare a non-draft version ASAP.

JasonGross · 2024-03-20T20:32:40Z

I see:
This job is stuck because of one of the following problems. There are no active runners online, no runners for the protected branch , or no runners that match all of the job's tags: docker

SkySkimmer · 2024-03-21T14:02:21Z

This job is stuck because of one of the following problems. There are no active runners online, no runners for the protected branch , or no runners that match all of the job's tags: docker

Yes we need to enable the inria custom runners for docker-boot, it's a pain.
(we don't keep them enabled because they're unreliable)

SkySkimmer · 2024-03-21T14:03:55Z

in fact they're currently down

ejgallego · 2024-03-21T14:24:02Z

Something I was thinking was about running coverage on Github actions, however that doesn't scale in the case we'd eventually like to run the coverage for the full CI.

Another option is actually to run the full CI "offline", in one of our servers, and them push the reports to a static website.

JasonGross · 2024-03-21T18:17:39Z

Something I was thinking was about running coverage on Github actions, however that doesn't scale in the case we'd eventually like to run the coverage for the full CI.

What is the issue? Presumably running coverage on the full CI could happen, say, on a schedule (once a week?) and when requested (like the bench), and there'd be no problem with using GitHub Actions then (other than having to duplicate everything in .gitlab.yml, which is maybe the lack of scaling you're talking about?)

SkySkimmer · 2024-04-17T13:25:12Z

We now use the gitlab.inria.fr shared runners for docker-boot so if you rebase we may be able to get this merged

ejgallego · 2024-04-26T13:32:45Z

Ok rebased, still not sure how to run the CI tho.

ejgallego · 2024-04-26T13:33:26Z


 let decimal =
-  let ( || ) = parser_or in
+  let ( ||| ) = parser_or in


Bisect got confused with this overloading, I guess we should see if that's the case and submit a bug there (and remove this change)

JasonGross · 2024-04-28T15:00:45Z

@coqbot run light ci

JasonGross · 2024-04-30T05:30:41Z

$ opam switch set -y "${COMPILER}${OPAM_VARIANT}"
[ERROR] No switch 4.09.0+flambda is currently installed. Did you mean 'opam switch create 4.09.0+flambda'?
        Installed switches are:
          - 4.09.0+32bit
          - 4.09.0

@ejgallego Do you need some extra setup somewhere?

ejgallego · 2024-05-06T16:18:19Z

This failed due to the complexity tests...

I cannot wait for the day these tests are removed from Coq, they only get in the way (pretty often in my case)

coqbot-app · 2024-06-06T02:15:41Z

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

Closes rocq-prover#10267

coqbot-app · 2024-08-05T02:18:46Z

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

coqbot-app · 2024-09-04T02:21:56Z

This PR was not rebased after 30 days despite the warning, it is now closed.

aantron · 2024-09-04T06:58:46Z

Is this something the Coq project wants? What is necessary from the Bisect side? aantron/bisect_ppx#436?

ejgallego added kind: infrastructure CI, build tools, development tools. part: build The build system. needs: independent fix The PR reveals an independent bug. needs: progress Work in progress: awaiting action from the author. labels May 6, 2020

ejgallego force-pushed the dune+bisect branch 9 times, most recently from 53d4f3f to a1a58fa Compare May 6, 2020 13:24

ejgallego mentioned this pull request May 6, 2020

Type error with partial application and optional argument aantron/bisect_ppx#319

Closed

ejgallego force-pushed the dune+bisect branch from a1a58fa to bf16371 Compare May 6, 2020 14:53

ejgallego force-pushed the dune+bisect branch from bf16371 to 877b369 Compare May 10, 2020 19:45

ejgallego force-pushed the dune+bisect branch from 877b369 to 5edacd6 Compare May 14, 2020 22:06

jfehrle mentioned this pull request Jul 15, 2020

Generate parsing statistics #10652

Closed

Zimmi48 added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jul 16, 2020

JasonGross reviewed Mar 19, 2024

View reviewed changes

ejgallego commented Apr 26, 2024

View reviewed changes

JasonGross reviewed Apr 27, 2024

View reviewed changes

Comment thread .gitlab-ci.yml

This comment was marked as outdated.

Sign in to view

SkySkimmer reviewed Apr 30, 2024

View reviewed changes

Comment thread .gitlab-ci.yml

ejgallego added 2 commits June 6, 2024 13:23

[build] Add support for code coverage

4c31e59

Closes rocq-prover#10267

[wip] Fixup to bisect report upload

3a81966

	# - bisect-ppx-report send-to --source-path=_build/coverage --coverage-path=_build/coverage Codecov
	- bisect-ppx-report send-to --source-path=_build/coverage --coverage-path=_build/coverage Codecov --git --service-name="github" --service-pull-request="${CI_COMMIT_BRANCH#pr-}" --service-job-id="$CI_JOB_ID"
	- bisect-ppx-report send-to --source-path=_build/coverage --coverage-path=_build/coverage Coveralls --git --service-name="github" --service-pull-request="${CI_COMMIT_BRANCH#pr-}" --service-job-id="$CI_JOB_ID"

Uh oh!

Conversation

ejgallego commented May 6, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ejgallego commented May 6, 2020

Uh oh!

SkySkimmer commented May 6, 2020

Uh oh!

ejgallego commented May 6, 2020

Uh oh!

ejgallego commented May 7, 2020

Uh oh!

aantron commented May 11, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JasonGross commented May 11, 2020

Uh oh!

aantron commented May 11, 2020

Uh oh!

ejgallego commented May 11, 2020

Uh oh!

aantron commented May 11, 2020

Uh oh!

ejgallego commented May 11, 2020

Uh oh!

jfehrle commented Jul 15, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ejgallego commented Jun 27, 2023

Uh oh!

aantron commented Jun 27, 2023

Uh oh!

ejgallego commented Jun 28, 2023

Uh oh!

coqbot-app Bot commented Jul 31, 2023

Uh oh!

coqbot-app Bot commented Aug 30, 2023

Uh oh!

ejgallego commented Mar 19, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JasonGross Mar 19, 2024

Choose a reason for hiding this comment

Uh oh!

ejgallego Mar 20, 2024

Choose a reason for hiding this comment

Uh oh!

JasonGross Mar 20, 2024

Choose a reason for hiding this comment

Uh oh!

JasonGross Mar 20, 2024

Choose a reason for hiding this comment

Uh oh!

JasonGross Mar 20, 2024

Choose a reason for hiding this comment

Uh oh!

JasonGross Mar 20, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ejgallego commented Mar 20, 2024

Uh oh!

SkySkimmer commented Mar 20, 2024

Uh oh!

ejgallego commented Mar 20, 2024

Uh oh!

JasonGross commented Mar 20, 2024

Uh oh!

SkySkimmer commented Mar 21, 2024

Uh oh!

SkySkimmer commented Mar 21, 2024

Uh oh!

ejgallego commented Mar 21, 2024

Uh oh!

JasonGross commented Mar 21, 2024

Uh oh!

SkySkimmer commented Apr 17, 2024

Uh oh!

ejgallego commented Apr 26, 2024

ejgallego commented May 6, 2020 •

edited

Loading

aantron commented May 11, 2020 •

edited

Loading

jfehrle commented Jul 15, 2020 •

edited

Loading

ejgallego commented Mar 19, 2024 •

edited

Loading

JasonGross Mar 20, 2024 •

edited

Loading