Stream: Coq Platform devs & users

Topic: Building from sources fails on Windows


view this post on Zulip Michael Soegtrop (Oct 16 2022 at 09:09):

Please note that 2022.09~beta1 (and all other previous releases) currently have an issue when building from sources caused by an updated lablgtk which is missing a patch (my bad to not push it upstream). There is a PR for a fix in CI.

view this post on Zulip Théo Zimmermann (Oct 16 2022 at 09:45):

Isn't the Coq Platform script install supposed to use the local opam patch repo?

view this post on Zulip Théo Zimmermann (Oct 16 2022 at 09:50):

Oh, I see that what you meant is that the patch was not pushed to the Coq Platform repo.

view this post on Zulip Michael Soegtrop (Oct 16 2022 at 11:20):

The issue is that I use a locally patched lablgtk, but this patch is only valid for a specific version. Now a new version was published, so the build picks up the new version without the patch.

I thought in the past about fixing the version of lablgtk to the one I patched, but then I wouldn't find out if there are new versions ...

This would be solved if I push my fix upstream. I didn't do so because for Windows I need some more fixes, which were not accepted in the MinGW Opam repo.

view this post on Zulip Paolo Giarrusso (Oct 16 2022 at 13:48):

if the intention of the platform is to be a fully tested distribution, isn't it a logical conclusion that you _need_ to pin lablgtk for users / have upper bounds? You need to be notified somehow, but in this perspective, users shouldn't

view this post on Zulip Paolo Giarrusso (Oct 16 2022 at 13:49):

(pls ignore if that's already treaded ground, but IIRC what we discussed was different)

view this post on Zulip Karl Palmskog (Oct 16 2022 at 13:50):

I understand that CoqIDE is special, but arguably VsCoq + VS Code should be tested as well if we adopt that mindset (e.g., set up CI to pull latest VS Code and install VsCoq, then run a bit)

view this post on Zulip Michael Soegtrop (Oct 16 2022 at 13:52):

Currently I only pin Ocaml itself, Coq related packages and packages where not pinning would result in changing the version in a sequential build. The assumption is that changes in the OCaml ecosystem don't affect Coq. And indeed such effects are rare.

view this post on Zulip Karl Palmskog (Oct 16 2022 at 13:52):

at least according to the survey, the userbase is fairly evenly split across Emacs, CoqIDE, VS Code

view this post on Zulip Michael Soegtrop (Oct 16 2022 at 13:53):

My fear is that pinning everything make Coq Platform less adaptive to system changes.

view this post on Zulip Paolo Giarrusso (Oct 16 2022 at 13:54):

Karl: I wasn't trying to expand the scope of the platform's testing (it'd be great but harder)

view this post on Zulip Paolo Giarrusso (Oct 16 2022 at 13:54):

_maybe_ harder

view this post on Zulip Karl Palmskog (Oct 16 2022 at 13:55):

well, if you pin, isn't that extending scope? Then it's basically official that some version is part of the Platform

view this post on Zulip Théo Zimmermann (Oct 16 2022 at 13:55):

I am completely missing your point Karl.

view this post on Zulip Paolo Giarrusso (Oct 16 2022 at 13:55):

(also, VSCode itself self-updates monthly, so I'm not sure you _could_ support that)

view this post on Zulip Michael Soegtrop (Oct 16 2022 at 13:56):

@Paolo Giarrusso : my point is more or less that this is not enough of a problem to demand a solution. Such things happen about once a year and I fix them.

view this post on Zulip Paolo Giarrusso (Oct 16 2022 at 13:57):

Michael: sorry, I wasn't trying to push further

view this post on Zulip Michael Soegtrop (Oct 16 2022 at 13:58):

Don't be sorry - I enjoy a discussion on such topics. It is not easy to make the right decisions here.

view this post on Zulip Karl Palmskog (Oct 16 2022 at 13:58):

isn't everything that isn't pinned/curated considered outside scope [of Platform]?

view this post on Zulip Michael Soegtrop (Oct 16 2022 at 13:58):

@Karl Palmskog : well only as long as it works ...

view this post on Zulip Michael Soegtrop (Oct 16 2022 at 14:00):

But yes, my current philosophy is to not pin things which are not Coq or the OCaml compiler version unless there is very good reason. So far this did work well, but I can't tell if this will ever be the case.

view this post on Zulip Théo Zimmermann (Oct 16 2022 at 14:00):

Personally, I was of the opinion that it would be better to pin every dependency for reproducibility, but Michael's argument above convinced me that it is not the best idea.

view this post on Zulip Michael Soegtrop (Oct 16 2022 at 14:00):

The current issue definitely could have been avoided by pushing my lablgtk fixes upstream (will do so now).

view this post on Zulip Théo Zimmermann (Oct 16 2022 at 14:01):

BTW, this broke the Coq CI. But I guess you are already aware.

view this post on Zulip Michael Soegtrop (Oct 16 2022 at 14:02):

@Théo Zimmermann : the point of the daily builds is to notify me in case something bad happens.

view this post on Zulip Michael Soegtrop (Oct 16 2022 at 14:02):

The fix CI is almost through ...

view this post on Zulip Michael Soegtrop (Oct 16 2022 at 14:04):

Another reason for not pinning everything is that it would make Coq Platform extremely rigid and it would become hard to compile say latest plugins on top of it, which might require a newer version of something. I try to avoid version upper bounds as much as possible and usually encourage packages in Coq Platform to drop these.

view this post on Zulip Michael Soegtrop (Oct 16 2022 at 14:05):

If we want Coq Platform to be a base for further development, pinning would be quite a pain.

view this post on Zulip Paolo Giarrusso (Oct 16 2022 at 14:06):

I think there's a genuine tradeoff, but maybe opam lock would be a better tool for those who want to opt-in to reproducibility?

view this post on Zulip Paolo Giarrusso (Oct 16 2022 at 14:07):

I have _not_ used it so I don't know, but I think the use-case exists.

view this post on Zulip Michael Soegtrop (Oct 16 2022 at 14:08):

Btw.: currently even the coq-xyz packages are not pinned, but I install all of them with an explicit version and test if there are no recompiles in a sequential build. Before 2022.09 even Coq was not pinned, but from 2022.09 on I pin Coq to avoid unwanted effects.

view this post on Zulip Paolo Giarrusso (Oct 16 2022 at 14:08):

yep, we discussed that one already :-)

view this post on Zulip Théo Zimmermann (Oct 16 2022 at 14:09):

Paolo Giarrusso said:

I think there's a genuine tradeoff, but maybe opam lock would be a better tool for those who want to opt-in to reproducibility?

@Karl Palmskog @Enrico Tassi We might want to discuss these aspects in the journal version of our "Coq Platform for reproducibility" paper.

view this post on Zulip Michael Soegtrop (Oct 16 2022 at 14:10):

But again, it might make sense to have a "rigid" option, say for research artefact reproduction or so.

view this post on Zulip Michael Soegtrop (Oct 16 2022 at 14:12):

@Théo Zimmermann : the fix is merged, so Coq CI should be fine again.

view this post on Zulip Paolo Giarrusso (Oct 16 2022 at 14:13):

to be clear, reproducibility also has well-known tradeoffs (including upsides) even for development :-)

view this post on Zulip Michael Soegtrop (Oct 16 2022 at 14:14):

One more note on this: from gut feeling I would say that in the past it did happen more frequently that changes in cygwin than changes in opam broke the Windows CI.

view this post on Zulip Michael Soegtrop (Oct 16 2022 at 14:15):

@Paolo Giarrusso : indeed - for his reason I think it might make sense to have different levels of rigidity of the picking:

view this post on Zulip Jim Fehrle (Oct 16 2022 at 15:02):

Karl Palmskog said:

I understand that CoqIDE is special, but arguably VsCoq + VS Code should be tested as well if we adopt that mindset (e.g., set up CI to pull latest VS Code and install VsCoq, then run a bit)

A reasonable wish, but if you start a CoqIDE or vsCode process, you would need some tooling to send it keystrokes and mouse actions. Do you know of any good options to do that?

view this post on Zulip Karl Palmskog (Oct 16 2022 at 15:11):

VS Code is essentially a web application, so Selenium is the usual answer, which they seem to have applied here: https://github.com/redhat-developer/vscode-extension-tester

view this post on Zulip Michael Soegtrop (Oct 17 2022 at 07:44):

In my experience testing GUI applications on headless CI runners poses a lot of extra challenges. I guess to make this in any way feasible one would need a runner which is not headless. For GTK there should be test frameworks and for VSCode I would also use Selenium.

view this post on Zulip Pierre-Marie Pédrot (Oct 17 2022 at 11:37):

Despite the PR having been merged, it seems that the Coq Windows CI is still not fixed. Is it normal (some deployment delay?) or is that another issue?

view this post on Zulip Théo Zimmermann (Oct 17 2022 at 12:54):

Ah, it's possible that the version of the Platform we use is pinned. In this case, we should bump the pin.

view this post on Zulip Michael Soegtrop (Oct 17 2022 at 13:31):

Indeed there is : https://github.com/coq/coq/blob/0c8ab3b6475de377bc11a7653d073bc4b4556b19/.github/workflows/ci-windows.yml#L35


Last updated: Jan 30 2023 at 11:03 UTC