dune: bump to 3.8 #79
Conversation
There was a problem hiding this comment.
@Alizter Thank you for the PR. I recently became the maintainer of multinomials and I'm taking a look at old PRs. Would you mind rebasing and updating (if needed) the PR? I don't know how to write a dune configuration but I can test it.
|
@pi8027 If you are interested, I can also set it up so that Dune generates the .opam file from package bounds set in dune-project. |
|
You also probably don't need the configure script any longer. |
Signed-off-by: Ali Caglayan <[email protected]>
|
@Alizter What is the advantage of that approach compared to coq-community templates? (I didn't even know it was possible to generate .opam file using Dune. As a maintainer, I rather don't want to depend too much on a tool I'm not familiar with.) |
|
There is currently no strong advantage apart from not having to edit an opam file by hand, which can lead to syntax errors. In the future, Dune will be able to build package dependencies of projects, allowing for Dune to be the only dependency needed to build this package. That is still some time off, so I'll just drop what the dune-project file will probably look like: This can be used in the future as a starting point, when Dune might be more useful here. Only the |
|
I've rebased, two questions:
|
|
Concerning the template you inserted above, it should be used with caution: you miss-spelled the mail address of Pierre-Yves, but moreover, I thought it had been agreed that Pierre-Yves was not maintainer anymore. |
|
@ybertot That's fine, it can be updated as needed. I just wanted to demonstrate which structural elements would be needed. I've corrected the typo (sorry). The information is just what I read from the opam file. I'm being agnostic to the actual relevancy of the information contained within. |
|
I'll try to resolve the build errors locally. It seems something changed since I posted the PR which I will need to understand. |
If I generate the .opam file using the coq-community templates, I'm not going to edit the .opam file by hand. (Well, it would be possible to trigger a syntax error by writing broken version constraints, but that unlikely happens.)
They are also suppressed in MathComp. So I think that the answer is yes.
That would be a question to @erikmd. |
That's fine, let's forget about this for now. |
|
I attempted to fix CI but it did not work. The invocations of |
|
Rather than -R Dune is using -Q, which I think is fine. In my unfinished attempt, I added the elpi library and plugin to the Here is what I am using: The command Dune is attempting to run is: giving me the following error: I can reproduce when running that command (which I took from _build/log). When I remove -boot, Coq compiles. So something is interacting weirdly with findlib plugin loading in Coq and the -boot flag. |
|
I think @Alizter 's problem is due to Coq / CoqDune not supporting his hybrid setup where ocamlfind doesn't come from OPAM (but the rest of OCaml deps do) For the CI here, I think what is happening is simpler, are you sure the new Certainly it seems like the output corresponds to the old dune file. |
|
@ejgallego Thanks. I fixed the CI issue. @Alizter Do we agree to merge this as is and open another PR to see if we can remove the configure script? |
|
@pi8027 I'm happy with it if you are. Let's make sure the CI is happy too. |
|
BTW, we probably need to fix the version constraint on |
|
Yes @pi8027, another thing that we wouldn't need to worry about if we generated. Adding >= 3.8 should be sufficient. |
|
To be clear, I won't use Dune to generate stuff unless I see a significant advantage over the coq-community templates. Most MathComp-related packages use the coq-community templates for that purpose. So, the coq-community templates have an advantage over Dune that it is easier for us to maintain. In general, I would only accept patches I (or other MathComp devs) can maintain. That also applies to the removal of the configure script. |
|
@pi8027 That's fine, I was only mentioning that in passing. The configure script, AFAIU is a way to get around an issue with older versions of Dune where you would have to state the native rules explicitly. Now this is done automatically by Dune, therefore it might be time to remove it. (Doesn't have to be this PR I suppose). cc @proux01 who I believe I discussed this issue with a few years ago. |
|
I can confirm that the configure script was only a hack to workaround the deficiencies of dune < 3.8, so requiring dune >= 3.8 means removing the configure script (and moving src/dune.in to src/dune). To be clear I'am in favor of either moving to dune >= 3.8 or moving back to coq_makefile, either solution would be an improvement over the current hackish status. |
|
(but in case of moving back to coq_makefile, please notify me because I would need to update the Nix package or CI would be broken) |
|
I also don't know the reason behind the use of Dune, and I won't go back to coq_makefile without knowing the reason. (Such a change can complicate the reviewing and merging process, and I suggest not doing that in this PR.) 3485ea6 |
|
I guess only @strub might remember the reason for the use of Dune here. |
There was a problem hiding this comment.
Please choose whether
- to not remove the configure script, not remove the comment line in
dune.in, and not movedune.intodune, or - to remove the configure script, remove the comment line in
dune.in, and movedune.intodune.
(The last commit f22432e does the second item but does not do the rest. Therefore, I'm not accepting the patch.)
In the latter case, approval from someone who worked on this configure script (Érik or Pierre ?) is required.
|
I vote for 2 (and thereby approve it). |
|
@Alizter I think you need to remove |
|
@pi8027 Yes sorry, I pushed then realised, but I was in the middle of setting up my opam switch again. I will push a tested fix shortly. |
Signed-off-by: Ali Caglayan <[email protected]>
|
@pi8027 This should be ready now. Hopefully the CI agrees. |
|
Thanks a lot @Alizter for finally fixing this ! |
Broken in nixpkgs since math-comp/multinomials#79
Dune 3.8 has support for composing with installed Coq theories. So here is an updated dune file. The native rules are also chosen according to how coqc was configured so no need to explicitly enable it.