rocq: init at 9.0+rc1 #377439
rocq: init at 9.0+rc1 #377439
Conversation
nix-owners
bot
requested review from
roconnor,
Zimmi48,
thoughtpolice and
vbgl
|
@vbgl CI green both here and on coq-community/coq-nix-toolbox#318 There is definitely room for improvement (for instance by providing better support for writing the coq compatibility packages) but this is a first working version, enabling users to test that their rocq-only packages indeed compile without the coq compatibility shim. Please take your time if you want to review this one a bit more carefully and ask any question, this is not urgently needed. |
|
That's pretty long, can't we just make an alias so that we can use both? |
|
No. Auto-complete exists and is supported by all Nix commands. |
|
Of course, I'm not going to ask the same thing for |
|
Well, it's not consistent anyway. The thing currently called rocq is closer from the rocq-core opam package. Maybe we should rename it rocq-core and add a rocq-prover metapackage? |
|
Indeed, it would be much better to make it more consistent the way you propose! |
|
So let's rename to rocq-core and see in a further PR how we could get a rocq-prover metapackage (still a bit unclear to me but maybe it's just a matter of having something with |
|
|
||
| { lib, stdenv, fetchzip, fetchurl, writeText, pkg-config, gnumake42 | ||
| , customOCamlPackages ? null | ||
| , ocamlPackages_4_14 |
There was a problem hiding this comment.
Naïve question: would it be better to use the current version of OCaml, i.e., 5.2 (and maybe soon 5.3)? or is OCaml 4.14 the correct thing to use to compile Rocq as of today?
This question is both for the PR author and for any careful reader such as Théo.
There was a problem hiding this comment.
OCaml 5 has the following disadvantages:
- not native_compute
- small performance penalty
My understanding is that nixpkgs doesn't really support native_compute anyway so maybe we could switch to OCaml 5. No strong opinion here.
There was a problem hiding this comment.
small performance penalty
I'm unsure that this is still true with OCaml 5.2.
My understanding is that nixpkgs doesn't really support native_compute anyway so maybe we could switch to OCaml 5. No strong opinion here.
Indeed! Native compute users could still override the version of OCaml to use OCaml 4.14 instead.
There was a problem hiding this comment.
small performance penalty
I'm unsure that this is still true with OCaml 5.2.
My understanding is that it will "always" remain true for fundamental reasons. But I may be wrong.
github-actions
bot
added
the
8.has: maintainer-list (update)
Indeed, not needed. |
proux01
force-pushed
the
rocq
branch
2 times, most recently
from
fb18346 to
bffc16d
Compare
|
@vbgl thanks for the review, CI green both here and on coq-community/coq-nix-toolbox#318 |
| rocqPackages_9_0 = mkRocqPackages rocq-core_9_0; | ||
|
|
||
| rocqPackages = recurseIntoAttrs rocqPackages_9_0; | ||
| rocq-core = rocqPackages.rocq-core; |
There was a problem hiding this comment.
While I'm OK with only creating rocq-core in this PR and keeping rocq-prover for later, I don't think that we should expose at the top level a package with the name rocq-core. It should probably only be made available as rocqPackages.rocq-core. In the future, when we introduce a rocq-prover package, we can make this one available at top level.
There was a problem hiding this comment.
I still think it is useful to get easy access to rocq-core.
In any case, I think we should merge this rapidly, so as to be able to test things in CIs during the RC period (we still can't test compilation without coq compat shim yet). We can still improve the little details later.
There was a problem hiding this comment.
My point is that rocq-core is a bit of a strange name for something at top level.
|
@Zimmi48 Théo, we need your approval for merging. Thanks. |
| rocqPackages_9_0 = mkRocqPackages rocq-core_9_0; | ||
|
|
||
| rocqPackages = recurseIntoAttrs rocqPackages_9_0; | ||
| rocq-core = rocqPackages.rocq-core; |
There was a problem hiding this comment.
My point is that rocq-core is a bit of a strange name for something at top level.
|
Question: should some of the package descriptions be improved?
It seems like the Rocq Prover description could mention that it is the new name of the Coq proof assistant. Perhaps, having the I find it interesting BTW that |
Things done
nix.conf? (See Nix manual)sandbox = relaxedsandbox = truenix-shell -p nixpkgs-review --run "nixpkgs-review rev HEAD". Note: all changes have to be committed, also see nixpkgs-review usage./result/bin/)Add a 👍 reaction to pull requests you find important.