[coq] Restore compatibility with Coq < 8.10 for coq-lang < 0.3#4224
[coq] Restore compatibility with Coq < 8.10 for coq-lang < 0.3#4224ejgallego merged 1 commit intoocaml:mainfrom
Conversation
ejgallego
force-pushed
the
coq+native_tweaks_coq_version
branch
from
f1226b2 to
ee5adfb
Compare
|
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. |
I use them and encourage others to do so.
Sure. Just sync up with @bobot who was also interested in a 2.9 release |
rgrinberg
left a comment
rgrinberg
left a comment
There was a problem hiding this comment.
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.
|
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, |
Ok, added to the milestone thanks!
Sounds good, I can help with 2.9 in general if you folks needs a RM.
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 |
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 |
Yes indeed. We need to clean those up.
Sounds good |
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 <[email protected]>
ejgallego
force-pushed
the
coq+native_tweaks_coq_version
branch
from
ee5adfb to
53775cc
Compare
|
Umm, a problem with adding PRs to be backported to milestones is that once they land on 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... |
Isn't that because the milestone has only 1 PR attached to it, and hence merging the PR completes the milestone?
Sounds like a useful thing. |
I meant the PRs won't show up as "pending", milestone itself has to be manually closed IIANM. |
…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)
2 participants
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 [email protected]