Stream: Coq devs & plugin devs

Topic: Big Dune PR incoming


view this post on Zulip Gaëtan Gilbert (Jun 24 2022 at 12:03):

that big link doesn't work for me
https://gitlab.com/coq/coq/-/jobs/2636082744 is perf tests not fiat-crypto

view this post on Zulip Gaëtan Gilbert (Jun 24 2022 at 12:04):

Ali Caglayan said:

I want to merge https://github.com/coq/coq/pull/15560 today so we have time to fix any issues that occur and not do it when people are working during the week.

weird logic
if people aren't working who's finding issues?

view this post on Zulip Ali Caglayan (Jun 24 2022 at 12:20):

My thinking is that if we merge this during next week, then many PRs will have to be rebased as people are working on them.

view this post on Zulip Gaëtan Gilbert (Jun 24 2022 at 12:21):

I don't understand

view this post on Zulip Gaëtan Gilbert (Jun 24 2022 at 12:21):

how does a couple days change the number of conflicting prs?

view this post on Zulip Ali Caglayan (Jun 24 2022 at 12:22):

Isn't it better to merge ASAP to find issues ASAP?

view this post on Zulip Ali Caglayan (Jun 24 2022 at 12:23):

If we merge next week, and there is a huge issue (not that I think there will be) suddenly everybody's CI doesn't work etc.

view this post on Zulip Gaëtan Gilbert (Jun 24 2022 at 12:23):

it should be merged when it's ready not based on trying to guess timing

view this post on Zulip Ali Caglayan (Jun 24 2022 at 12:24):

If we merge today and find there is a huge issue, we have the whole weekend to fix it rather than trying to quickly fix it throughout the week

view this post on Zulip Gaëtan Gilbert (Jun 24 2022 at 12:24):

that means asking people to commit to working during the weekend

view this post on Zulip Ali Caglayan (Jun 24 2022 at 12:24):

It is ready to be merged today, I am trying to let everybody know that I will do it

view this post on Zulip Ali Caglayan (Jun 24 2022 at 12:25):

Do you think it should wait? If so why?

view this post on Zulip Gaëtan Gilbert (Jun 24 2022 at 12:25):

if there's a huge issue that CI didn't catch what makes you think you'll catch it before people work with the PR

view this post on Zulip Gaëtan Gilbert (Jun 24 2022 at 12:26):

Ali Caglayan said:

Do you think it should wait? If so why?

I don't know if it should wait, I just reject all reasoning talking about the weekend

view this post on Zulip Ali Caglayan (Jun 24 2022 at 12:27):

The reason I bring up the weekend is because I have time to help fix things.

view this post on Zulip Gaëtan Gilbert (Jun 24 2022 at 12:28):

is it really ready? what about the CI issues?

view this post on Zulip Ali Caglayan (Jun 24 2022 at 12:31):

Performance tests now passed

view this post on Zulip Ali Caglayan (Jun 24 2022 at 12:35):

I've restarted fiat-crypto, if its done then good I will merge

view this post on Zulip Ali Caglayan (Jun 24 2022 at 12:35):

The issue with coqbot on older branches may or may not be fixable, I will take a look now.

view this post on Zulip Guillaume Melquiond (Jun 24 2022 at 12:39):

Not fixable is not an option. We are not just talking about breaking some very old branches. We are also talking about breaking the current 8.16.0 release.

view this post on Zulip Ali Caglayan (Jun 24 2022 at 12:42):

I won't merge if coqbot is not fixable

view this post on Zulip Ali Caglayan (Jun 24 2022 at 12:44):

Actually you know what. Merging coqbot after this PR seems super flaky to me. I think I will delay merging till next week.

view this post on Zulip Ali Caglayan (Jun 24 2022 at 12:45):

I will try to make a backwards compatible coqbot patch today, and I can even deploy it to check it is working fine. Then both the CI for the new dune PR should be green and other PRs too.

view this post on Zulip Ali Caglayan (Jun 24 2022 at 13:59):

OK I've made a patch to coqbot which I am currently deploying.

view this post on Zulip Ali Caglayan (Jun 24 2022 at 14:00):

If it works for other PRs then I will create a PR for coqbot.

view this post on Zulip Ali Caglayan (Jun 24 2022 at 14:00):

This will mean that coqbot will be able to handle before and after #15560.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:10):

A couple of things:

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:13):

view this post on Zulip Ali Caglayan (Jun 24 2022 at 14:16):

coqbot needs to have a higher level understanding of the Github/GItlab API in order to be configurable. That way we can say "add a new CI job, point to this URL in a check, etc.".

view this post on Zulip Ali Caglayan (Jun 24 2022 at 14:16):

This is not something that is easy to implement and will take some time to design.

view this post on Zulip Ali Caglayan (Jun 24 2022 at 14:17):

For now, following the spaghetti and updating links now and then seems to work.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:24):

For now it works, but it is a bit time sink

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:24):

I lost hours with that manual config setup

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:27):

Let me know Ali when you want me to rebase the PR

view this post on Zulip Ali Caglayan (Jun 24 2022 at 14:27):

You can rebase it now if you like

view this post on Zulip Ali Caglayan (Jun 24 2022 at 14:27):

We can also start a bench

view this post on Zulip Ali Caglayan (Jun 24 2022 at 14:28):

Fingers crossed tomorrow it is green :)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:28):

Yes, I'll start the bench

view this post on Zulip Ali Caglayan (Jun 24 2022 at 14:28):

I will leave merging till Monday tho so we have more eyes

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:28):

It should be, it's seen a lot of iterations

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:28):

let's merge when it is ready, but I think it is ready

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:28):

we also need to sync with the Docker people @Erik Martin-Dorel

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:29):

and opam dev

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:29):

this PR finally achieves a very good thing

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:29):

the files in Coq repos should be the ones is core-dev

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:29):

also, the build is finally split in several packages

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:29):

and all the features we'd like are supported

view this post on Zulip Ali Caglayan (Jun 24 2022 at 14:32):

What about docker needs to be synced? Are the dev images not working?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:34):

There is a special coq.opam.docker which is not needed anymore

view this post on Zulip Ali Caglayan (Jun 24 2022 at 14:35):

Create an issue in the coq-docker repo then

view this post on Zulip Ali Caglayan (Jun 24 2022 at 14:36):

Fiat doesn't look good

view this post on Zulip Ali Caglayan (Jun 24 2022 at 14:36):

Its already more than 2 hrs

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:39):

In master takes close to 3 hours usually

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:41):

flags coq is built are not changed

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:41):

already in master is built using dune

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:41):

tho we set release mode now

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:42):

which should be the default, it could be the case that release mode in flambda is slower than dev mode?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:42):

wouldn't be the first time that -O2 makes things slower

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:42):

but that's IMO orthogonal to this PR, the jobs you mention are all already very close to timeout and are timing out in unrelated PRs from time to time

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:42):

I bet if someone would spend time optimizig flambda flags for Coq we'd see an speedup

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:52):

Moreover some more tests were added to performance that are making the thing fail

view this post on Zulip Ali Caglayan (Jun 24 2022 at 14:53):

performance is working now, I'm not sure what you mean

view this post on Zulip Gaëtan Gilbert (Jun 24 2022 at 14:54):

the tests were removed

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:54):

I saw the exponential test for extraction was added, that made it timeout

view this post on Zulip Gaëtan Gilbert (Jun 24 2022 at 14:56):

now removed

view this post on Zulip Gaëtan Gilbert (Jun 24 2022 at 14:57):

(now = some time yesterday)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 14:57):

Thanks for the update

view this post on Zulip Gaëtan Gilbert (Jun 24 2022 at 14:57):

https://github.com/coq-community/coq-performance-tests/pull/22#issuecomment-1165010862

view this post on Zulip Erik Martin-Dorel (Jun 24 2022 at 15:28):

Emilio Jesús Gallego Arias said:

we also need to sync with the Docker people Erik Martin-Dorel

Thanks @Emilio Jesús Gallego Arias for the ping;
can you confirm what should be done regarding dune in docker-coq? (just skimmed your discussion so far, sorry)

FTR, currently all images provide dune 3.2.0:
https://github.com/coq-community/docker-base/blob/a98293eef30ab09ddcb7ad453ced4e657fee6a2f/images.yml#L9

but two versions of dune have been released last week:
https://github.com/ocaml/dune/releases

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:29):

@Erik Martin-Dorel , the change concerns the coq.opam.docker file

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:29):

and coq.dev packages

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:30):

where is the coq.opam.docker file used?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:30):

I couldn't see it, let me clone

view this post on Zulip Erik Martin-Dorel (Jun 24 2022 at 15:31):

it is used by the --locked option of the opam install command

view this post on Zulip Erik Martin-Dorel (Jun 24 2022 at 15:31):

here: https://github.com/coq-community/docker-coq/blob/master/coq/dev/Dockerfile#L21

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:32):

ah ok, I searched for the full thing, I see is just the suffix

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:32):

so I think we can remove that

view this post on Zulip Erik Martin-Dorel (Jun 24 2022 at 15:32):

anyway and as soon as coq.opam.docker is changed in coq#master, this trigger a rebuild of the image coqorg/coq:dev

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:32):

How can we test #15560 with the docker image?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:33):

I just did remove coq.opam.docker there, now it should work fine

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:33):

but note that there are 3 packages to pin

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:33):

coq-core, core-stdlib, and coq

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:33):

and for coqide

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:33):

coqide-sever and coqide

view this post on Zulip Erik Martin-Dorel (Jun 24 2022 at 15:34):

what plan do you have in mind?
testing #15560 with docker-coq before merging the PR?

view this post on Zulip Erik Martin-Dorel (Jun 24 2022 at 15:34):

in which case I can create a temporary image that tracks the underlying PR branch

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:35):

I don't know how to test that, but I'd be nice if we can test it

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:35):

that puts finally an end to the several opam files

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:35):

now the opam files in the coq repos are canonical for coq.dev

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:35):

and for pin

view this post on Zulip Erik Martin-Dorel (Jun 24 2022 at 15:35):

yes, it's better to test it before merging… and needing yet another PR 😅

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:35):

yes I think so

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:36):

I'll be happy to follow the strategy you think is best

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:36):

We have improved in that PR the opam testing we do in CI too

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:36):

quite a bit

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:36):

actually I wonder if we could have some setup in core-dev that just tells opam "look for the opam files in the repos"

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 15:36):

as already we specify

view this post on Zulip Erik Martin-Dorel (Jun 24 2022 at 15:40):

BTW @Emilio Jesús Gallego Arias does this testing requires dune 3.3.x ?

because as I told beforehand, currently coqorg/base assumes dune 3.2.0

view this post on Zulip Ali Caglayan (Jun 24 2022 at 16:01):

This is all dune 2.9

view this post on Zulip Erik Martin-Dorel (Jun 24 2022 at 16:06):

Erik Martin-Dorel said:

what plan do you have in mind?
testing #15560 with docker-coq before merging the PR?

done: see the following GitLab CI pipeline that should take ~30':

https://gitlab.com/coq-community/docker-coq/-/pipelines/572405390

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 16:08):

Thanks a lot @Erik Martin-Dorel ; Coq indeed depends on Dune 2.9

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2022 at 16:08):

or higher, we had to raise the dep due to some bugs that were affecting us, for example in the generation of opam files which we'd like to use

view this post on Zulip Ali Caglayan (Jun 24 2022 at 16:12):

Btw I checked that the CI of the consolidation PR is all green now (from the previous run)

view this post on Zulip Ali Caglayan (Jun 24 2022 at 16:12):

And it looks like the newly deployed coqbot is working fine for this PR

view this post on Zulip Ali Caglayan (Jun 24 2022 at 16:15):

To check it hasn't broken anything in older branches I've reset the refman job here https://github.com/coq/coq/pull/16180

view this post on Zulip Ali Caglayan (Jun 24 2022 at 16:15):

However it doesn't seem to be working

view this post on Zulip Ali Caglayan (Jun 24 2022 at 16:15):

https://gitlab.com/coq/coq/-/jobs/2637491035

view this post on Zulip Ali Caglayan (Jun 24 2022 at 16:15):

This is not coqbot related AFAICT

view this post on Zulip Ali Caglayan (Jun 24 2022 at 16:15):

ERROR: Job failed: failed to pull image "registry.gitlab.com/coq/coq:bionic_coq-V2022-05-20-cb9fc1de6b" with specified policies [always]: Error response from daemon: manifest for registry.gitlab.com/coq/coq:bionic_coq-V2022-05-20-cb9fc1de6b not found: manifest unknown: manifest unknown (manager.go:203:0s)

view this post on Zulip Ali Caglayan (Jun 24 2022 at 16:16):

I've reset it like 5 times now, is there something going on with the docker images?

view this post on Zulip Ali Caglayan (Jun 24 2022 at 16:17):

It can't be related to the coqbot or consolidation PR right?

view this post on Zulip Ali Caglayan (Jun 24 2022 at 16:18):

Is it because the job is old?

view this post on Zulip Gaëtan Gilbert (Jun 24 2022 at 16:32):

yes, it's older than the most recent image so its image got cleaned up

view this post on Zulip Ali Caglayan (Jun 28 2022 at 10:06):

Merging soon

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 10:08):

(bracing for impact)

view this post on Zulip Ali Caglayan (Jun 28 2022 at 10:24):

Don't brace just yet, still waiting for @Erik Martin-Dorel because he wants to merge something before

view this post on Zulip Erik Martin-Dorel (Jun 28 2022 at 10:37):

Yes, thanks (give me 15' and I'm back to my office)

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 10:38):

This kind of PR is like a twin-engine Aeoroflot tupolev bound for Omsk, it's always better to bring your own parachute and brace constantly, just in case.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 28 2022 at 12:00):

I apologize in advance @Pierre-Marie Pédrot if we disappoint you and in the it just turns out to be a ride in 25cts plastic horse machine

view this post on Zulip Matthieu Sozeau (Jun 28 2022 at 12:11):

Fingers crossed :) IIUC we can expect the coqorg/coq:dev docker image to work fine once this is merged?

view this post on Zulip Ali Caglayan (Jun 28 2022 at 12:49):

@Matthieu Sozeau Yes, Erik took care of that.

view this post on Zulip Ali Caglayan (Jun 28 2022 at 14:26):

merged

view this post on Zulip Ralf Jung (Jun 29 2022 at 02:30):

is it possible that this broke the coq.dev opam packages?

[ERROR] The installation of coq failed at "make COQ_USE_DUNE= install".

#=== ERROR while installing coq.dev ===========================================#
# context     2.1.1 | linux/x86_64 | ocaml-variants.4.14.0+options | https://coq.inria.fr/opam/core-dev#2022-06-25 15:20
# path        ~/.opam/coq-test/.opam-switch/build/coq.dev
# command     ~/.opam/opam-init/hooks/sandbox.sh install make COQ_USE_DUNE= install
# exit-code   2
# env-file    ~/.opam/log/coq-837414-1861ee.env
# output-file ~/.opam/log/coq-837414-1861ee.out
### output ###
# To install Coq using dune, use 'dune build -p P && dune install P'
# where P is any of the packages defined by opam files in the root dir
# make: *** [Makefile.dune:170: install] Error 1

view this post on Zulip Ralf Jung (Jun 29 2022 at 02:31):

I did opam update && opam upgrade, to no avail

view this post on Zulip Pierre Roux (Jun 29 2022 at 05:08):

Yes, https://github.com/coq/opam-coq-archive/pull/1923 not merged yet

view this post on Zulip Ralf Jung (Jun 29 2022 at 11:25):

ah, okay. Iris CI will fail until that happens then, so I'd appreciate a quick merge. :)

view this post on Zulip Ralf Jung (Jun 29 2022 at 11:26):

(FWIW this looks like a coordination issue to me, if the Coq PR was merged knowing that would break opam.)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 29 2022 at 12:07):

I was aware of the coordination problem, and was correctly noted in my todo, I just literally couldn't get to the keyboard in time

view this post on Zulip Erik Martin-Dorel (Jun 29 2022 at 12:25):

Hi @Ralf Jung
In the meantime, note that you can prepend your opam install coq.dev command with some opam git pinning to use the official upstream-committed .opam files:

opam pin add -n -y -k git coq-core.dev "git+https://github.com/coq/coq#master"
opam pin add -n -y -k git coq-stdlib.dev "git+https://github.com/coq/coq#master"
opam pin add -n -y -k git coq.dev "git+https://github.com/coq/coq#master"
opam install -j "$(nproc)" coq.dev

view this post on Zulip Ralf Jung (Jun 29 2022 at 13:51):

that doesn't really help for CI, where we have infrastructure to very easily say "install that version of that package" but not "run this arbitrary code"

view this post on Zulip Ralf Jung (Jun 29 2022 at 13:52):

Emilio Jesús Gallego Arias said:

I was aware of the coordination problem, and was correctly noted in my todo, I just literally couldn't get to the keyboard in time

fair.
I hope the opam PR gets merged quickly then. :)


Last updated: Feb 06 2023 at 00:03 UTC