Emilio Jesús Gallego Arias (Apr 21 2023 at 11:09): Emilio Jesús Gallego Arias (Apr 21 2023 at 11:09):Hi all,
after the merge of the PR that makes Coq lang support detection of theories that have been installed globally, we are deprecating all previous build modes for Dune 3.8 .
That means that all Dune users are encouraged to port their developments to Dune 3.8 and (coq lang 0.8).
If for some reason that is not possible for you please let us know.
We expect that (coq lang 0.8) will eventually become (coq lang 1.0) , so indeed we hope we can keep supporting 0.8 for a long time.
Karl Palmskog (Apr 21 2023 at 11:22):note that there are packages like coq-mathcomp-word that are in the Platform and use (using coq 0.3). If deprecated means "will stop working soon", we'll have to add patches to packages (otherwise the Platform build breaks)
Emilio Jesús Gallego Arias (Apr 21 2023 at 11:25):How would the platform build break? It has control over the Dune version it uses right?
Karl Palmskog (Apr 21 2023 at 11:33):it's restricted by what Coq supports
Emilio Jesús Gallego Arias (Apr 21 2023 at 11:34):Yes, how is that a problem?
For the Coq Opam archive there will be some impact, but we evaluated it and it is quite small, but we will indeed add the right upper bound constraints, but for the platform I don't foresee any trouble.
Karl Palmskog (Apr 21 2023 at 11:35):the Platform has builds going back to Coq 8.12
Emilio Jesús Gallego Arias (Apr 21 2023 at 11:36):Yes I know, but what is the problem you are thinking of?
Karl Palmskog (Apr 21 2023 at 11:36):but for example, if Coq 8.18 drops Dune 3.6, and mathcomp-word doesn't do a new release, then you get breakage right?
Emilio Jesús Gallego Arias (Apr 21 2023 at 11:36):That'd be dropping Dune 3.8 or Dune 3.9 , at the very earliest, but yes
Emilio Jesús Gallego Arias (Apr 21 2023 at 11:37):In that case you'd need a release. I don't see Coq dropping Dune 3.8 any time soon tho.
Emilio Jesús Gallego Arias (Apr 21 2023 at 11:38):Coq still supports Dune 2.0 /.1 (we require a bit higher due to some other features and bugfixes related to opam support etc..., but the base rules would work with quite old dune versions)
Emilio Jesús Gallego Arias (Apr 21 2023 at 11:39):Once the platform moves to Dune 3.9 indeed all the packages there would require to be up to date to 0.8, but that's a very good thing.
But I don't see anything requiring the platform to move to 3.9 in the short / medium term.
Emilio Jesús Gallego Arias (Apr 21 2023 at 11:39):But indeed there is a bit of a migration to do.
Emilio Jesús Gallego Arias (Apr 21 2023 at 11:40):We have deprecated these modes for 3.8, not sure when we will remove them, certainly not before all packages have new releases using the (coq lang 0.8) build language version which is the candidate for 1.0 semantics
Emilio Jesús Gallego Arias (Apr 21 2023 at 11:41):Given how low the impact on the Coq Opam archive is, we are indeed hoping to remove older modes not too far in the future tho, but we will see.
Ali Caglayan (Apr 21 2023 at 12:04):Overall I'm not too certain deprecating old lang versions is something we want to do. If a package builds with an older version then I think its fine to keep it. The reason we would want to deprecate something is so that we can warn users that eventually newer versions of Dune will not support these older coq lang versions.
Ali Caglayan (Apr 21 2023 at 12:04):The thing with the deprecation message is that it just annoys people and gets ignored in the cases where it should matter.
Ali Caglayan (Apr 21 2023 at 12:05):If a user cares about their Dune version then it is likely they will use a newer version of Dune anyway.
Ali Caglayan (Apr 21 2023 at 12:06):By deprecating I mean spitting out a warning when they are used in 3.8. Currently we do no such warning.
Ali Caglayan (Apr 21 2023 at 12:06):We could of course officially deprecate it in the doc.
Emilio Jesús Gallego Arias (Apr 21 2023 at 12:35):Ali Caglayan said:
The reason we would want to deprecate something is so that we can warn users that eventually newer versions of Dune will not support these older coq lang versions.
Indeed, that's exactly the case here.
As I wrote in the PR, I'm unsure how a warning is more annoying that breaking your build entirely.
Karl Palmskog (Apr 21 2023 at 12:37):warnings don't show up in opam builds unless you ask for them
Emilio Jesús Gallego Arias (Apr 21 2023 at 12:38):Karl Palmskog said:
warnings don't show up in opam builds unless you ask for them
Yes I know, but what do you mean by pointing out this?
Karl Palmskog (Apr 21 2023 at 12:47):the point is that we can ignore warnings when we need to, so I'd say nearly anyone prefers them over breakage. This makes no sense at all to me:
I'm unsure how a warning is less annoying that breaking your build entirely.
Emilio Jesús Gallego Arias (Apr 21 2023 at 12:50):Ouch I mean "more annoying"
Emilio Jesús Gallego Arias (Apr 21 2023 at 12:50):Spanish / English woes
Emilio Jesús Gallego Arias (Apr 21 2023 at 12:51):Yes I agree. I'm unsure why Ali wants to skip the deprecation phase but certainly I don't want to.
Emilio Jesús Gallego Arias (Apr 21 2023 at 12:52):And I'm happy to extend the deprecation for a few Dune versions, tho given the advantages of (coq lang 0.8) I'd expect most users to migrate quickly.
Karl Palmskog (Apr 21 2023 at 12:53):if you want my input, I'd prefer there was 1.0 before deprecating anything. Now, there seems to be the off chance that 0.8 gets deprecated for 1.0 (which I think some people, including me, would find frustrating)
Emilio Jesús Gallego Arias (Apr 21 2023 at 12:55):As I wrote "We expect that (coq lang 0.8) will eventually become (coq lang 1.0) , so indeed we hope we can keep supporting 0.8 for a long time."
Emilio Jesús Gallego Arias (Apr 21 2023 at 12:55):But indeed hard to predict without testing.
Emilio Jesús Gallego Arias (Apr 21 2023 at 12:55):Delaying the deprecation could be done, however that also risks delaying testing of the 1.0 candidate which is 0.8
Emilio Jesús Gallego Arias (Apr 21 2023 at 12:56):The thing is that really all the users in < 0.8 need to migrate now, the current model is just broken
Ali Caglayan (Apr 21 2023 at 12:57):We don't plan to change anything with regards to install semantics between 0.8 and 1.0 btw.
Ali Caglayan (Apr 21 2023 at 12:58):It's just that at the moment, we have many cases in the code keeping compat for < 0.8. Ideally we would remove all of these.
Emilio Jesús Gallego Arias (Apr 21 2023 at 12:58):I can see how people would be frustrated when 0.8 gets deprecated (which it will)
Karl Palmskog (Apr 21 2023 at 13:00):@Ali Caglayan so here you see why I have both coq_makefile and Dune builds - coq_makefile always in the package based on tags
Ali Caglayan (Apr 21 2023 at 13:01):In the case of coqhammer nothing should change as it doesn't require any installed theories. Except maybe one file about mathcomp.
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:03):Emilio Jesús Gallego Arias said:
I can see how people would be frustrated when 0.8 gets deprecated (which it will)
however the alternatives may be even worse, imagine you get no warning, you stay on 0.5 for example, then when 1.0 is released, you discover that we didn't properly test your setup, so that's gonna be even more frustating IMHO.
Dune + Coq is still experimental (as marked in the manual) so indeed people adopting 0.x versions are exposed to some churn, no matter how much we try to minimize it. We should make it minimal tho as testing is really appreciated.
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:03):Karl Palmskog said:
Ali Caglayan so here you see why I have both coq_makefile and Dune builds - coq_makefile always in the package based on tags
Why ?
Karl Palmskog (Apr 21 2023 at 13:06):because it doesn't get deprecated. Dune is great in CI builds, but if I can't trust builds to work in the future, I have to look elsewhere for permanent artifacts. I'm sure you'll solve this for 1.0, but that's how it is now.
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:11):Yup in general it is hard to guarantee that builds will keep working in the future, but that's not a problem specific to Dune
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:12):You have the same problem with Coq versions, etc...
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:12):OCaml versions....
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:12):So I don't see how Dune is special, even coq_makefile could break again at some point in a future Coq release
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:17):@Karl Palmskog what do you think?
Karl Palmskog (Apr 21 2023 at 13:23):sure, anything can break, and so on, but if there's an effort by devs to ensure backwards compatibility, that's different to me than "deprecations happen"
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:24):We could keep compat with 0.x versions of the Coq language, but I'm unsure how useful that'd be
Karl Palmskog (Apr 21 2023 at 13:24):I'll continue using Dune in CI and so on, but probably only in tag-based packages after 1.0
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:25):As is done routinely for other packages, we will just add the right upper bound when we remove them, if we remove them.
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:26):Karl Palmskog said:
I'll continue using Dune in CI and so on, but probably only in tag-based packages after 1.0
Sure that seems like a safe choice.
Karl Palmskog (Apr 21 2023 at 13:26):but you can see how for someone who's looking for a backwards compatibility commitment, 0.3 and 0.8 is basically the same ("not 1.0")
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:26):0.8 is officially 1.0 beta
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:26):so yeah it is still not 1.0
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:26):if we find a serious problem it could be indeed deprecated, we hope not!
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:27):Karl Palmskog said:
but you can see how for someone who's looking for a backwards compatibility commitment, 0.3 and 0.8 is basically the same ("not 1.0")
That's a strange view as we have just made the statement that they are different
Ali Caglayan (Apr 21 2023 at 13:27):yeah but let's not confuse ourselves with deprecating 0.8 that won't come anytime soon. We are talking about deprecating < 0.8 here.
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:27):Not sure what part of "We expect that (coq lang 0.8) will eventually become (coq lang 1.0) , so indeed we hope we can keep supporting 0.8 for a long time." sounds confusing.
Karl Palmskog (Apr 21 2023 at 13:28):sure, there is an expectation, etc. etc., but the real reason to update is basically composition with installed
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:32):Karl Palmskog said:
sure, there is an expectation, etc. etc., but the real reason to update is basically composition with installed
Yup, the reason to update is to get support this, also to move to a supported library model.
We think it makes little sense to offer the < 0.8 model, as it is broken
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:33):but yeah if we find some reason we could. But for now that model is deprecated because we consider it broken.
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:33):If we remove it we will have to add a few upper bounds on dune
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:39):Actually @Karl Palmskog I see a few of the tagged packages in coq-opam archive from Coq Community are using dune not coq_makefile , is that a bug then?
Karl Palmskog (Apr 21 2023 at 13:46):there are some packages like stalmarck where the coq_makefile build was absolutely atrocious, so I purged it (plugin code depending on extracted code). It's a low-impact package anyway
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:51):I also see zorns lemma, and a few others like gaia / hydra battles?
Emilio Jesús Gallego Arias (Apr 21 2023 at 13:52):Actually it would have been of great help if all the packages in coq-opam-archive used coq_makefile indeed
Théo Zimmermann (Apr 21 2023 at 13:54):Yes, anything using a multi-package repo greatly benefit from using Dune.
Karl Palmskog (Apr 21 2023 at 13:55):the rule of thumb has been that we use Dune in packaging only when we really need it, like Hydras & Co. It's a monorepo as Théo suggests, not handled well by coq_makefile
Emilio Jesús Gallego Arias (Apr 21 2023 at 14:01):It seems that most of these packages are actually already using an upper bound for Coq
Emilio Jesús Gallego Arias (Apr 21 2023 at 14:01):so adding a Dune upper bound seems like not a large restriction then
Emilio Jesús Gallego Arias (Apr 21 2023 at 14:02):right?
Karl Palmskog (Apr 21 2023 at 14:02):sure, we have made sure that Dune deprecation impact is small in Coq-community
Karl Palmskog (Apr 21 2023 at 14:04):and anyway Théo or I could theoretically make new releases that fix a broken Dune-based package (should the maintainer not do it)
Emilio Jesús Gallego Arias (Apr 21 2023 at 14:09):For an eventual removal we don't need a new release but just an upper bound like dune < 3.11
Emilio Jesús Gallego Arias (Apr 21 2023 at 14:09):in the opam file
Emilio Jesús Gallego Arias (Apr 21 2023 at 14:09):The deprecation impact should be 0 tho.
Emilio Jesús Gallego Arias (Apr 21 2023 at 14:09):The eventual removal would have an impact.
Last updated: Oct 13 2024 at 01:02 UTC