Stream: Dune devs & users

Topic: Migrating Coq Community to dune-coq 0.7


view this post on Zulip Paolo Giarrusso (Aug 19 2023 at 11:01):

Coq-community is still using dune-coq 0.3. While concerns about 0.8 have been discussed _exhaustively_ and they're off-topic here,
in https://coq.zulipchat.com/#narrow/stream/344515-Hydras-.26-Co.2E-universe/topic/Library.20for.20countability.3F/near/385733001 I convinced @Karl Palmskog to look into 0.7, to gain support for composition of ~theories~ projects (from 0.4) and other small fixes. Is there any other pitfall to keep in mind? Cc @Rodolphe Lepigre as well.

view this post on Zulip Karl Palmskog (Aug 19 2023 at 11:01):

thanks, if Rodolphe gives a thumbs-up and my testing works out, I think we will try to upgrade all Coq-community projects to dune-coq 0.7

view this post on Zulip Rodolphe Lepigre (Aug 19 2023 at 12:08):

I would definitely move as much code as possible to (coq lang 0.7). As far as I know, this version is a strict improvement over previous versions, and there is no significant change of semantics (unlike with 0.8), only new features and bug fixes.

view this post on Zulip Karl Palmskog (Aug 19 2023 at 12:55):

OK, we have a problem with 0.7. Some projects are using the Nix toolbox and have useDune2 = true;, while Dune-Coq 0.7 requires Dune 3.7 or later. Could perhaps @Théo Zimmermann give advice? Is it as simple as changing Nix toolbox config?

Example of failing build: https://github.com/coq-community/huffman/actions/runs/5911496468/job/16034057584
My test PR: https://github.com/coq-community/huffman/pull/50

view this post on Zulip Théo Zimmermann (Aug 19 2023 at 12:57):

You probably can replace with useDune = true;. Perhaps, you need to update to the latest version of the toolbox for this to work.

view this post on Zulip Karl Palmskog (Aug 19 2023 at 13:04):

@Théo Zimmermann how do I do the "latest version update" for the toolbox for a project like Huffman? There's nothing obvious in the Nix toolbox readme

view this post on Zulip Théo Zimmermann (Aug 19 2023 at 13:07):

Agreed that the doc is still very unsatisfying. To update, you need to run the updateNixToolBox command inside nix-shell --arg do-nothing true. It looks like this is even missing from the README in fact. If you do not have a nix command at hand, I can take care of it.

view this post on Zulip Karl Palmskog (Aug 19 2023 at 13:08):

would be grateful if you took care of it, but since I have nix command now, would be useful to replicate locally. But is the exact commands then the following?

nix-shell --arg do-nothing true # in huffman root
updateNixToolBox

view this post on Zulip Théo Zimmermann (Aug 19 2023 at 13:10):

Yes.

view this post on Zulip Théo Zimmermann (Aug 19 2023 at 13:11):

In most cases, this should only update the pinned commit in the .nix/coq-nix-toolbox.nix file BTW.

view this post on Zulip Théo Zimmermann (Aug 19 2023 at 13:18):

It seemed like this fixed this error, but now there is a new one, relative to native compilation.

view this post on Zulip Karl Palmskog (Aug 19 2023 at 13:19):

I tried nix-shell --arg do-nothing true --run "genNixActions" locally, and there were a bunch of modifications to the Nix workflows in .github/workflows. Maybe the workflow defs are out of date? Or the native stuff is unrelated to that?

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

I think this is unrelated, but I'll commit these anyway (good point noticing them).

view this post on Zulip Théo Zimmermann (Aug 19 2023 at 13:22):

It looks to me like the issue is that previously Dune wasn't trying to do the native compilation, and now it does, but the Coq stdlib was not native compiled.

view this post on Zulip Karl Palmskog (Aug 19 2023 at 13:23):

I guess we can turn off native compilation in the dune project config, but maybe not the best place to solve the problem

view this post on Zulip Karl Palmskog (Aug 19 2023 at 13:26):

hmm, apparently in Dune-Coq 0.7 it's (seemingly) not possible to tell Dune to not use native, if Coq itself uses native

view this post on Zulip Rodolphe Lepigre (Aug 19 2023 at 13:27):

I think you can do (mode vo) in theories.

view this post on Zulip Rodolphe Lepigre (Aug 19 2023 at 13:28):

The setup you seem to run seems weird though: do I understand correctly that you have Coq with native compilation enabled, but a standard library that only has vo files?

view this post on Zulip Théo Zimmermann (Aug 19 2023 at 13:28):

I didn't think that Coq had native compilation enabled. I'll look into this.

view this post on Zulip Karl Palmskog (Aug 19 2023 at 13:30):

at least in Dune-Coq 0.6, native has to be manually enabled, according to docs

view this post on Zulip Théo Zimmermann (Aug 19 2023 at 13:32):

The nixpkgs definition doesn't pass any configure option related to native compilation, but the default value changed to no in Coq 8.17.

view this post on Zulip Théo Zimmermann (Aug 19 2023 at 13:32):

Karl Palmskog said:

at least in Dune-Coq 0.6, native has to be manually enabled, according to docs

Yes, but starting from 0.7, it follows Coq's configuration, so it's not surprising that we see this error appearing.

view this post on Zulip Théo Zimmermann (Aug 19 2023 at 13:34):

Théo Zimmermann said:

The nixpkgs definition doesn't pass any configure option related to native compilation, but the default value changed to no in Coq 8.17.

In 8.13-8.16, it was set to ondemand, thus the stdlib was not precompiled, but the Dune doc says that this will trigger native compilation in Dune.

view this post on Zulip Théo Zimmermann (Aug 19 2023 at 13:35):

I wonder if this shouldn't be considered as a bug of Dune that the ondemand configuration triggers native compilation.

view this post on Zulip Théo Zimmermann (Aug 19 2023 at 13:36):

(Probably unnoticed because nowadays, everyone is set to yes or no, and ondemand is not used, at least in the opam world.)

view this post on Zulip Théo Zimmermann (Aug 19 2023 at 13:36):

Rodolphe Lepigre said:

The setup you seem to run seems weird though: do I understand correctly that you have Coq with native compilation enabled, but a standard library that only has vo files?

Basically, this answers the question: Dune triggers native compilation in ondemand mode, but the stdlib is not precompiled in this case indeed.

view this post on Zulip Karl Palmskog (Aug 19 2023 at 13:42):

OK, so what do we do? Do we try the (mode vo) workaround? I only use Dune for CI in most projects, not for packaging.

view this post on Zulip Ali Caglayan (Aug 19 2023 at 13:47):

On demand always triggers native compilation. Otherwise people wouldn't be able to demand native compilation rules. If you don't want them set (mode vo).

view this post on Zulip Théo Zimmermann (Aug 19 2023 at 14:15):

@Ali Caglayan Isn't this a misunderstanding of what ondemand is supposed to mean? Cf. https://github.com/coq/ceps/blob/master/text/048-packaging-coq-native.md#readme and in particular: "option -native-compiler ondemand (which becomes the default when compiling coq manually) preserves the previous default behavior (modulo the stdlib that is not precompiled anymore)."

view this post on Zulip Paolo Giarrusso (Aug 19 2023 at 15:04):

As an alternative, maybe you want dune-coq 0.6 , since 0.7 changes the behavior of native compilation

view this post on Zulip Karl Palmskog (Aug 19 2023 at 15:06):

I think this will have to be solved in Nix packaging anyway. But for Coq-community, I guess we can go for 0.6 in the meantime.

view this post on Zulip Paolo Giarrusso (Aug 19 2023 at 15:06):

@Théo Zimmermann IIRC, -native-compiler ondemand is anyway the worst of both worlds; is it possible that Nix packaging should follow opam packaging here?

view this post on Zulip Paolo Giarrusso (Aug 19 2023 at 15:14):

We had a CEP about this and I might misremember, but my personal recollection is that on-demand native compilation would be great if outputs were cached and reused, but that's lots of work that nobody signed up for. Without that, the other settings are better.

view this post on Zulip Paolo Giarrusso (Aug 19 2023 at 15:17):

(but I don't think we discussed that idea too much, given the required amount of work)

view this post on Zulip Karl Palmskog (Aug 19 2023 at 16:59):

OK 0.6 works fine with Nix and Dune, and it works with the env thing. Let's go there as first step. The 0.7 thing should probably lead to a Dune and/or Nix and/or Coq issue, and I'm not qualified to decide.

view this post on Zulip Karl Palmskog (Aug 19 2023 at 17:02):

it seems you're not using Nix internally at Bedrock then, or we would have likely found out these problems sooner...

view this post on Zulip Paolo Giarrusso (Aug 19 2023 at 19:23):

Yeah sorry, we're not using Nix or native-compute...

view this post on Zulip Paolo Giarrusso (Aug 19 2023 at 19:26):

Dune-wise, it seems dune is forcing ondemand to behave like yes. It could offer a global option for the opposite choice, but it might be simpler to change this in Nix — that'd be my preference since everything is moving away from building Coq with ondemand.

view this post on Zulip Paolo Giarrusso (Aug 19 2023 at 19:28):

But you might want to confirm with CEP48's authors, since that one's tricky and I might have lost track of relevant details.

view this post on Zulip Théo Zimmermann (Aug 20 2023 at 16:56):

Currently, the Nix package for Coq doesn't set any configure option related to native compilation. We can change it to set -native-compiler no for the moment. There was an (unfinished) attempt by Ali to apply a similar setup to the one in opam to nixpkgs (https://github.com/NixOS/nixpkgs/pull/224110), but there are some long-standing issues relating to using native compilation with Nix (https://github.com/NixOS/nixpkgs/issues/34657).

view this post on Zulip Théo Zimmermann (Aug 20 2023 at 17:05):

FWIW, this should be an easy fix, but I won't take care of it (at least not right now) because I'm on vacations.

view this post on Zulip Karl Palmskog (Aug 20 2023 at 17:11):

I also vote for -native-compiler no in Nix, I guess we can migrate to 0.7 in Coq-community when it happens

view this post on Zulip Ali Caglayan (Sep 04 2023 at 13:20):

Karl Palmskog said:

OK, we have a problem with 0.7. Some projects are using the Nix toolbox and have useDune2 = true;, while Dune-Coq 0.7 requires Dune 3.7 or later. Could perhaps Théo Zimmermann give advice? Is it as simple as changing Nix toolbox config?

Example of failing build: https://github.com/coq-community/huffman/actions/runs/5911496468/job/16034057584
My test PR: https://github.com/coq-community/huffman/pull/50

Rereading this discussion again: There is a vague effort in nixpkgs to remove dune2 entirely, so I would highly advise getting projects to drop dune2. If these are hard limitations I would like to know about them since Dune is supposed to be as backwards compatible as possible.

view this post on Zulip Théo Zimmermann (Sep 04 2023 at 14:23):

There is no known limitation whatsoever of any Coq project on Dune 2.

view this post on Zulip Ali Caglayan (Sep 04 2023 at 15:40):

Do you mean there is no reason for any Coq projects to use Dune 2 or that Dune 2 has no limitations for Coq projects?

view this post on Zulip Théo Zimmermann (Sep 04 2023 at 16:26):

There are no Coq projects that I know of that willingly depend on Dune 2 specifically. When there was a useDune2 = true thing, this was because the Nix definition hadn't been updated in a long time.

view this post on Zulip Karl Palmskog (Sep 04 2023 at 16:36):

pretty much everyone does "dune" {>= 2.5} or something higher (in particular, in Coq-community)


Last updated: May 25 2024 at 19:02 UTC