Bas Spitters (Jan 04 2021 at 21:22): Bas Spitters (Jan 04 2021 at 21:22):Is lean's nix support better than Coq's?
Simon Hudon (Jan 04 2021 at 22:48):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
Cyril Cohen (Jan 05 2021 at 00:16):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.
Cyril Cohen (Jan 05 2021 at 00:20):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...
Paolo Giarrusso (Jan 05 2021 at 00:21):so if you don't have time to learn Nix you can't use Lean either? That's fun
Simon Hudon (Jan 05 2021 at 02:37):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.
Simon Hudon (Jan 05 2021 at 02:41):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
Théo Zimmermann (Jan 05 2021 at 08:37):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).
Karl Palmskog (Jan 05 2021 at 08:46):many, many Nix packages in unstable are severely out of date, and it seems to be a quite slow process to get packages updated.
Karl Palmskog (Jan 05 2021 at 08:47):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
Enrico Tassi (Jan 05 2021 at 09:25):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).
Enrico Tassi (Jan 05 2021 at 09:28):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.
Théo Zimmermann (Jan 05 2021 at 09:31):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.
Théo Zimmermann (Jan 05 2021 at 09:32):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.
Théo Zimmermann (Jan 05 2021 at 09:33):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.
Enrico Tassi (Jan 05 2021 at 09:36):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?
Enrico Tassi (Jan 05 2021 at 09:36):(for the projects not using the template, they could submit 2 files handwritten)
Théo Zimmermann (Jan 05 2021 at 09:38):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).
Karl Palmskog (Jan 05 2021 at 09:39):@Théo Zimmermann so "package with Nix" here means: (1) tarball/archive with default.nix or (2) git repo with default.nix?
Théo Zimmermann (Jan 05 2021 at 09:41):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?
Enrico Tassi (Jan 05 2021 at 09:42):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
Karl Palmskog (Jan 05 2021 at 09:42):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?
Théo Zimmermann (Jan 05 2021 at 09:43):Karl Palmskog said:
OK, so Nix packages would only be for actual tags on GitHub? Not for equivalents of
extra-devpackages?
The infrastructure put in place by Cyril also allows an equivalent of extra-dev.
Théo Zimmermann (Jan 05 2021 at 09:45):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.
Karl Palmskog (Jan 05 2021 at 09:45):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?
Théo Zimmermann (Jan 05 2021 at 09:46):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.
Théo Zimmermann (Jan 05 2021 at 09:47):In particular, when you talk about calling dune multiple times, you are in fact talking about multi-packages repositories, right?
Karl Palmskog (Jan 05 2021 at 09:47):yes
Théo Zimmermann (Jan 05 2021 at 09:47):Then the multi-package nature of a repository should be reflected in having several Nix derivations, just like you have several opam files.
Théo Zimmermann (Jan 05 2021 at 09:48):And thus, that use case should eventually get properly supported.
Karl Palmskog (Jan 05 2021 at 09:48):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
Théo Zimmermann (Jan 05 2021 at 09:49):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.
Karl Palmskog (Jan 05 2021 at 09:50):how are even "multiple derivations" organized? default1.nix, default2.nix?
Théo Zimmermann (Jan 05 2021 at 09:52):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:
Enrico Tassi (Jan 05 2021 at 09:53):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)
Théo Zimmermann (Jan 05 2021 at 09:54):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.
Théo Zimmermann (Jan 05 2021 at 09:55):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.
Théo Zimmermann (Jan 05 2021 at 09:55):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.
Enrico Tassi (Jan 05 2021 at 09:56):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.
Théo Zimmermann (Jan 05 2021 at 09:57):True. I think nixpkgs's CI is much more flexible but I don't master it enough right now to properly discuss it.
Enrico Tassi (Jan 05 2021 at 10:06):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]
Théo Zimmermann (Jan 05 2021 at 10:07):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:
Karl Palmskog (Jan 05 2021 at 10:09):yeah what the heck is the deal with Alpine Linux? seems to be the bane of nearly all opam-repository PRs
Karl Palmskog (Jan 05 2021 at 10:10):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)
Enrico Tassi (Jan 05 2021 at 10:10):I'm pretty sure they don't test s a distro that claims time from busybox is actually an implementation of gnu time. ;-)
Enrico Tassi (Jan 05 2021 at 10:12):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.
Karl Palmskog (Jan 05 2021 at 10:13):hm, I was thinking, aren't there trust issues with the binary cache?
Karl Palmskog (Jan 05 2021 at 10:13):somehow it's reassuring to have my local Coq version build proofs that I want to trust
Enrico Tassi (Jan 05 2021 at 10:14):It's hashed no? And in a reproducible way so.
Enrico Tassi (Jan 05 2021 at 10:14):I guess you can rebuild from sources and obtain the same hash
Karl Palmskog (Jan 05 2021 at 10:15):sure, but I would probably want that to be the default
Théo Zimmermann (Jan 05 2021 at 10:19):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).
Théo Zimmermann (Jan 05 2021 at 10:20):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.
Karl Palmskog (Jan 05 2021 at 10:50):can we have MathComp devs sign their hashes of binary versions?
Théo Zimmermann (Jan 05 2021 at 14:55):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.
Enrico Tassi (Jan 05 2021 at 14:57):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).
Enrico Tassi (Jan 05 2021 at 15:00):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).
Théo Zimmermann (Jan 05 2021 at 15:03):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.
Théo Zimmermann (Jan 05 2021 at 15:04):It's fine that it is not for security-extremists like Karl. You are not forced to use it ;-)
Karl Palmskog (Jan 05 2021 at 15:05):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.
Théo Zimmermann (Jan 05 2021 at 15:17):I don't see the difference with Nix with the binary cache disabled.
Karl Palmskog (Jan 05 2021 at 15:30):I wasn't concerned with Nix in general, just the use of the binary cache as a trust issue
Paolo Giarrusso (Jan 05 2021 at 16:44):@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.
Karl Palmskog (Jan 05 2021 at 16:46):I think they mean w.r.t. system dependencies - no need to figure out depext...
Paolo Giarrusso (Jan 05 2021 at 16:47):for the casual user, opam install opam-depext seems easy?
Paolo Giarrusso (Jan 05 2021 at 16:47):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.
Théo Zimmermann (Jan 05 2021 at 16:47):No, I didn't mean this in particular. Everything about opam is just so complicated!
Théo Zimmermann (Jan 05 2021 at 16:48):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.
Théo Zimmermann (Jan 05 2021 at 16:49):As for flambda, we could also provide alternative package sets if it's deemed useful.
Paolo Giarrusso (Jan 05 2021 at 16:49):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 :-)
Paolo Giarrusso (Jan 05 2021 at 16:49):yes, in this case that's probably best
Théo Zimmermann (Jan 05 2021 at 16:50):For sure, advance usage of Nix is not easy. I was really talking about casual use (for pre-determined use cases).
Théo Zimmermann (Jan 05 2021 at 16:50):In fact, what's the hardest is not "advance usage" but grasping the concepts.
Paolo Giarrusso (Jan 05 2021 at 16:50):agreed! And this use case is "easy" in opam and hard in Nix.
Paolo Giarrusso (Jan 05 2021 at 16:50):Anyway, I just wanted the OCaml that Emilio (used to) recommend (with flambda enabled)
Paolo Giarrusso (Jan 05 2021 at 16:50):and a Coq without costs from native-compiler
Karl Palmskog (Jan 05 2021 at 16:51):I would argue the concept of a derivation is not easy to grasp
Théo Zimmermann (Jan 05 2021 at 16:51):Yep, I agree that Nix concepts are hard to grasp.
Paolo Giarrusso (Jan 05 2021 at 16:51):so I'll happily write an issue to make this one of the preconfigured option, but where? coq/coq?
Karl Palmskog (Jan 05 2021 at 16:51):and arguably anything beyond copy-pasting commands in Nix will require a lot upfront, even more than opam
Paolo Giarrusso (Jan 05 2021 at 16:52):yes, and bringing up OOP/AOP was not just a joke, tho I don't know enough to make that accurate.
Paolo Giarrusso (Jan 05 2021 at 17:01):Anyway, at least I filed https://github.com/coq/coq/issues/13717, HTH.
Théo Zimmermann (Jan 05 2021 at 17:02):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
Karl Palmskog (Jan 05 2021 at 17:05):aspect-oriented programming
Karl Palmskog (Jan 05 2021 at 17:06):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
Paolo Giarrusso (Jan 05 2021 at 17:08):AOP was an academic fad based on inheritance on steroids, where external modules can override functions that you hadn't set up for overriding.
Karl Palmskog (Jan 05 2021 at 17:08):[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.
Karl Palmskog (Jan 05 2021 at 17:09):AOP is still used for various purposes in the Java world
Paolo Giarrusso (Jan 05 2021 at 17:09):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.
Paolo Giarrusso (Jan 05 2021 at 17:11):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.
Karl Palmskog (Jan 05 2021 at 17:13):I didn't know we were debating... just saying the connection AOP-ITP has been made before
Paolo Giarrusso (Jan 05 2021 at 17:14):ah, I thought you were objecting to "academic fad", which is indeed oversimplified
Paolo Giarrusso (Jan 05 2021 at 17:15):anyway, sth like the issue I filed might be most of what I missed from Nix.
Karl Palmskog (Jan 05 2021 at 17:15):well, I was implicitly objecting to "was", but not very inflammatorily
Paolo Giarrusso (Jan 05 2021 at 19:21):re “nothing to do with OOP”: I see override and super only “mimic” OOP (https://stackoverflow.com/q/57449098/53974)
Karl Palmskog (Jan 05 2021 at 21:30):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) Sebastian Ullrich (Jan 08 2021 at 18:01):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.
Théo Zimmermann (Feb 28 2021 at 10:46):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/
Théo Zimmermann (Feb 28 2021 at 10:46):This should be of interest to you @Karl Palmskog
Last updated: May 31 2023 at 02:31 UTC