Ali Caglayan (Jun 24 2022 at 11:43): Ali Caglayan (Jun 24 2022 at 11:43):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.
Ali Caglayan (Jun 24 2022 at 11:43):There are some issues standing however, such as with the jobs in the CI.
Ali Caglayan (Jun 24 2022 at 11:45):I see that performance tests takes around 00:23:58 before
Ali Caglayan (Jun 24 2022 at 11:46):Now it hit the limit, looks like it was restarted, let's see what is happening.
Ali Caglayan (Jun 24 2022 at 11:47):fiat-crypto was also taking 1:40
Ali Caglayan (Jun 24 2022 at 11:49):Logs for an old fiat-crypto job don't show COQNATIVE
Ali Caglayan (Jun 24 2022 at 11:49): Ali Caglayan (Jun 24 2022 at 11:50):But the new one does
Ali Caglayan (Jun 24 2022 at 11:50):https://gitlab.com/coq/coq/-/jobs/2636082744
Ali Caglayan (Jun 24 2022 at 11:50):I can't tell if this is because some hiding flags were tweaked
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
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?
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.
Gaëtan Gilbert (Jun 24 2022 at 12:21):I don't understand
Gaëtan Gilbert (Jun 24 2022 at 12:21):how does a couple days change the number of conflicting prs?
Ali Caglayan (Jun 24 2022 at 12:22):Isn't it better to merge ASAP to find issues ASAP?
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.
Gaëtan Gilbert (Jun 24 2022 at 12:23):it should be merged when it's ready not based on trying to guess timing
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
Gaëtan Gilbert (Jun 24 2022 at 12:24):that means asking people to commit to working during the weekend
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
Ali Caglayan (Jun 24 2022 at 12:25):Do you think it should wait? If so why?
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
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
Ali Caglayan (Jun 24 2022 at 12:27):The reason I bring up the weekend is because I have time to help fix things.
Gaëtan Gilbert (Jun 24 2022 at 12:28):is it really ready? what about the CI issues?
Ali Caglayan (Jun 24 2022 at 12:31):Performance tests now passed
Ali Caglayan (Jun 24 2022 at 12:35):I've restarted fiat-crypto, if its done then good I will merge
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.
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.
Ali Caglayan (Jun 24 2022 at 12:42):I won't merge if coqbot is not fixable
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.
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.
Ali Caglayan (Jun 24 2022 at 13:59):OK I've made a patch to coqbot which I am currently deploying.
Ali Caglayan (Jun 24 2022 at 14:00):If it works for other PRs then I will create a PR for coqbot.
Ali Caglayan (Jun 24 2022 at 14:00):This will mean that coqbot will be able to handle before and after #15560.
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:10):A couple of things:
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:13):build:base to build stdlib doc (as Coq coudln't built it from installed sources). Now that works, so we have two jobs as opposed to one before. That motivated me to go and update coqbot for this. But the big problem I see is that coq/bot is embedding configuration in its source code. It should not do that, otherwise indeed as branches evolves, it is a mess to keep up to date. 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.".
Ali Caglayan (Jun 24 2022 at 14:16):This is not something that is easy to implement and will take some time to design.
Ali Caglayan (Jun 24 2022 at 14:17):For now, following the spaghetti and updating links now and then seems to work.
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:24):For now it works, but it is a bit time sink
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:24):I lost hours with that manual config setup
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:27):Let me know Ali when you want me to rebase the PR
Ali Caglayan (Jun 24 2022 at 14:27):You can rebase it now if you like
Ali Caglayan (Jun 24 2022 at 14:27):We can also start a bench
Ali Caglayan (Jun 24 2022 at 14:28):Fingers crossed tomorrow it is green :)
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:28):Yes, I'll start the bench
Ali Caglayan (Jun 24 2022 at 14:28):I will leave merging till Monday tho so we have more eyes
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:28):It should be, it's seen a lot of iterations
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:28):let's merge when it is ready, but I think it is ready
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:28):we also need to sync with the Docker people @Erik Martin-Dorel
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:29):and opam dev
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:29):this PR finally achieves a very good thing
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:29):the files in Coq repos should be the ones is core-dev
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:29):also, the build is finally split in several packages
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:29):and all the features we'd like are supported
Ali Caglayan (Jun 24 2022 at 14:32):What about docker needs to be synced? Are the dev images not working?
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:34):There is a special coq.opam.docker which is not needed anymore
Ali Caglayan (Jun 24 2022 at 14:35):Create an issue in the coq-docker repo then
Ali Caglayan (Jun 24 2022 at 14:36):Fiat doesn't look good
Ali Caglayan (Jun 24 2022 at 14:36):Its already more than 2 hrs
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:39):In master takes close to 3 hours usually
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:41):flags coq is built are not changed
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:41):already in master is built using dune
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:41):tho we set release mode now
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?
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:42):wouldn't be the first time that -O2 makes things slower
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
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
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
Ali Caglayan (Jun 24 2022 at 14:53):performance is working now, I'm not sure what you mean
Gaëtan Gilbert (Jun 24 2022 at 14:54):the tests were removed
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:54):I saw the exponential test for extraction was added, that made it timeout
Gaëtan Gilbert (Jun 24 2022 at 14:56):now removed
Gaëtan Gilbert (Jun 24 2022 at 14:57):(now = some time yesterday)
Emilio Jesús Gallego Arias (Jun 24 2022 at 14:57):Thanks for the update
Gaëtan Gilbert (Jun 24 2022 at 14:57):https://github.com/coq-community/coq-performance-tests/pull/22#issuecomment-1165010862
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
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:29):@Erik Martin-Dorel , the change concerns the coq.opam.docker file
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:29):and coq.dev packages
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:30):where is the coq.opam.docker file used?
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:30):I couldn't see it, let me clone
Erik Martin-Dorel (Jun 24 2022 at 15:31):it is used by the --locked option of the opam install command
Erik Martin-Dorel (Jun 24 2022 at 15:31):here: https://github.com/coq-community/docker-coq/blob/master/coq/dev/Dockerfile#L21
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
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:32):so I think we can remove that
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
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:32):How can we test #15560 with the docker image?
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:33):I just did remove coq.opam.docker there, now it should work fine
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:33):but note that there are 3 packages to pin
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:33):coq-core, core-stdlib, and coq
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:33):and for coqide
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:33):coqide-sever and coqide
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?
Erik Martin-Dorel (Jun 24 2022 at 15:34):in which case I can create a temporary image that tracks the underlying PR branch
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
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:35):that puts finally an end to the several opam files
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:35):now the opam files in the coq repos are canonical for coq.dev
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:35):and for pin
Erik Martin-Dorel (Jun 24 2022 at 15:35):yes, it's better to test it before merging… and needing yet another PR 😅
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:35):yes I think so
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:36):I'll be happy to follow the strategy you think is best
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
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:36):quite a bit
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"
Emilio Jesús Gallego Arias (Jun 24 2022 at 15:36):as already we specify
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
Ali Caglayan (Jun 24 2022 at 16:01):This is all dune 2.9
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
Emilio Jesús Gallego Arias (Jun 24 2022 at 16:08):Thanks a lot @Erik Martin-Dorel ; Coq indeed depends on Dune 2.9
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
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)
Ali Caglayan (Jun 24 2022 at 16:12):And it looks like the newly deployed coqbot is working fine for this PR
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
Ali Caglayan (Jun 24 2022 at 16:15):However it doesn't seem to be working
Ali Caglayan (Jun 24 2022 at 16:15):https://gitlab.com/coq/coq/-/jobs/2637491035
Ali Caglayan (Jun 24 2022 at 16:15):This is not coqbot related AFAICT
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)
I've reset it like 5 times now, is there something going on with the docker images?
Ali Caglayan (Jun 24 2022 at 16:17):It can't be related to the coqbot or consolidation PR right?
Ali Caglayan (Jun 24 2022 at 16:18):Is it because the job is old?
Gaëtan Gilbert (Jun 24 2022 at 16:32):yes, it's older than the most recent image so its image got cleaned up
Ali Caglayan (Jun 28 2022 at 10:06):Merging soon
Pierre-Marie Pédrot (Jun 28 2022 at 10:08):(bracing for impact)
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
Erik Martin-Dorel (Jun 28 2022 at 10:37):Yes, thanks (give me 15' and I'm back to my office)
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.
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
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?
Ali Caglayan (Jun 28 2022 at 12:49):@Matthieu Sozeau Yes, Erik took care of that.
Ali Caglayan (Jun 28 2022 at 14:26):merged
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
I did opam update && opam upgrade, to no avail
Pierre Roux (Jun 29 2022 at 05:08):Yes, https://github.com/coq/opam-coq-archive/pull/1923 not merged yet
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. :)
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.)
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
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
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"
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: Apr 17 2024 at 23:01 UTC