Is lean's nix support better than Coq's?
The Lean Nix support has only just come out. I assume Coq's support is more mature and I expect there will be a few bumps on the Lean road
Coq support is using stable only features of nix, and is indeed working and stable.
Lean4 uses yet unreleased features of nix, and takes advantage of them (in a way I intended to do for Coq, when the features are release). Because of that, Lean4's use of nix is both more advanced and not yet suitable for the general public.
Moreover since Lean4 is built with nix in mind as its main "package manager", it means they do not have to hack around their way to support several installation procedures, and could rely on the fact compiled libraries are always in the nix store, which IMHO is a great invariant to rely on...
so if you don't have time to learn Nix you can't use Lean either? That's fun
Nix can be a bit scary but like the rest of the tools we use for programming languages and provers, we can have a simple set of instructions that lets a user invoke nix without becoming a proficient nix user.
The hope with the experiment is that it will be a simpler toolchain to use and maintain than what we currently use for Lean 3
For the casual user, Nix is certainly easier to use than opam! Fortunately for us, the work of Michael around the Coq platform resulted in easy-to-use scripts that wrap every call to opam. And relying on Nix means imposing the use of WSL on Windows (but it's not such a big deal nowadays).
many, many Nix packages in unstable are severely out of date, and it seems to be a quite slow process to get packages updated.
so I'm not sure we could work the same way (as with opam) with only Nix, without creating some Nix repo of our own
Karl Palmskog said:
so I'm not sure we could work the same way (as with opam) with only Nix, without creating some Nix repo of our own
At some point there was an idea of sharing a single source of metadata and generate opam/nix out of it (it could be opam itself I guess).
Théo Zimmermann said:
For the casual user, Nix is certainly easier to use than opam! Fortunately for us, the work of Michael around the Coq platform resulted in easy-to-use scripts that wrap every call to opam. And relying on Nix means imposing the use of WSL on Windows (but it's not such a big deal nowadays).
The platform is opam based, but the selection of packages is not really (we ask upstreams to tag/release what is in there). Having a script to take that list and run nix on it seems feasible to me (for the ones that prefer to use nix), proviso these versions are also available on nix.
Karl Palmskog said:
many, many Nix packages in unstable are severely out of date, and it seems to be a quite slow process to get packages updated.
The reason is that the updates are done by very few people on a needs basis. But Cyril has worked on infrastructure (https://github.com/NixOS/nixpkgs/pull/105877) that will allow: first, to install any version of a Coq package with Nix and second, to better integrate with an infrastructure to be set in the development repositories themselves. Then, we can expect automatic package updates (for projects relying on the coq-community templates) at the same point that we introduce it for the opam archive.
Having our own Nix overlay (or flake, which is the advanced feature used by Lean IIUC) is a possible option if we discover that relying on nixpkgs doesn't bring enough flexibility.
Enrico Tassi said:
Théo Zimmermann said:
For the casual user, Nix is certainly easier to use than opam! Fortunately for us, the work of Michael around the Coq platform resulted in easy-to-use scripts that wrap every call to opam. And relying on Nix means imposing the use of WSL on Windows (but it's not such a big deal nowadays).
The platform is opam based, but the selection of packages is not really (we ask upstreams to tag/release what is in there). Having a script to take that list and run nix on it seems feasible to me (for the ones that prefer to use nix), proviso these versions are also available on nix.
Absolutely! Here, I was just highlighting the fact that opam is not beginner-friendly and that the platform interactive script brings this beginner-friendliness.
About the templates, would it be possible to have a package "tag" just submitted to the opam-coq-archive and have both the opam and nix file be generated/tested and eventually merged? I mean, 1 place to submit a tag to, and two backend-archives?
(for the projects not using the template, they could submit 2 files handwritten)
I was rather thinking that once the repository maintainers tag (or release with the GitHub feature), then coqbot kicks in and opens the two corresponding PRs (on the opam archive and on nixpkgs).
@Théo Zimmermann so "package with Nix" here means: (1) tarball/archive with default.nix
or (2) git repo with default.nix
?
I'm not quite sure I understand your question, but the templates would generate Nix-specific files (one default.nix
at the root and helper files in a sub-directory) and CI would test these files so that once the project gets a release, it's a trivial operation to add the new version to nixpkgs. Does that answer your question?
Théo Zimmermann said:
I was rather thinking that once the repository maintainers tag (or release with the GitHub feature), then coqbot kicks in and opens the two corresponding PRs (on the opam archive and on nixpkgs).
This is a way to do it, but then one has 2 PRs and two reviews/reviewers... And it also entagnles tagging and packaging, which has both pros and cons
OK, so Nix packages would only be for actual tags on GitHub? Not for equivalents of extra-dev
packages that use version control repos directly?
Karl Palmskog said:
OK, so Nix packages would only be for actual tags on GitHub? Not for equivalents of
extra-dev
packages?
The infrastructure put in place by Cyril also allows an equivalent of extra-dev
.
There can also be a way to install directly from the dev repo (e.g. if the dependency list or build instructions have changed) similar to what is possible with opam.
from my limited experience, creating default.nix
when the basic template doesn't work is quite difficult, e.g., one has to invoke dune multiple times... that will still be a limitation, right?
Well, the current default.nix
was barely maintained so far and doesn't account for complex use cases, but it will definitely need to if we want to use the templates, e.g., for the main math-comp repo.
In particular, when you talk about calling dune
multiple times, you are in fact talking about multi-packages repositories, right?
yes
Then the multi-package nature of a repository should be reflected in having several Nix derivations, just like you have several opam files.
And thus, that use case should eventually get properly supported.
due to current limitations in Dune, the only way to build a multi-package Coq repo where one package depends on the other is to do "dune install" twice in the right order
Yes, for development it's a bit of a shame (and hopefully it will be resolved in the not too distant future) but for packaging it makes perfect sense to follow that scheme anyway.
how are even "multiple derivations" organized? default1.nix
, default2.nix
?
In the plan laid out by Cyril (and refined through discussions with Vincent and myself), the default.nix
file at the root will only be a convenience file. The proper derivations will be stored:
Is then a "coq specific" repository of derivations out of the plan? (I don't know how smooth it is to merge in the main repo)
Not out of the plan: as I said earlier, we decided to first continue to use the main repo and to consider having our own if it turns out to not be flexible enough.
We have pretty much control on what Coq-specific stuff we put in nixpkgs but the only limitation right now is that Vincent is the only committer in our group.
That being said, there are more Coq users (a bit further from the dev team) who are Nix committers as well and whom we could involve.
I believe also CI is important, I would not be happy to use the one of ocaml/opam for the coq repo of opam packages.
True. I think nixpkgs's CI is much more flexible but I don't master it enough right now to properly discuss it.
I guess I'm unhappy about "what" not how. [rant] I mean, 99% of my opam PRs fail on Alpine linux and at the same time I'm sure that 99% of OCaml users wouldn't care less of running their code on a (debatable choice of) embedded linux distro. I hope nix CI does a more sensible choice of "what" is worth testing and hence ask users to fix their packages on that scenario. [/rant]
Yes, nixpkgs is not that ambitious with respect to the platforms it targets. As for the distributions, well, it doesn't care, since the Nix experience is reproducible whatever the distro :victory:
yeah what the heck is the deal with Alpine Linux? seems to be the bane of nearly all opam-repository PRs
I guess the difference is that Nix is closed-off from the world, while the system bleeds more into opam (not obvious what the right design choice is)
I'm pretty sure they don't test s a distro that claims time
from busybox is actually an implementation of gnu time. ;-)
Anyway, to me the binary cache is what will make nix the way to go in the long run. So I'm very happy your guys are working on it.
hm, I was thinking, aren't there trust issues with the binary cache?
somehow it's reassuring to have my local Coq version build proofs that I want to trust
It's hashed no? And in a reproducible way so.
I guess you can rebuild from sources and obtain the same hash
sure, but I would probably want that to be the default
The default is to trust only the official binary cache, though you can decide to even not trust that but rebuilding the whole world is a bit heavy (and you anyway have to trust the initial bootstrap binaries).
To trust an additional binary cache, e.g. the one of Coq or of math-comp, you have to explicitly opt-in by adding a public key to your trusting base.
can we have MathComp devs sign their hashes of binary versions?
Not in the sense you probably imagine it. There is one (single) key for an entire binary cache. The current privileged approach is to let Cachix manage that key and to generate tokens which can be used as a secret variable in a CI service (and invalidated if it becomes necessary). Every build (not just releases) are uploaded to the cache so that you can benefit from this even if you are working on a dev branch.
I guess that if one provides an additional binary cache for mathcomp, then that one could be signed by a MC dev (I'm not suggesting that, just trying to understand the model).
FTR, it is the same in Debian, the developer signs the package on upload, then it is built and the result signed with a key specific to the release containing the package (possibly in between the machine building the package may sign it, and pass it to the archive, but no trace of this is left in the final product IIRC).
Enrico Tassi said:
I guess that if one provides an additional binary cache for mathcomp, then that one could be signed by a MC dev (I'm not suggesting that, just trying to understand the model).
I was describing how the math-comp binary cache works just above.
It's fine that it is not for security-extremists like Karl. You are not forced to use it ;-)
I'm not extremist in practice, but it seems the binary cache drops any possibility of being an extremist. At least in opam I know I am building an archive, and I know the checksum of that archive, and I can verify that the archive was built from a revision signed by someone.
I don't see the difference with Nix with the binary cache disabled.
I wasn't concerned with Nix in general, just the use of the binary cache as a trust issue
@Théo Zimmermann > For the casual user, Nix is certainly easier to use than opam!
Not to install a package but changing a version of a dependency.
I think they mean w.r.t. system dependencies - no need to figure out depext...
for the casual user, opam install opam-depext
seems easy?
choosing dependencies wasn't easy even for versions that are pre-configured, but getting packages for OCaml 4.07.1+flambda was outside my Nix budget.
No, I didn't mean this in particular. Everything about opam is just so complicated!
As often, what works best is what other people have configured for you before. Fortunately, Cyril's work is going to make selecting a specific version very easy.
As for flambda, we could also provide alternative package sets if it's deemed useful.
I'm not a fan of opam. But it doesn't require to use OOP/AOP against semi-documented APIs :-) I'm sure it can be done, not casually :-)
yes, in this case that's probably best
For sure, advance usage of Nix is not easy. I was really talking about casual use (for pre-determined use cases).
In fact, what's the hardest is not "advance usage" but grasping the concepts.
agreed! And this use case is "easy" in opam and hard in Nix.
Anyway, I just wanted the OCaml that Emilio (used to) recommend (with flambda enabled)
and a Coq without costs from native-compiler
I would argue the concept of a derivation is not easy to grasp
Yep, I agree that Nix concepts are hard to grasp.
so I'll happily write an issue to make this one of the preconfigured option, but where? coq/coq?
and arguably anything beyond copy-pasting commands in Nix will require a lot upfront, even more than opam
yes, and bringing up OOP/AOP was not just a joke, tho I don't know enough to make that accurate.
Anyway, at least I filed https://github.com/coq/coq/issues/13717, HTH.
Nix is a (weird) untyped functional language with a core notion of attribute sets. Nothing to do with OOP. I don't know what AOP means except https://fr.wikipedia.org/wiki/Appellation_d%27origine_prot%C3%A9g%C3%A9e
aspect-oriented programming
tactical theorem proving in Coq has been likened to "an extreme form of AOP" https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/mop.pdf
AOP was an academic fad based on inheritance on steroids, where external modules can override functions that you hadn't set up for overriding.
[Coq use being like AOP] is not A Good Thing, particularly for beginners. Scripts are unreadable by themselves, as one has no idea what the tactics are doing to the proof state, and the documentation for them is incomprehensible to the novice. The only thing that works is lots and lots of trial and error in an interactive environment, and I still couldn’t give a coherent general description of what some of the tactics I’ve used many times actually do, or how they differ from half a dozen apparently similar ones.
AOP is still used for various purposes in the Java world
The only link is that if foo
specifies that it wants to be built by OCaml 4.09, you can still write an expression that overrides foo
's choice.
I didn't want to open a debate on AOP, but my PhD supervisor used to work on it; the original problem is still there, but AspectJ's not a good solution to that. It is indeed used for binary instrumentation, but that doesn't achieve AOP's intended goal.
I didn't know we were debating... just saying the connection AOP-ITP has been made before
ah, I thought you were objecting to "academic fad", which is indeed oversimplified
anyway, sth like the issue I filed might be most of what I missed from Nix.
well, I was implicitly objecting to "was", but not very inflammatorily
re “nothing to do with OOP”: I see override
and super
only “mimic” OOP (https://stackoverflow.com/q/57449098/53974)
https://twitter.com/ammkrn/status/1331587114706866177
@derKha It finally makes sense, nix is the work of time travelers. An idea from 2030 where you compose bash (1989) scripts using a homebrew language that feels like its from the 1960s, by following the documentation (which will be good in 21xx).
- CB (@ammkrn)Hi folks, person pushing Nix in Lean here. I'm loving the discussion and learning about use of Nix for Coq, just wanted to clarify that
Paolo Giarrusso said:
so if you don't have time to learn Nix you can't use Lean either? That's fun
is not true at all, no more than for Coq. If you take a look at Setting Up Lean, it should be clear that the "basic" setup (which I suppose is only a slightly weaker name than "default setup") is fully supported and not going anywhere anytime soon.
Karl Palmskog said:
hm, I was thinking, aren't there trust issues with the binary cache?
Trustix: Distributed trust and reproducibility tracking for binary caches
https://www.tweag.io/blog/2020-12-16-trustix-announcement/
This should be of interest to you @Karl Palmskog
Last updated: May 31 2023 at 02:31 UTC