Karl Palmskog (Oct 05 2021 at 15:55): Karl Palmskog (Oct 05 2021 at 15:55):Sorry if this has already been discussed, but is a platform release on Nix doable/feasible? Could I theoretically say: open a Nix shell and get me all packages from 2021.11?
Théo Zimmermann (Oct 05 2021 at 15:56):Thanks for raising the question. The answer is twofold.
Théo Zimmermann (Oct 05 2021 at 15:57):First, the platform scripts as they are do not work on NixOS (because opam depext doesn't work there). So currently, we have no way of getting the Coq platform on NixOS :confused:
Théo Zimmermann (Oct 05 2021 at 15:58):Second, it was anyway planned from the beginning that once a platform pick would be defined, it would be available for package maintainers to reuse in their packaging system, so this is what we should do in nixpkgs.
Karl Palmskog (Oct 05 2021 at 15:59):ah, so "the Coq platform as currently defined" can't be directly used in Nix
Théo Zimmermann (Oct 05 2021 at 16:00):Indeed, though with Cyril's work, it has become trivial to support multiple versions of Coq packages in nixpkgs, so it's just about doing the work of getting through the list of Coq platform packages, making sure they are available in nixpkgs at this version, then bundling that together in a meta-package.
Théo Zimmermann (Oct 05 2021 at 16:02):I guess I could take care of doing this when 2021.09 is released (though if that's considered helpful, I could already start doing that for 2021.02).
Karl Palmskog (Oct 05 2021 at 16:04):ah, one more item to automate. Could it even make sense to abstract over opam at some point? (we define a more general package metadata format that generates opam and other forms)
Karl Palmskog (Oct 05 2021 at 16:05):if we could get the platform projects to "fully" adopt Dune for everything Coq or OCaml at some point when Dune-Coq 1.0 is out, that could probably go a long way
Théo Zimmermann (Oct 05 2021 at 16:12):Karl Palmskog said:
ah, one more item to automate. Could it even make sense to abstract over opam at some point? (we define a more general package metadata format that generates opam and other forms)
Yes, a pretty simple text format listing packages and their versions would probably be all what we need.
Théo Zimmermann (Oct 05 2021 at 16:13):Karl Palmskog said:
if we could get the platform projects to "fully" adopt Dune for everything Coq or OCaml at some point when Dune-Coq 1.0 is out, that could probably go a long way
That's another option, and this one would be more aligned with what @Emilio Jesús Gallego Arias defends following his experiments (together with @Shachar Itzhaky) on the jsCoq "sort-of-platform" (which it would make sense to make converge with the Coq platform anyway, even if the package format was kept different).
Emilio Jesús Gallego Arias (Oct 05 2021 at 17:01):The use of Dune in jscoq is more of a convenience than a real attempt to do a package system; having a way to do a consistent complete build of the set of packages saves loads of time to us I think.
There is a lot of tension indeed between dune and opam, and that has been discussed a few times upstream.
Théo Zimmermann (Oct 05 2021 at 17:05):But you told me that you had a package format for jsCoq, right?
Emilio Jesús Gallego Arias (Oct 05 2021 at 18:07):It is more a library format I guess, in the sense it doesn't have meta-data like dependencies etc...
Emilio Jesús Gallego Arias (Oct 05 2021 at 18:07):I think
Emilio Jesús Gallego Arias (Oct 05 2021 at 18:08):see here https://github.com/jscoq/jscoq/blob/v8.14/coq-jslib/build/project.ts#L176
Emilio Jesús Gallego Arias (Oct 05 2021 at 18:11):but indeed it is a bit of a hybrid,
Emilio Jesús Gallego Arias (Oct 05 2021 at 18:11):it creates a zip file which contains all the .vo plus the metadata to load them
Emilio Jesús Gallego Arias (Oct 05 2021 at 18:11):plus dep metadata so Require Import can automatically download the package
Emilio Jesús Gallego Arias (Oct 05 2021 at 18:13):so mainly it is lacking versioning
Shachar Itzhaky (Oct 05 2021 at 19:02):I'm going to adopt the term "sort-of-platform" as the official jsCoq slogan from now on
Michael Soegtrop (Oct 05 2021 at 19:42):I must admit I can't really contribute to the discussion because I don't know Nix. The next "platform" I plan to support is docker and after that we can also discuss Nix. The depext issue might not be that serious. On Cygwin I also install all required system dependencies upfront, because depext didn't always work on cygwin. Of cause the extensibility with additional packages suffers from that, but then not than many opam packages used in the Coq world require exotic system packages.
Ali Caglayan (Oct 06 2021 at 13:47):Is there planned opam support for nix?
Théo Zimmermann (Oct 06 2021 at 13:50):opam works on Nix, just not the external dependency feature.
Ali Caglayan (Oct 06 2021 at 13:53):Sorry let me rephrase that, is there any planned opam depext support for nix?
Théo Zimmermann (Oct 06 2021 at 14:01):I don't know, but I would expect there isn't much pressure from users given that many of them (including me) use Nix as a full alternative to opam.
Michael Soegtrop (Oct 06 2021 at 16:23):@Théo Zimmermann : can you elaborate on this a bit? Or maybe can you describe how you would envision Nix support in Coq Platform?
Théo Zimmermann (Oct 06 2021 at 16:58):Elaborate on what exactly?
Can you describe how you would envision Nix support in Coq Platform?
The simplest solution (at least to begin with) is what I wrote above:
it was anyway planned from the beginning that once a platform pick would be defined, it would be available for package maintainers to reuse in their packaging system, so this is what we should do in nixpkgs.
it's just about doing the work of getting through the list of Coq platform packages, making sure they are available in nixpkgs at this version, then bundling that together in a meta-package
Basically, this means a purely Nix-based Coq platform (as opposed to an opam-based one like in other systems).
Michael Soegtrop (Oct 06 2021 at 17:24):But I guess one could automatically create whatever information Nix needs from an opam based Coq Platform installation - similar how we do installers. Opam should have all required meta information.
Michael Soegtrop (Oct 06 2021 at 17:27):Elaborate on what exactly?
I meant on "Nix as a full alternative to opam".
Paolo Giarrusso (Oct 07 2021 at 01:23):https://github.com/timbertson/opam2nix-packages and https://github.com/timbertson/opam2nix exist (tho I got stuck with them early)
Paolo Giarrusso (Oct 07 2021 at 01:27):Oh right, @Cyril Cohen spent some time on it, but didn't get it to use the coq-released repository: https://github.com/timbertson/opam2nix/issues/50
Paolo Giarrusso (Oct 07 2021 at 01:30):Otherwise, this is a take on what you ask @Michael Soegtrop — create a Nix derivation from an Opam one.
Paolo Giarrusso (Oct 07 2021 at 01:31):I wouldn't expect that to be very good, since good Nix packages let you pick different settings... But I might be off-base and @Théo Zimmermann has more insight.
Michael Soegtrop (Oct 07 2021 at 07:06):@Paolo Giarrusso : yes somehow this is what I have in mind except that - as with the Windows installers - the "conversion" should be done by the maintainers and officially published.
Théo Zimmermann (Oct 07 2021 at 08:43):Approaches relying on a tool to automate the conversion between an ecosystem package format and Nix have been used and adopted in nixpkgs for the packages coming from several (large) ecosystems such as node.js / Ruby Gems / etc. But for smaller ecosystems such as OCaml and Coq, I'm not sure that they are worth. The work we have done with @Cyril Cohen has rather been to simplify (manually) packaging new Coq packages and to simplify the use of alternative versions. We have a CI (https://github.com/coq-community/coq-nix-toolbox/actions) that ensures that all the package sets that we provide (such as coqPackages_8_13) are fully compatible. These package sets are geared toward using the latest compatible versions of every package, but we could just as well provide say package sets (coq_platform_packages_2021_09) where packages are pinned to specific versions to correspond to the official platform releases; and meta-packages that would put them all in scope (coq_platform_2021_09) . IMHO this would represent significantly less effort to put that in place manually compared to what it would entail to automate the conversion.
Michael Soegtrop (Oct 07 2021 at 13:13):IMHO this would represent significantly less effort to put that in place manually compared to what it would entail to automate the conversion.
If this is so, fine. Automation can still be done if someone thinks it is worth it.
Last updated: Jun 03 2023 at 05:01 UTC