Emilio Jesús Gallego Arias (Apr 06 2022 at 18:45): Emilio Jesús Gallego Arias (Apr 06 2022 at 18:45):I'm coming here to explore if indeed we need to allocate time on the Coq Dune Windows build in case it doesn't work properly.
In theory, there should not be any problem, but we need to test.
@Michael Soegtrop , can you provide more information on what the concrete testing setup is?
Likely time to close https://github.com/coq/coq/issues/9199 too
Ali Caglayan (Apr 06 2022 at 20:56):What is the standard way to install dune for windows? I can only find things about cygwin
Ali Caglayan (Apr 06 2022 at 21:44):For installing OCaml on Windows, this seems to be the recommendation: https://fdopen.github.io/opam-repository-mingw/installation/
Ali Caglayan (Apr 06 2022 at 21:44):But that says it is being discontinued, so I am not sure what you are supposed to do after that.
Ali Caglayan (Apr 06 2022 at 21:53):This also seems to have just installed OCaml in cygwin.
Ali Caglayan (Apr 06 2022 at 21:53):How on earth do people install OCaml natively on windows?
Paolo Giarrusso (Apr 06 2022 at 22:00):downloading the Coq Platform binary installer I guess?
Ali Caglayan (Apr 06 2022 at 22:01):That definitely uses cygwin, I'm trying to test the claim that we can use dune natively on windows to build coq
Rudi Grinberg (Apr 06 2022 at 22:41):Ali Caglayan said:
What is the standard way to install dune for windows? I can only find things about cygwin
If you don't want to use opam, you can just clone the dune repo and then run the commands in the opam file manually
Rudi Grinberg (Apr 06 2022 at 22:43):The only requirement is a C toolchain and OCaml
Ali Caglayan (Apr 06 2022 at 23:00):Actually the cygwin installation can produce a dune.exe via cygwin opam which I can call from Windows command line after putting it in path.
Ali Caglayan (Apr 06 2022 at 23:15):OK as long as I setup the correct enviornment vars everything seems to be working
Ali Caglayan (Apr 06 2022 at 23:15):I had to set OCAMLLIB and add the bin dir to PATH
Rudi Grinberg (Apr 06 2022 at 23:15):Though note that it should work even without cygwin. I.e. with msvc and an OCaml binary
Rudi Grinberg (Apr 06 2022 at 23:34):In particular, it would be curious to see if Coq compiles with this OCaml distribution on Windows https://diskuv.gitlab.io/diskuv-ocaml/index.html
Which I think does not rely on Cygwin
Ali Caglayan (Apr 06 2022 at 23:45):It is a chunky download, lets see if it works tomorrow
Théo Zimmermann (Apr 07 2022 at 06:46):@Ali Caglayan note that the Coq Platform binary installer does not install cygwin. It used cygwin for building, yes, because it is needed for opam, but it creates native binaries and ships them.
Théo Zimmermann (Apr 07 2022 at 06:46):Esy is also said to work well on Windows (and shouldn't rely on cygwin), but I've never tested it.
Michael Soegtrop (Apr 07 2022 at 06:59):Ali Caglayan said:
That definitely uses cygwin, I'm trying to test the claim that we can use dune natively on windows to build coq
No, as Théo said - the installers don't include cygwin and also don't need it at run time - they just need it for building. They don't contain dune or ocamlc either (I think, would have to check for Windows), but that would be easy to change.
And yes, the main issue is that in theory OCaml and Dune should work fine on Windows, but in practice this might require some non obvious bootstrap process. I think it would be fine to use the Coq Platform (cygwin based) infrastructure to do this bootstrapping, that is just include dune and OCaml in Coq Platform - and maybe have an OCaml only pick.
The goal for Coq Platform is to have an installer which also sets up opam so that opam install works, but which does not require cygwin. This for sure would not work for all packages (some use autoconf), but it should work for most modern Coq packages users might want to install in addition - the hard stuff could be precompiled and shipped binary.
This is more or less my plan for the near future.
Michael Soegtrop (Apr 07 2022 at 07:05):Of course this plan also includes to replace the Windows opam distribution by fdopen with something else, since it is officially discontinued since summer last year.
Enrico Tassi (Apr 07 2022 at 07:19):We should also not forger that not all coq projects use dune for building, and even when they do they often include a makefile for extra targets. IMO having the scripts set up cygwin is a bonus for windows users which have to build their own projects.
Karl Palmskog (Apr 07 2022 at 07:25):in my view, the whole Coq community is in a transition period from Make to Dune, which will likely take several (2-4?) years, and during this time the best configuration for most projects is to have both a Make-based and a Dune-based build
Michael Soegtrop (Apr 07 2022 at 07:26):Sure, there will be a transition period where at least every advanced user needs the cygwin "compile from sources" thing or WSL2 and definitely the core of Coq Platform will require Cygwin to build for a while. But the goal should be that the number of users which need this is reduced over time. I think it is not unrealistic that a large number of packages a user might want to install on top of Coq Platform can be installed without cygwin quite soon.
Michael Soegtrop (Apr 07 2022 at 07:28):E.g. I think for the majority of lectures it should be possible to live without Cygwin and WSL2, since the lecturers usually have some control over the extra packages they need.
Karl Palmskog (Apr 07 2022 at 07:29):OK, here's a basic one: does MathComp even have preliminary Dune scripts? Do MC maintainers want to use Dune anytime soon? This would be a litmus test in my book.
Karl Palmskog (Apr 07 2022 at 07:31):what one can do from Platform side is to recommend Platform project maintainers to include Dune scripts, and possibly help them write those scripts (I've done this for CoqHammer and some others), and explain the benefits. But it's a long term project.
Enrico Tassi (Apr 07 2022 at 08:34):I think your view about the transition is too optimistic.
Many projects do have a dune file, but it is not tested nor used. The reason is that is was added by a PR by someone enthusiastic/knowledgeable about dune and that PR was kindly merged, but the author/maintainer has no clue on how to use it.
I did help a user the other day which was in this exact situation, he did not know how to update the dune file.
In the CI of Coq we don't even test the dune file of the downstream projects we track, we just test the coq_makefile targets.
About MC, there is a PR on MC adding dune support. It has been there for a while, re-evaluated over and over... But since the makefile works fine, nobody sees the switch as a priority worth investing time (in learning dune, I mean, clicking merge is easy).
Karl Palmskog (Apr 07 2022 at 08:37):wait, you're saying that 2-4 years transitioning to Dune is optimistic? What's the counterproposal, 10+ years?
Enrico Tassi (Apr 07 2022 at 08:37):And frankly, I don't even know what the future plans are. In Coq it seems we are going toward a coq_dune tool which generates the dune files/rules. I don't know if that will also be the future for Coq projects, and in that case it looks like the transition is going to be even longer.
Enrico Tassi (Apr 07 2022 at 08:38):What is optimistic is to consider it a transition. As in the same way there was no transition from C to C++, you just have both (but I'm pretty sure some people thought it would be a transition).
Karl Palmskog (Apr 07 2022 at 08:39):what I mean by transition is comparable to how OCaml people consider OCamlbuild and Dune: the former will still be around and continue to be maintained, but the community usage pattern and effort is shifting towards Dune
Karl Palmskog (Apr 07 2022 at 08:41):for example, I think the Coq refman and other documentation in the community should start to recommend Dune when it reaches 1.0 Coq support.
Enrico Tassi (Apr 07 2022 at 08:55):I think we should recommend building Coq projects with dune when:
Michael Soegtrop (Apr 07 2022 at 08:59):Well my main point is that nothing will happen at all if we don't test what is possible and what the issues are:
@Karl Palmskog : as I said the idea is to build the Coq Platform (including mathcomp) as is based on cygwin, but then provide in the installers dune + opam so that additional packages can be built on that basis without cygwin. I don't find this unrealistic.
Karl Palmskog (Apr 07 2022 at 08:59):from what Rudi has said, Coq support in Dune reaching 1.0 means that it's supported by Dune maintainers for the long term (i.e., old project build scripts will continue to work)
Karl Palmskog (Apr 07 2022 at 09:00):this has always been the bar for me to start to recommend Dune to mainstream Coq projects, rather than just saying people should add optional support for Dune when feasible to for example Coq-community projects.
Enrico Tassi (Apr 07 2022 at 09:06):Note that my worry about maintaining dune files was not only related to tool keeping backward compatibility, but also in the project maintainer to be able to maintain it. Of course you know how to do that, but how do I (lambda Coq user) learn it and what would that brings me? Unfortunately I don't think there are convincing answers to these questions as of today. That would be my bar for recommending a tool.
Ali Caglayan (Apr 07 2022 at 09:07):Documentation for dune is somewhat lacking, though on the Coq side we definitely could be writing more.
Dune works by generating rules under the hood that turn dependencies into targets.
Karl Palmskog (Apr 07 2022 at 09:09):@Enrico Tassi the situation with coq_makefile is not good either. For example, see the fundamental problems with parallelism in this PR due to Makefile design: https://github.com/coq/opam-coq-archive/pull/2146
Here is my fix, which uses Makefile.coq.local nontrivially (I don't think regular users can write this out-of-the-box): https://github.com/jwiegley/coq-haskell/pull/4
Ali Caglayan (Apr 07 2022 at 09:10):I think in order to recommend something, you have to have a convincing argument for why it is a good idea. Currently our solution is "go read through a somewhat maintained reference manual". If I didn't know anything about dune, that would be less than convincing.
Ali Caglayan (Apr 07 2022 at 09:11):I think that we should strive to tell people about using dune for their projects, but as Enrico says, I wouldn't go out of my way to claim it is the best and only way of building your project.
Ali Caglayan (Apr 07 2022 at 09:11):The Coq support in dune needs time to mature mostly.
Ali Caglayan (Apr 07 2022 at 09:12):If you have grievances about the state of Coq support in dune today, please open a talking point here: https://github.com/coq/coq/wiki/DuneWG-2022 We are organising a working group on dune soon, so it would be good to get peoples ideas / suggestions.
Karl Palmskog (Apr 07 2022 at 09:14):"Should all Coq projects use Dune" is in my opinion a really bad summary of what we discussed here
Ali Caglayan (Apr 07 2022 at 09:15):OK perhaps correct that to "should we recommend using dune to all coq projects".
Karl Palmskog (Apr 07 2022 at 09:17):the problem we considered is how people can build Coq projects without Cygwin or WSL on Windows, in particular after installing the Windows Platform. Dune is one possible solution.
Enrico Tassi (Apr 07 2022 at 09:17):@Karl Palmskog I agree make is difficult, and coq_makefile has bugs. But note that you could fix it without submitting a patch to make, which is already something, IMO ;-)
Enrico Tassi (Apr 07 2022 at 09:18):About that point, what is the problem having a cygwin around?
Karl Palmskog (Apr 07 2022 at 09:19):I don't think Michael said explicitly, but it's a big dependency and just installing it is a quite long process where a user has to make choices about packages to install
Ali Caglayan (Apr 07 2022 at 09:21):That was what I was trying to work out earlier in this thread. Why is cygwin needed? How much of ocaml + dune + coq works out of the box in windows?
Ali Caglayan (Apr 07 2022 at 09:21):The problem is, I am having some trouble understanding which box to look in for Windows.
Enrico Tassi (Apr 07 2022 at 09:32):Dunno how to feel about that. Git for windows comes with some shell stuff behind the scenes. If they did not manage to completely get rid of it, I think we are aiming too far.
Gaëtan Gilbert (Apr 07 2022 at 09:45):isn't git half written in shell though?
Karl Palmskog (Apr 07 2022 at 09:47):hmm, aren't people using TortoiseGit on Windows (pure C/C++?). Looks like it only requires git.exe.
Emilio Jesús Gallego Arias (Apr 07 2022 at 09:52):The reason I haven't pushed for more projects to use Dune is that still some key features are missing to support them well
Emilio Jesús Gallego Arias (Apr 07 2022 at 09:53):in particulat inter-scope composition
Emilio Jesús Gallego Arias (Apr 07 2022 at 09:53):Many of the other questions here have been already been answered and discussed at lenght, so I'd refer to these discussions / roadmap
Emilio Jesús Gallego Arias (Apr 07 2022 at 09:54):We keep hickjackign topics all the time tho XD
Emilio Jesús Gallego Arias (Apr 07 2022 at 09:56):See https://github.com/coq/coq/wiki/Coq-Call-2021-11-10
Karl Palmskog (Apr 07 2022 at 09:57):do you really consider this thread hijacked? The point about Cygwin and the Platform and Dune is pretty new to me
Enrico Tassi (Apr 07 2022 at 09:57):That call happened 13 months ago. Is it still actual?
Karl Palmskog (Apr 07 2022 at 09:59):are the "Dune for Coq itself" and "Dune in the Coq ecosystem" issues really tied as closely as one might think? It's certainly helpful to have Coq itself as a Dune customer for stdlib, but I think we can make decisions about using Dune in Windows for Platform projects, and for projects outside the Platform that can be built via the Platform, regardless of how the Dune-in-Coq plans proceed
Emilio Jesús Gallego Arias (Apr 07 2022 at 10:59):Enrico Tassi said:
That call happened 13 months ago. Is it still actual?
No it is not, I posted the wrong link sorry, ummm, that's a big problem, finding the notes
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:05):That's the good one I think https://github.com/coq/coq/wiki/Coq-Call-2021-11-10
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:05):but we didn't take the most detailed notes
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:15):The basic story for Coq and Dune is that indeed we are generating rules in two ways:
(coq.theory which thanks to upcoming and past events we hope to push to 1.0 soonBoth versions share code and should eventually be identical.
One blocking point which is not trivial is that indeed, there is a big mess in the Coq codebase w.r.t. some stuff such as multiple implementations of stuff like loadpath, bad surface vernac APIs, etc... It is hard to estimate how much effort thi would take the get in shape, but I'd say 1 full man year at least. So yeah, with current resources will take time.
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:16):Karl Palmskog said:
do you really consider this thread hijacked? The point about Cygwin and the Platform and Dune is pretty new to me
I considert his thread very hijacked as it was about building Coq with Windows, now we have expanded to much broader, unrelated topics, and I still don't know if @Michael Soegtrop bash problems are solved, I think they should and we can close the corresponding bug
Enrico Tassi (Apr 07 2022 at 11:26):Emilio Jesús Gallego Arias said:
The basic story for Coq and Dune is that indeed we are generating rules in two ways:
- for users, with
(coq.theorywhich thanks to upcoming and past events we hope to push to 1.0 soon- for Coq, with coq-dune , as Ali said, that's just a way to control the way dune rules ourselves. We could also keep a private dune version for us, as proposed in some PR (which was shut down, but I'm still convinced was a good idea)
Both versions share code and should eventually be identical.
My understanding is that coq_dune would let us decouple the release of dune and the changes we do in Coq. That is a big plus. But I don't see how that would help for external projects using the coq.theory stanza. In particular the findlib patch (#15220) was problematic w.r.t. that, since we had to change one rule. Can coq_dune also be used by external projects to update/override the built in rules?
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:29):@Enrico Tassi if someone wants to package it, I'd be good. But I'd hope that users can be happy with (coq.theory) , and we have a workflow such as:
so they can adapt. The findlib patch was a bit special, but that's a good point in the sense of how often we expect to have such large-impacting changes to happen.
At least we have improved the dune bus factor quite a bit thanks to the winter hackathon, and also the upcoming dune hackkathon should greatly help with that.
Enrico Tassi (Apr 07 2022 at 11:35):I don't think it is a matter of how often. It will, for sure, happen again. So it would be nice telling users to run "coq_dune; dune build" when their dune is too old. A bit like re-running coq_makefile when they upgrade Coq.
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:38):That's one choice, other option is to tell users "Coq 8.20 require Dune 3.3.1"
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:38):There is overhead in maintaining coq_dune
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:38):at some point Dune will allow us to unify both thru the plugin API
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:39):Enrico Tassi said:
It will, for sure, happen again.
What would be an example of that?
Ali Caglayan (Apr 07 2022 at 11:45):Emilio Jesús Gallego Arias said:
at some point Dune will allow us to unify both thru the plugin API
*In the far future
Enrico Tassi (Apr 07 2022 at 11:51):For example, I hope one day we will kill .glob and .aux, and store that data elsewhere, partially in the .vo. Even this stupid change will impact build rules. Another one is coqc -> coqc + coq_native. Maybe it already happened, but it is another example of how things may change. A last one, hard to summarize here, is that Extraction should become just an annotation to be honored by a coq_extraction tool to run on the .vo (not unlike coq_native), it makes no sense it is a vernacular command akin to Inductive or Module. That would also change the compilation chain a little.
Enrico Tassi (Apr 07 2022 at 11:52):Another example is the coqdep thing, from a .v -> .v.d to a *.v -> all.d, again it changes the rules of the game.
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:53):These are good examples thanks; yeah, these should be easy for Dune \ge 3.0 as we can detect the coq version, the way coq_dune works is that it should allow porting one to other very easily
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:53):Enrico Tassi said:
Another example is the coqdep thing, from a .v -> .v.d to a *.v -> all.d, again it changes the rules of the game.
That's a bit orthogonal, both strategies work today
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:54):After the recent patch to coqdep rules in dune, there is little incentive anymore for that one tho.
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:54):but yes we will implement it, but likely support both schemes
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:55):To be more concrete, I plan to vendor coq_dune in dune
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:55):so @Ali Caglayan point about the far future should not be so far
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:56):so if we are careful, we can just bump the vendored lib
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:56):I am not interested in maintaining coq_dune as something exposed to users, but if someone wants, go ahead!
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:56):there are many other issues in maintaining such a tool, such as versioning of the language, etc...
Emilio Jesús Gallego Arias (Apr 07 2022 at 11:56):that Dune takes care and I don't want to duplicate
Paolo Giarrusso (Apr 07 2022 at 14:08):I didn’t read everything, but shouldn’t the platform just include cygwin in all configuration? I haven’t seen an upside of excluding cygwin, and the only one I can imagine (download size) doesn’t seem so compelling…
Paolo Giarrusso (Apr 07 2022 at 14:10):If using cygwin is annoying (which is likely!), the platform should make this unnecessary as much as possible, but still include cygwin.
Paolo Giarrusso (Apr 07 2022 at 14:12):At least until some appropriate litmus test is passed, but it seems most of us agree we’re not there.
Paolo Giarrusso (Apr 07 2022 at 14:16):(reads up) regarding the choices in installing cygwin, maybe the platform should have an advanced option to disable it, and by default install some appropriate choices of <enough cygwin packages> — say, enough to use coq_makefile output, or enough to build the platform, etc.
Théo Zimmermann (Apr 07 2022 at 14:16):It indeed used to be the case that Cygwin would seriously inflate the Platform size, but as Michael mentioned elsewhere, this isn't so true anymore (because the Platform has inflated a lot for other reasons).
Michael Soegtrop (Apr 08 2022 at 07:27):@Paolo Giarrusso : the main reason for not including cygwin is that it is huge and it would not be easy to maintain it for many users and to maintain an installer (short of running the cygwin installer and installing from sources - which we already have). I am looking for something simpler and I honestly don't see the need for this huge complexity.
Michael Soegtrop (Apr 08 2022 at 07:37):Emilio Jesús Gallego Arias said:
I considert his thread very hijacked as it was about building Coq with Windows, now we have expanded to much broader, unrelated topics, and I still don't know if Michael Soegtrop bash problems are solved, I think they should and we can close the corresponding bug
I don't know. My main question was "what should work". I would recap the answers with "we are not aware of any issues but also not aware of anybody who ever tried it". I deduced the second part from the rather thin answers on how one would install dune on Windows.
So I still think it would make sense that a few experts (say a dune expert, an opam expert and me) sit together, discuss this and see what is possible and what not and a plan on how to get the holes filled. I can also do this alone, but it would just be much faster with a bit of team work and I have not so much spare time left with managing Coq Platform.
Michael Soegtrop (Apr 08 2022 at 07:40):Btw.: I am following up on (https://github.com/coq/platform/issues/11). "Adding dune" would require that it runs with the installers on all platforms Coq Platform supports. Otherwise adding a build tool like dune wouldn't make sense.
Last updated: Oct 13 2024 at 01:02 UTC