Ensure `coqide.opam` actually installs `coqide` #16505

Blaisorblade · 2022-09-17T14:26:29Z

Naive, but worth an attempt. I encourage people to take over or open new PRs if this is useful.

Without this change, dune build coqide.install fails silently when dependencies are missing. With this patch, dune build coqide-server.install still succeeds while dune build coqide.install reports the missing deps:

$ dune build coqide.install
File "ide/coqide/dune", line 33, characters 54-74:
33 |  (libraries coqide-server.protocol coqide-server.core lablgtk3-sourceview3))
                                                           ^^^^^^^^^^^^^^^^^^^^
Error: Library "lablgtk3-sourceview3" not found.
-> required by library "coqide_gui" in _build/default/ide/coqide
-> required by executable coqide_main in ide/coqide/dune:53
-> required by _build/default/ide/coqide/coqide_main.exe
-> required by _build/install/default/bin/coqide
-> required by _build/default/coqide.install

Added changelog.

Probably naive, but worth an attempt.

Blaisorblade · 2022-09-17T14:30:01Z

The optional directives I'm dropping were added in faf6ffc and 1d454c7, but I don't understand those commit logs.

Blaisorblade · 2022-09-17T15:00:32Z

https://gitlab.com/coq/coq/-/jobs/3043744428 fails with

$ dune build -p coq-core,coq-stdlib,coqide-server,coqide,coq
File "ide/coqide/dune", line 33, characters 54-74:
33 |  (libraries coqide-server.protocol coqide-server.core lablgtk3-sourceview3))
                                                           ^^^^^^^^^^^^^^^^^^^^
Error: Library "lablgtk3-sourceview3" not found.

so I now explicitly skip building coqide on that ~~platform~~ Gitlab CI job.

This should be dropped if we change the default in the template (or if you prefer), but it seems `configure` will auto-enable coqide if dependencies are available.

Blaisorblade · 2022-09-17T15:56:45Z

This passed at least NJOBS=10 make test-suite locally; seems good enough for an initial review.

Alizter · 2022-09-17T16:04:45Z

Windows build seems to have failed. ~~I wonder if we were ever actually building CoqIDE on windows before?~~ cc @MSoegtropIMC any idea what might have gone wrong?

Blaisorblade · 2022-09-17T16:18:03Z

Windows build seems to have failed. ~~I wonder if we were ever actually building CoqIDE on windows before?~~ cc @MSoegtropIMC any idea what might have gone wrong?

I assume not: That’s the same error I got at first (and fixed) on 32bit, so we should disable that as well. Or install the dependency if possible (32bit has a comment clarifying it's not possible for now).

FWIW, there’s a potential regression: the commit messages I linked suggest maybe something was still built and tested in the coqide packages? I haven’t checked, but even if that's the case, that stuff should move elsewhere. I'm sure I miss something, but "coqide might not include coqide" is too confusing.

Zimmi48 · 2022-09-17T16:38:38Z

If coqide was not built on windows, that was a bug in the CI configuration.

MSoegtropIMC · 2022-09-18T10:47:12Z

@Blaisorblade : in Coq Platform, where opam takes care that all dependencies are there, CoqIDE builds fine on all platforms (MacOS, Linux, Windows). I didn't have much of a look at the "outside of opam" builds. Afaik the CoqIDE opam file is dune based.

…iew3

Blaisorblade · 2022-09-18T12:46:41Z

@MSoegtropIMC The problem was in the CI for the dev platform.

AFAICT:

coq/coqide.opam did not depend on lablgtk3-sourceview3. This was a bug and I pushed a fix.
The platform relies on that dependency existing, so package picks only pin lablgtk3.3.1.2, and let opam install lablgtk3-sourceview3. I don't consider that a bug.
Before this MR, if lablgtk3-sourceview3 was not installed, installing coq/coqide.opam succeeded without building coqide; thankfully @palmskog noticed and @silene diagnosed it.

Blaisorblade · 2022-09-19T00:56:15Z

Cool, this is passing CI — up to unimath's hopefully unrelated time out.

Blaisorblade · 2022-09-19T10:38:03Z

BTW: dune regeneration also suggests adding an odoc optional dependency: Blaisorblade@d3c0ab8. I'd rather not add it here (and risk breaking CI and entangling discussions), but we could do an MR on top.

Alizter · 2022-09-19T11:04:16Z

@Blaisorblade That's fine to ignore it for now. The OCaml documentation generated by dune relies on odoc which is why you are seeing it.

ejgallego · 2022-09-19T20:12:28Z

Why not move coqide's to its own CI job?

Blaisorblade · 2022-09-20T11:20:20Z

This MR attempts (and I think succeeds) at an obvious fix for a clear bug. I don't personally use coqide, but it seemed it could be simple enough to try.

Splitting coqide seems a separate question: while it avoids ~3 lines of shell code, it requires adding and maintaining 5 new jobs, since there are 6 jobs building coq and only 1 of those skips coqide. That seems a regression to me, but that's not my call.

Either way, I admit I don't think I have time for it — so it's fine if this MR is turned down.

ejgallego · 2022-09-20T12:40:30Z

I think the PR makes sense, but indeed the shell code looks a bit hackish, the problem is that I don't understand shell well :)

I'd be nice if we can find a quick way to not to use this hack, so I was thinking that maybe another job could do the trick, OMMV.

Alizter · 2022-09-20T12:54:04Z

Let's keep this fix for now, splitting the job is a separate future concern.

Alizter · 2022-09-20T12:55:16Z

@SkySkimmer I wouldn't mind another pair of eyes if you don't mind

SkySkimmer · 2022-09-20T13:08:23Z

I don't think we should split the jobs, I expect the coqide jobs would be dominated by docker/VM boot overhead.
Changes look OK, we should probably remove the configure switch since configure doesn't command the default targets anymore but that's for another PR.

Blaisorblade · 2022-09-20T14:20:16Z

.gitlab-ci.yml

    - dev/ci/gitlab-section.sh end coq.build

    - dev/ci/gitlab-section.sh start coq.install coq.install
-    - dune install --prefix="$(pwd)/_install_ci" coq-core coq-stdlib coqide-server coqide coq
+    - dune install --prefix="$(pwd)/_install_ci" $(sed -e 's/,/ /g' <<< ${PKGS})


This idiom isn't that hard if you know, but it is gratuitous obfuscation:

Suggested change

- dune install --prefix="$(pwd)/_install_ci" $(sed -e 's/,/ /g' <<< ${PKGS})

- dune install --prefix="$(pwd)/_install_ci" $(echo ${PKGS} | sed -e 's/,/ /g')

(This shouldn't block merge, but is motivated by @ejgallego 's comment and will help some people read it).

If we are talking about more concise and possibly more readable alternatives, I suggest ${PKGS//,/ }.

Zimmi48 · 2022-09-20T18:57:43Z

The choice of skipping the build of CoqIDE in the 32 bit job was made 5 years ago in the initial version of the GitLab CI configuration. Has someone checked that it is still necessary? If this is the only job skipping it and there's actually no need to skip it, it would save a lot of logical complexity.

Blaisorblade · 2022-09-20T21:09:15Z

Has someone checked that it is still necessary?

This MR definitely failed before I implemented the skipping. Maybe one could install the missing library, I can at least try in the job (but I have no idea/privileges how to patch it in the Docker image).

Alizter · 2022-09-20T21:11:41Z

Let's defer that to a separate PR for now I think.

Alizter · 2022-09-20T21:12:05Z

@Blaisorblade Are you happy for me to merge?

Blaisorblade · 2022-09-20T21:38:16Z

@Alizter Very happy with merging! We can defer all the other improvements.

Alizter · 2022-09-20T21:39:09Z

@coqbot merge now

Blaisorblade · 2022-10-11T08:57:09Z

I assume not: That’s the same error I got at first (and fixed) on 32bit, so we should disable that as well. FWIW, there’s a potential regression: the commit messages I linked suggest maybe something was still built and tested in the coqide packages? I haven’t checked, but even if that's the case, that stuff should move elsewhere. I'm sure I miss something, but "coqide might not include coqide" is too confusing.

On Sat 17. Sep 2022 at 18:04, Ali Caglayan ***@***.***> wrote: Windows build seems to have failed. I wonder if we were ever actually building CoqIDE on windows before? — Reply to this email directly, view it on GitHub <#16505 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AACGZKEE24DV22L2JKJHKRLV6XT2RANCNFSM6AAAAAAQPA3ZPQ> . You are receiving this because you authored the thread.Message ID: ***@***.***>

-- Paolo G. Giarrusso

Try making coqide non-optional

8779460

Probably naive, but worth an attempt.

Blaisorblade added 3 commits September 17, 2022 17:19

Gitlab CI: skip building coqide on 32bit

fda8226

Gitlab CI: Also pass -coqide opt automatically

7cc1faf

Gitlab CI: remove redundant COQIDE: "opt" settings

8baf88a

This should be dropped if we change the default in the template (or if you prefer), but it seems `configure` will auto-enable coqide if dependencies are available.

Blaisorblade force-pushed the coqide-non-optional branch from 9387fbd to 8baf88a Compare September 17, 2022 15:19

Blaisorblade marked this pull request as ready for review September 17, 2022 15:56

Blaisorblade requested review from a team as code owners September 17, 2022 15:56

dune-project, coqide.opam: manually add dependency to lablgtk-sourcev…

f77b24c

…iew3

Blaisorblade changed the title ~~Try making coqide non-optional~~ Ensure coqide.opam actually installs coqide Sep 19, 2022

Alizter approved these changes Sep 20, 2022

View reviewed changes

Alizter added kind: fix This fixes a bug or incorrect documentation. part: CI The continuous integration system. labels Sep 20, 2022

Alizter added this to the 8.17+rc1 milestone Sep 20, 2022

Alizter added this to To do in CI via automation Sep 20, 2022

Alizter self-assigned this Sep 20, 2022

SkySkimmer mentioned this pull request Sep 20, 2022

configure: remove coqide switch #16512

Merged

Blaisorblade commented Sep 20, 2022

View reviewed changes

coqbot-app bot merged commit 944ed31 into coq:master Sep 20, 2022

CI automation moved this from To do to Done Sep 20, 2022

Blaisorblade deleted the coqide-non-optional branch September 20, 2022 23:30

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Ensure `coqide.opam` actually installs `coqide` #16505

Ensure `coqide.opam` actually installs `coqide` #16505

Blaisorblade commented Sep 17, 2022 •

edited

Blaisorblade commented Sep 17, 2022

Blaisorblade commented Sep 17, 2022 •

edited

Blaisorblade commented Sep 17, 2022

Alizter commented Sep 17, 2022 •

edited

Blaisorblade commented Sep 17, 2022 •

edited

Zimmi48 commented Sep 17, 2022

MSoegtropIMC commented Sep 18, 2022

Blaisorblade commented Sep 18, 2022

Blaisorblade commented Sep 19, 2022

Blaisorblade commented Sep 19, 2022

Alizter commented Sep 19, 2022

ejgallego commented Sep 19, 2022

Blaisorblade commented Sep 20, 2022

ejgallego commented Sep 20, 2022

Alizter commented Sep 20, 2022

Alizter commented Sep 20, 2022

SkySkimmer commented Sep 20, 2022

Blaisorblade Sep 20, 2022

Blaisorblade Sep 20, 2022

silene Sep 20, 2022

Zimmi48 commented Sep 20, 2022

Blaisorblade commented Sep 20, 2022

Alizter commented Sep 20, 2022

Alizter commented Sep 20, 2022

Blaisorblade commented Sep 20, 2022

Alizter commented Sep 20, 2022

Blaisorblade commented Oct 11, 2022 via email

	- dune install --prefix="$(pwd)/_install_ci" $(sed -e 's/,/ /g' <<< ${PKGS})
	- dune install --prefix="$(pwd)/_install_ci" $(echo ${PKGS} \| sed -e 's/,/ /g')

Navigation Menu

Ensure coqide.opam actually installs coqide #16505

Ensure coqide.opam actually installs coqide #16505

Conversation

Blaisorblade commented Sep 17, 2022 • edited

Blaisorblade commented Sep 17, 2022

Blaisorblade commented Sep 17, 2022 • edited

Blaisorblade commented Sep 17, 2022

Alizter commented Sep 17, 2022 • edited

Blaisorblade commented Sep 17, 2022 • edited

Zimmi48 commented Sep 17, 2022

MSoegtropIMC commented Sep 18, 2022

Blaisorblade commented Sep 18, 2022

Blaisorblade commented Sep 19, 2022

Blaisorblade commented Sep 19, 2022

Alizter commented Sep 19, 2022

ejgallego commented Sep 19, 2022

Blaisorblade commented Sep 20, 2022

ejgallego commented Sep 20, 2022

Alizter commented Sep 20, 2022

Alizter commented Sep 20, 2022

SkySkimmer commented Sep 20, 2022

Blaisorblade Sep 20, 2022

Choose a reason for hiding this comment

Blaisorblade Sep 20, 2022

Choose a reason for hiding this comment

silene Sep 20, 2022

Choose a reason for hiding this comment

Zimmi48 commented Sep 20, 2022

Blaisorblade commented Sep 20, 2022

Alizter commented Sep 20, 2022

Alizter commented Sep 20, 2022

Blaisorblade commented Sep 20, 2022

Alizter commented Sep 20, 2022

Blaisorblade commented Oct 11, 2022 via email

Ensure `coqide.opam` actually installs `coqide` #16505

Ensure `coqide.opam` actually installs `coqide` #16505

Blaisorblade commented Sep 17, 2022 •

edited

Blaisorblade commented Sep 17, 2022 •

edited

Alizter commented Sep 17, 2022 •

edited

Blaisorblade commented Sep 17, 2022 •

edited