Michael Soegtrop (Oct 16 2022 at 09:09): 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.
Théo Zimmermann (Oct 16 2022 at 09:45):Isn't the Coq Platform script install supposed to use the local opam patch repo?
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.
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.
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
Paolo Giarrusso (Oct 16 2022 at 13:49):(pls ignore if that's already treaded ground, but IIRC what we discussed was different)
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)
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.
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
Michael Soegtrop (Oct 16 2022 at 13:53):My fear is that pinning everything make Coq Platform less adaptive to system changes.
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)
Paolo Giarrusso (Oct 16 2022 at 13:54):_maybe_ harder
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
Théo Zimmermann (Oct 16 2022 at 13:55):I am completely missing your point Karl.
Paolo Giarrusso (Oct 16 2022 at 13:55):(also, VSCode itself self-updates monthly, so I'm not sure you _could_ support that)
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.
Paolo Giarrusso (Oct 16 2022 at 13:57):Michael: sorry, I wasn't trying to push further
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.
Karl Palmskog (Oct 16 2022 at 13:58):isn't everything that isn't pinned/curated considered outside scope [of Platform]?
Michael Soegtrop (Oct 16 2022 at 13:58):@Karl Palmskog : well only as long as it works ...
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.
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.
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).
Théo Zimmermann (Oct 16 2022 at 14:01):BTW, this broke the Coq CI. But I guess you are already aware.
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.
Michael Soegtrop (Oct 16 2022 at 14:02):The fix CI is almost through ...
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.
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.
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?
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.
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.
Paolo Giarrusso (Oct 16 2022 at 14:08):yep, we discussed that one already :-)
Théo Zimmermann (Oct 16 2022 at 14:09):Paolo Giarrusso said:
I think there's a genuine tradeoff, but maybe
opam lockwould 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.
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.
Michael Soegtrop (Oct 16 2022 at 14:12):@Théo Zimmermann : the fix is merged, so Coq CI should be fine again.
Paolo Giarrusso (Oct 16 2022 at 14:13):to be clear, reproducibility also has well-known tradeoffs (including upsides) even for development :-)
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.
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:
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?
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
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.
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?
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.
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: Jun 03 2023 at 05:01 UTC