Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ocamlPackages.elpi: use release tarball #343266

Merged
merged 2 commits into from
Sep 23, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion doc/languages-frameworks/coq.section.md
Original file line number Diff line number Diff line change
Expand Up @@ -23,12 +23,13 @@ The recommended way of defining a derivation for a Coq library, is to use the `c
* if it is a string of the form `owner:branch` then it tries to download the `branch` of owner `owner` for a project of the same name using the same vcs, and the `version` attribute of the resulting derivation is set to `"dev"`, additionally if the owner is not provided (i.e. if the `owner:` prefix is missing), it defaults to the original owner of the package (see below),
* if it is a string of the form `"#N"`, and the domain is github, then it tries to download the current head of the pull request `#N` from github,
* `defaultVersion` (optional). Coq libraries may be compatible with some specific versions of Coq only. The `defaultVersion` attribute is used when no `version` is provided (or if `version = null`) to select the version of the library to use by default, depending on the context. This selection will mainly depend on a `coq` version number but also possibly on other packages versions (e.g. `mathcomp`). If its value ends up to be `null`, the package is marked for removal in end-user `coqPackages` attribute set.
* `release` (optional, defaults to `{}`), lists all the known releases of the library and for each of them provides an attribute set with at least a `hash` attribute (you may put the empty string `""` in order to automatically insert a fake hash, this will trigger an error which will allow you to find the correct hash), each attribute set of the list of releases also takes optional overloading arguments for the fetcher as below (i.e.`domain`, `owner`, `repo`, `rev` assuming the default fetcher is used) and optional overrides for the result of the fetcher (i.e. `version` and `src`).
* `release` (optional, defaults to `{}`), lists all the known releases of the library and for each of them provides an attribute set with at least a `hash` attribute (you may put the empty string `""` in order to automatically insert a fake hash, this will trigger an error which will allow you to find the correct hash), each attribute set of the list of releases also takes optional overloading arguments for the fetcher as below (i.e.`domain`, `owner`, `repo`, `rev`, `artifact` assuming the default fetcher is used) and optional overrides for the result of the fetcher (i.e. `version` and `src`).
* `fetcher` (optional, defaults to a generic fetching mechanism supporting github or gitlab based infrastructures), is a function that takes at least an `owner`, a `repo`, a `rev`, and a `hash` and returns an attribute set with a `version` and `src`.
* `repo` (optional, defaults to the value of `pname`),
* `owner` (optional, defaults to `"coq-community"`).
* `domain` (optional, defaults to `"github.com"`), domains including the strings `"github"` or `"gitlab"` in their names are automatically supported, otherwise, one must change the `fetcher` argument to support them (cf `pkgs/development/coq-modules/heq/default.nix` for an example),
* `releaseRev` (optional, defaults to `(v: v)`), provides a default mapping from release names to revision hashes/branch names/tags,
* `releaseArtifact` (optional, defaults to `(v: null)`), provides a default mapping from release names to artifact names (only works for github artifact for now),
* `displayVersion` (optional), provides a way to alter the computation of `name` from `pname`, by explaining how to display version numbers,
* `namePrefix` (optional, defaults to `[ "coq" ]`), provides a way to alter the computation of `name` from `pname`, by explaining which dependencies must occur in `name`,
* `nativeBuildInputs` (optional), is a list of executables that are required to build the current derivation, in addition to the default ones (namely `which`, `dune` and `ocaml` depending on whether `useDune`, `useDuneifVersion` and `mlPlugin` are set).
Expand Down
4 changes: 2 additions & 2 deletions pkgs/applications/science/logic/coq/default.nix
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
# - The exact version can be specified through the `version` argument to
# the derivation; it defaults to the latest stable version.

{ lib, stdenv, fetchzip, writeText, pkg-config, gnumake42
{ lib, stdenv, fetchzip, fetchurl, writeText, pkg-config, gnumake42
, customOCamlPackages ? null
, ocamlPackages_4_05, ocamlPackages_4_09, ocamlPackages_4_10, ocamlPackages_4_12
, ocamlPackages_4_14
Expand Down Expand Up @@ -62,7 +62,7 @@ let
};
releaseRev = v: "V${v}";
fetched = import ../../../../build-support/coq/meta-fetch/default.nix
{ inherit lib stdenv fetchzip; }
{ inherit lib stdenv fetchzip fetchurl; }
{ inherit release releaseRev; location = { owner = "coq"; repo = "coq";}; }
args.version;
version = fetched.version;
Expand Down
4 changes: 2 additions & 2 deletions pkgs/build-support/coq/default.nix
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
{ lib, stdenv, coqPackages, coq, which, fetchzip }@args:
{ lib, stdenv, coqPackages, coq, which, fetchzip, fetchurl }@args:

let
lib = import ./extra-lib.nix {
Expand Down Expand Up @@ -71,7 +71,7 @@ let
"extraInstallFlags" "setCOQBIN" "mlPlugin"
"dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs;
fetch = import ../coq/meta-fetch/default.nix
{ inherit lib stdenv fetchzip; } ({
{ inherit lib stdenv fetchzip fetchurl; } ({
inherit release releaseRev;
location = { inherit domain owner repo; };
} // optionalAttrs (args?fetcher) {inherit fetcher;});
Expand Down
21 changes: 14 additions & 7 deletions pkgs/build-support/coq/meta-fetch/default.nix
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
{ lib, stdenv, fetchzip }@args:
{ lib, stdenv, fetchurl, fetchzip }@args:

let
lib = import ../extra-lib.nix {
Expand Down Expand Up @@ -28,11 +28,16 @@ let

inherit (lib.strings) match split;

default-fetcher = {domain ? "github.com", owner ? "", repo, rev, name ? "source", sha256 ? null, ...}@args:
let ext = if args?sha256 then "zip" else "tar.gz";
fmt = if args?sha256 then "zip" else "tarball";
default-fetcher = {domain ? "github.com", owner ? "", repo, rev, name ? "source", sha256 ? null, artifact ? null, ...}@args:
let kind = switch-if [
{ cond = artifact != null; out = {ext = "tbz"; fmt = "tbz"; fetchfun = fetchurl; }; }
{ cond = args?sha256 ; out = {ext = "zip"; fmt = "zip"; fetchfun = fetchzip; }; }
] {ext = "tar.gz"; fmt = "tarball"; fetchfun = builtins.fetchTarball; }; in
with kind; let
pr = match "^#(.*)$" rev;
url = switch-if [
{ cond = pr == null && (match "^github.*" domain) != null && artifact != null;
out = "https://github.com/${owner}/${repo}/releases/download/${rev}/${artifact}"; }
{ cond = pr == null && (match "^github.*" domain) != null;
out = "https://${domain}/${owner}/${repo}/archive/${rev}.${ext}"; }
{ cond = pr != null && (match "^github.*" domain) != null;
Expand All @@ -42,16 +47,18 @@ let
{ cond = (match "(www.)?mpi-sws.org" domain) != null;
out = "https://www.mpi-sws.org/~${owner}/${repo}/download/${repo}-${rev}.${ext}";}
] (throw "meta-fetch: no fetcher found for domain ${domain} on ${rev}");
fetch = x: if args?sha256 then fetchzip (x // { inherit sha256; }) else builtins.fetchTarball x;
fetch = x: fetchfun (if args?sha256 then (x // { inherit sha256; }) else x);
in fetch { inherit url ; };
in
{
fetcher ? default-fetcher,
location,
release ? {},
releaseRev ? (v: v),
releaseArtifact ? (v: null)
}:
let isVersion = x: isString x && match "^/.*" x == null && release?${x};
let
isVersion = x: isString x && match "^/.*" x == null && release?${x};
shortVersion = x: if (isString x && match "^/.*" x == null)
then findFirst (v: versions.majorMinor v == x) null
(sort versionAtLeast (attrNames release))
Expand All @@ -71,7 +78,7 @@ switch arg [
in
{
version = rv.version or v;
src = rv.src or fetcher (location // { rev = releaseRev v; } // rv);
src = rv.src or fetcher (location // { rev = releaseRev v; artifact = releaseArtifact v; } // rv);
};
}
{ case = isString;
Expand Down
33 changes: 15 additions & 18 deletions pkgs/development/ocaml-modules/elpi/default.nix
Original file line number Diff line number Diff line change
Expand Up @@ -9,39 +9,36 @@
, ppxlib_0_15, ppx_deriving_0_15
, coqPackages
, version ? if lib.versionAtLeast ocaml.version "4.08" then "1.18.1"
else if lib.versionAtLeast ocaml.version "4.07" then "1.15.2" else "1.14.1"
else "1.15.2"
}:

let p5 = camlp5; in
let camlp5 = p5.override { legacy = true; }; in

let fetched = coqPackages.metaFetch ({
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@vbgl removing this will break the ability to conveniently overlay ocamlPackages.elpi in various CIs to anything else than released versions, which might be pretty unconvenient. Although I'm not sure how often we use that feature.
Cc @CohenCyril @gares ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Right. So my question is: can we use metaFetch to download the released artifacts when available?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I use that feature via the coq nix toolbox.
But I also need elpi to have a version number (for conditional compilation).

I hope both requirements are not in conflict.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

can we use metaFetch to download the released artifacts when available?

I don't know, but if not, maybe an option can be added?

Copy link
Contributor

@CohenCyril CohenCyril Sep 20, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Right. So my question is: can we use metaFetch to download the released artifacts when available?

Sure, feel free to amend the default-fetcher here:
https://github.com/NixOS/nixpkgs/blob/master/pkgs/build-support/coq/meta-fetch/default.nix
You can add an extra "artifact" argument (false by default?) to change the url in the github case here:

{ cond = pr != null && (match "^github.*" domain) != null;
out = "https://api.${domain}/repos/${owner}/${repo}/${fmt}/pull/${head pr}/head"; }

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I use fetchurl when you probably use fetchzip?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah ... sure, but I thought the uncompressed archives were compared... why is the result different?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

fetchurl does not decompress: it computes the hash of the downloaded file.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done: da329e4

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks. Cherry-picked to this branch.

release."1.19.2".sha256 = "sha256-7VTUbsFVoNT6srLwcAn5WNSsWC7cVUdphKRWBHHiH5M=";
release."1.18.1".sha256 = "sha256-zgBJefQDe3JyCGbC0wvMcx/9iMVbftBJ43NPogkNeHY=";
release."1.17.0".sha256 = "sha256-DTxE8CvYl0et20pxueydI+WzraI6UPHMNvxyp2gU/+w=";
release."1.16.5".sha256 = "sha256-tKX5/cVPoBeHiUe+qn7c5FIRYCwY0AAukN7vSd/Nz9A=";
release."1.15.2".sha256 = "sha256-XgopNP83POFbMNyl2D+gY1rmqGg03o++Ngv3zJfCn2s=";
release."1.15.0".sha256 = "sha256:1ngdc41sgyzyz3i3lkzjhnj66gza5h912virkh077dyv17ysb6ar";
release."1.14.1".sha256 = "sha256-BZPVL8ymjrE9kVGyf6bpc+GA2spS5JBpkUtZi04nPis=";
release."1.13.7".sha256 = "10fnwz30bsvj7ii1vg4l1li5pd7n0qqmwj18snkdr5j9gk0apc1r";
release."1.13.5".sha256 = "02a6r23mximrdvs6kgv6rp0r2dgk7zynbs99nn7lphw2c4189kka";
release."1.13.1".sha256 = "12a9nbdvg9gybpw63lx3nw5wnxfznpraprb0wj3l68v1w43xq044";
release."1.13.0".sha256 = "0dmzy058m1mkndv90byjaik6lzzfk3aaac7v84mpmkv6my23bygr";
release."1.12.0".sha256 = "1agisdnaq9wrw3r73xz14yrq3wx742i6j8i5icjagqk0ypmly2is";
release."1.11.4".sha256 = "1m0jk9swcs3jcrw5yyw5343v8mgax238cjb03s8gc4wipw1fn9f5";
release."1.19.2".sha256 = "sha256-dBj5Ek7PWq/8Btq/dggJUqa8cUtfvbi6EWo/lJEDOU4=";
release."1.18.1".sha256 = "sha256-rrIv/mVC0Ez3nU7fpnzwduIC3tI6l73DjgAbv1gd2v0=";
release."1.17.0".sha256 = "sha256-J8FJBeaB+2HtHjrkgNzOZJngZ2AcYU+npL9Y1HNPnzo=";
release."1.15.2".sha256 = "sha256-+sQYQiN3n+dlzXzi5opOjhkJZqpkNwlHZcUjaUM6+xQ=";
release."1.15.0".sha256 = "sha256-vpQzbkDqJPCmaBmXcBnzlWGS7djW9wWv8xslkIlXgP0=";
release."1.13.7".sha256 = "sha256-0QbOEnrRCYA2mXDGRKe+QYCXSESLJvLzRW0Iq+/3P9Y=";
release."1.12.0".sha256 = "sha256-w4JzLZB8jcxw7nA7AfgU9jTZTr6IYUxPU5E2vNIFC4Q=";
release."1.11.4".sha256 = "sha256-dyzEpzokgffsF9lt+FZgUlcZEuAb70vGuHfGUtjZYIM=";
releaseRev = v: "v${v}";
releaseArtifact = v: if lib.versionAtLeast v "1.13.8"
then "elpi-${v}.tbz"
else "elpi-v${v}.tbz";
location = { domain = "github.com"; owner = "LPCIC"; repo = "elpi"; };
}) version;
in
buildDunePackage rec {
buildDunePackage {
pname = "elpi";
inherit (fetched) version src;

patches = lib.optional (version == "1.16.5")
./atd_2_10.patch;

minimalOCamlVersion = "4.04";
duneVersion = "3";
minimalOCamlVersion = "4.07";

# atdgen is both a library and executable
nativeBuildInputs = [ perl ]
Expand All @@ -68,6 +65,6 @@ buildDunePackage rec {
};

postPatch = ''
substituteInPlace elpi_REPL.ml --replace "tput cols" "${ncurses}/bin/tput cols"
substituteInPlace elpi_REPL.ml --replace-warn "tput cols" "${ncurses}/bin/tput cols"
'';
}
4 changes: 2 additions & 2 deletions pkgs/top-level/coq-packages.nix
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
{ lib, stdenv, fetchzip
{ lib, stdenv, fetchurl, fetchzip
, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09
, ocamlPackages_4_10, ocamlPackages_4_12, ocamlPackages_4_14
, fetchpatch, makeWrapper, coq2html
Expand All @@ -11,7 +11,7 @@ let
coqPackages = self // { __attrsFailEvaluation = true; recurseForDerivations = false; };

metaFetch = import ../build-support/coq/meta-fetch/default.nix
{inherit lib stdenv fetchzip; };
{inherit lib stdenv fetchzip fetchurl; };
mkCoqDerivation = lib.makeOverridable (callPackage ../build-support/coq {});

contribs = recurseIntoAttrs
Expand Down