Stream: Dune devs & users

Topic: Upcoming deprecation of `(coq lang)` < 0.8


view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Apr 21 2023 at 11:33):

it's restricted by what Coq supports

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Apr 21 2023 at 11:35):

the Platform has builds going back to Coq 8.12

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 11:36):

Yes I know, but what is the problem you are thinking of?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 11:39):

But indeed there is a bit of a migration to do.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 21 2023 at 12:06):

We could of course officially deprecate it in the doc.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Apr 21 2023 at 12:37):

warnings don't show up in opam builds unless you ask for them

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 12:50):

Ouch I mean "more annoying"

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 12:50):

Spanish / English woes

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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."

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 12:55):

But indeed hard to predict without testing.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 13:12):

You have the same problem with Coq versions, etc...

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 13:12):

OCaml versions....

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 13:17):

@Karl Palmskog what do you think?

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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")

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 13:26):

0.8 is officially 1.0 beta

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 13:26):

so yeah it is still not 1.0

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 13:51):

I also see zorns lemma, and a few others like gaia / hydra battles?

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Apr 21 2023 at 13:54):

Yes, anything using a multi-package repo greatly benefit from using Dune.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 14:01):

so adding a Dune upper bound seems like not a large restriction then

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 14:02):

right?

view this post on Zulip Karl Palmskog (Apr 21 2023 at 14:02):

sure, we have made sure that Dune deprecation impact is small in Coq-community

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 14:09):

in the opam file

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 14:09):

The deprecation impact should be 0 tho.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 14:09):

The eventual removal would have an impact.


Last updated: May 25 2024 at 19:02 UTC