coq_HEAD: Update to the latest commit #21822
Conversation
|
The value of the |
|
What should be a consistent way to name the |
|
Finally, what about something like |
|
I just checked from https://git-scm.com/docs/git-describe that the number represents the number of additional commits since the most recent tag. The prefix 'g' refers to git. Have yet to check how other vcs describe the version of their most recent commits. |
|
@vbgl how should I put a constraint on the ocaml version s.t. it is at least 4.02.1? |
This is simpler if it is up to the standard convention of each vcs (and each project's tags). |
|
What do you call a constraint? If you expect nix to solve such constraints then I don’t know. You can check the property you mention with |
|
I see, tho is it possible to specify something along the line of |
|
I think the only objection remaining for this PR is the versioning scheme, which as I stated, would be better to reuse the existing tag by the coq package maintainer (the number of extra commits rather than the timestamp). |
|
Let me rephrase: the version number should start by a digit; this is why I suggest to put a timestamp in front of the output of |
|
I see, it looks like there is one case e.g. |
|
alt: |
| csdpPatch = if csdp != null then '' | ||
| substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp" | ||
| substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true" | ||
| '' else ""; | ||
| ocaml = ocamlPackages_4_02.ocaml; |
There was a problem hiding this comment.
@vbgl I overrode the definition here so that there is no need to put an extra prefix ocamlPackages_4_02 in buildInputs. Plus, the version-specific statement is localized to only within the let clause. WDYT?
| in | ||
|
|
||
| stdenv.mkDerivation { | ||
| name = "coq-${version}"; | ||
|
|
||
| inherit coq-version; | ||
| inherit ocaml camlp5; | ||
| inherit ocaml findlib lablgtk camlp5; |
There was a problem hiding this comment.
What’s the purpose of this change?
There was a problem hiding this comment.
There are several ways to specify the scope (in all-packages.nix, in the let clause, or casted in inherit and buildInputs), I picked the let option because it is most localized within each packages nix file. If it were to be casted in inherit and buildInputs it'd be too verbose.
There was a problem hiding this comment.
This change adds two attributes to the argument of mkDerivation these two attributes are never used. So I wonder why you define them.
The ocaml and camlp5 attributes are not used it this derivation but in some Coq libraries that define OCaml plugins: they have to be compiled with the same version of the OCaml compiler that is used to compile Coq itself. That’s why these attributes “remember” with which OCaml/camlp5 Coq is compiled.
BTW, what do you call “casted”?
There was a problem hiding this comment.
This change adds two attributes to the argument of mkDerivation these two attributes are never used. So I wonder why you define them.
I assumed this is necessary because of https://github.com/NixOS/nixpkgs/pull/21822/files#diff-036410e9211b4336186fc613f7200b12L16966. But it looks like defining it in let is sufficient for coq-modules to get the right version of camlp5 (coq.camlp5).
BTW, what do you call “casted”?
I refer (ocamlPackages) ocaml ... as casting (nonstandard terminology, but it sure looks like type casting).
There was a problem hiding this comment.
Confirmed, coq.camlp5 has been used several times but neither for coq.findlib and coq.lablgtk.
There was a problem hiding this comment.
I refer
(ocamlPackages) ocaml ...as casting.
This piece of syntax cannot exist alone: it must come after the inherit keyword. It has nothing to do with type casting; it defines some attributes. See the nix manual for details.
There was a problem hiding this comment.
I know, I was just using 'casting' to describe the parentheses syntax. From the manual, this wasn't stated explicitly, only as an example ((xlibs)).
|
I know, I was just using 'casting' to describe the parentheses syntax.
If you really want to compare with C or Java syntax, it is much more
similar to an `if` construct (as in `if (b) ++x`; from this snippet, it
would make no sense to refer only to the `(b) ++x` fragment).
Back to the topic of this PR, the Nixpkgs contributor guide has [clear
recommendations on how to name
packages](https://nixos.org/nixpkgs/manual/#sec-package-naming),
specially when packaging “not a release but a commit from a repository”.
So please prepend `unstable-` to the version attribute (or insert it in
the name attribute).
|
|
Well, fine, in C-like langs, typecasting / type conversion can't be stated as a stand-alone expression, while Since version MUST start with a number, so I suppose it should inserted into the name attribute. |
|
(This is outside the scope of this PR, but any conclusion/standardization made here should apply to these packages as well: ) |
|
Confirmed, `coq.camlp5` has been used several times but neither for `coq.findlib` and `coq.lablgtk`.
Now there is a case for `coq.findlib` in ssreflect and mathcomp.
|
|
|
| @@ -6,6 +6,7 @@ | |||
| }: | |||
|
|
|||
| stdenv.mkDerivation rec { | |||
| version = ";"; | |||
There was a problem hiding this comment.
(accidentally did git commit -am on an unstaged local change ... reverting this line)
Motivation for this change
Testing an automatically generated nix file update, through https://github.com/rht/nixpkg-git-fetch-head/blob/master/nixpkg-git-fetch-head.sh.
With tiny modification (e.g. replace the ls-remote HEAD tag with release tags), this could be used for other packages that mainly use
fetchgit.Things done
(nix.useSandbox on NixOS,
or option
build-use-sandboxinnix.confon non-NixOS)
nix-shell -p nox --run "nox-review wip"./result/bin/)