Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[coq] Restore compatibility with Coq < 8.10 for coq-lang < 0.3 #4224

Merged
merged 1 commit into from
Feb 14, 2021
Merged

[coq] Restore compatibility with Coq < 8.10 for coq-lang < 0.3 #4224

merged 1 commit into from
Feb 14, 2021

Conversation

ejgallego
Copy link
Collaborator

Fixes #4142.

Changes introduced in #3210 meant that Dune became incompatible with
Coq < 8.10 ; this was not intentional and it turns out we had Coq Dune
users in Coq 8.9 / 8.8.

Indeed (using coq 0.3) does require Coq >= 8.10, but when (using coq 0.2) is set, we should remain compatible with Coq 8.7-8.9.

Signed-off-by: Emilio Jesus Gallego Arias e+git@x80.org

@ejgallego ejgallego added the coq label Feb 14, 2021
@ejgallego
Copy link
Collaborator Author

I'd like to signal this PR for backporting to both 2.8 and 2.9 branches, but I dunno how to do so, milestones seem to be not used anymore?

In general, I think I'd like to backport 3/4 Coq PRs to a 2.9 release, if possible. I'd be happy to do the backporting myself once it is agreed I can proceed.

@rgrinberg
Copy link
Member

milestones seem to be not used anymore?

I use them and encourage others to do so.

In general, I think I'd like to backport 3/4 Coq PRs to a 2.9 release, if possible. I'd be happy to do the backporting myself once it is agreed I can proceed.

Sure. Just sync up with @bobot who was also interested in a 2.9 release

rgrinberg
rgrinberg approved these changes Feb 14, 2021
View reviewed changes
Copy link
Member

@rgrinberg rgrinberg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me. It's a shame that the error message for 0.3 and coq < 8.10 can't be made better, but this is still an improvement.

@ejgallego ejgallego added this to the 2.8 milestone Feb 14, 2021
@rgrinberg
Copy link
Member

We haven't used milestones for point releases yet, but I think you should be specifying the concrete point release where this should PR should go. So, 2.8.3 in this case.

@ejgallego
Copy link
Collaborator Author

I use them and encourage others to do so.

Ok, added to the milestone thanks!

Just sync up with @bobot who was also interested in a 2.9 release

Sounds good, I can help with 2.9 in general if you folks needs a RM.

Looks good to me. It's a shame that the error message for 0.3 and coq < 8.10 can't be made better, but this is still an improvement.

Would be great to add a way to get Coq version , then we could improve the error message, and add some other goodies. My original use case was to have a variable %{coq:version} to be used in rules, however I'm a bit wary of adding this if there are some cases [such as when building with Coq vendored] where this variable cannot be determined properly.

@ejgallego ejgallego modified the milestones: 2.8, 2.8.3 Feb 14, 2021
@ejgallego
Copy link
Collaborator Author

We haven't used milestones for point releases yet, but I think you should be specifying the concrete point release where this should PR should go. So, 2.8.3 in this case.

Updated thanks; should we close the other milestones in the list that are then not to be used?

Note that in this case you may want to directly create 2.9.0 instead of 2.9 and 3.0.0+beta1 etc...

@rgrinberg
Copy link
Member

Updated thanks; should we close the other milestones in the list that are then not to be used?

Yes indeed. We need to clean those up.

Note that in this case you may want to directly create 2.9.0 instead of 2.9 and 3.0.0+beta1 etc...

Sounds good

@ejgallego
[coq] Restore compatibility with Coq < 8.10 for coq-lang < 0.3
53775cc 
Fixes ocaml#4142.

Changes introduced in ocaml#3210 meant that Dune became incompatible with
Coq < 8.10 ; this was not intentional and it turns out we had Coq Dune
users in Coq 8.9 / 8.8.

Indeed `(using coq 0.3)` does require Coq >= 8.10, but when `(using
coq 0.2)` is set, we should remain compatible with Coq 8.7-8.9.

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
@ejgallego ejgallego merged commit 5654855 into ocaml:main Feb 14, 2021
@ejgallego ejgallego deleted the coq+native_tweaks_coq_version branch February 14, 2021 17:27
@ejgallego
Copy link
Collaborator Author

Umm, a problem with adding PRs to be backported to milestones is that once they land on main they won't show up anymore.

In Coq we use a project for this, plus some automation. So when a PR with a backported milestone is merged, it gets added to a project Column "to backport", then when actually backported it moved to the done part. However this requires the use of scripts for merging so the automation recognizes format etc...

@rgrinberg
Copy link
Member

Umm, a problem with adding PRs to be backported to milestones is that once they land on main they won't show up anymore.

Isn't that because the milestone has only 1 PR attached to it, and hence merging the PR completes the milestone?

In Coq we use a project for this, plus some automation. So when a PR with a backported milestone is merged, it gets added to a project Column "to backport", then when actually backported it moved to the done part. However this requires the use of scripts for merging so the automation recognizes format etc...

Sounds like a useful thing.

@ejgallego
Copy link
Collaborator Author

Isn't that because the milestone has only 1 PR attached to it, and hence merging the PR completes the milestone?

I meant the PRs won't show up as "pending", milestone itself has to be manually closed IIANM.

@rgrinberg rgrinberg mentioned this pull request Mar 7, 2021
Closed
rgrinberg added a commit to rgrinberg/opam-repository that referenced this pull request Mar 7, 2021
@rgrinberg
[new release] dune-build-info, dune, dune-configurator, dune-site, du…
26052da 
…ne-action-plugin, dune-private-libs and dune-glob (2.8.3)

CHANGES:

- Make `patdiff` show refined diffs (ocaml/dune#4257, fixes ocaml/dune#4254, @hakuch)

- Fixed a bug that could result in needless recompilation under Windows due to
  case differences in the result of `Sys.getcwd` (observed under `emacs`).
  (ocaml/dune#3966, @nojb).

- Restore compatibility with Coq < 8.10 for coq-lang < 0.3 , document
  that `(using coq 0.3)` does require Coq 8.10 at least (ocaml/dune#4224, fixes
  ocaml/dune#4142, @ejgallego)

- Add a META rule for 'compiler-libs.native-toplevel' (ocaml/dune#4175, @AltGr)

- No longer call `chmod` on symbolic links (fixes ocaml/dune#4195, @dannywillems)

- Dune no longer automatically create or edit `dune-project` files
  (ocaml/dune#4239, fixes ocaml/dune#4108, @jeremiedimino)

- Have `dune` communicate the location of the standard library directory to
  `merlin` (ocaml/dune#4211, fixes ocaml/dune#4188, @nojb)

- Workaround incorrect exception raised by Unix.utimes (OCaml PR#8857) in
  Path.touch on Windows (ocaml/dune#4223, @dra27)

- `dune ocaml-merlin` is now able to provide configuration for source files in
  the `_build` directory. (ocaml/dune#4274, @voodoos)

- Automatically delete left-over Merlin files when rebuilding for the first time
  a project previously built with Dune `<= 2.7`. (ocaml/dune#4261, @voodoos, @aalekseyev)

- Fix `ppx.exe` being compiled for the wrong target when cross-compiling
  (ocaml/dune#3751, fixes ocaml/dune#3698, @toots)

- `dune top` correctly escapes the generated toplevel directives, and make it
  easier for `dune top` to locate C stubs associated to concerned libraries.
  (ocaml/dune#4242, fixes ocaml/dune#4231, @nojb)

- Do not pass include directories containing native objects when compiling
  bytecode (ocaml/dune#4200, @nojb)
@Blaisorblade Blaisorblade mentioned this pull request May 1, 2021
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@rgrinberg rgrinberg rgrinberg approved these changes

@emillon emillon Awaiting requested review from emillon

@nojb nojb Awaiting requested review from nojb

Assignees
No one assigned
Labels
coq
Projects
Coq + Dune
Archived in project
Milestone
2.8.3
Development

Successfully merging this pull request may close these issues.

coqc: ondemand: no such file or directory
2 participants
@ejgallego @rgrinberg