tjh.dev
1{
2 coq,
3 rocqPackages,
4 mkCoqDerivation,
5 lib,
6 version ? null,
7}@args:
8(mkCoqDerivation {
9
10 pname = "stdlib";
11 repo = "stdlib";
12 owner = "coq";
13 opam-name = "coq-stdlib";
14
15 inherit version;
16 defaultVersion =
17 with lib.versions;
18 lib.switch coq.version [
19 {
20 case = isEq "9.0";
21 out = "9.0.0";
22 }
23 # the one below is artificial as stdlib was included in Coq before
24 {
25 case = isLt "9.0";
26 out = "9.0.0";
27 }
28 ] null;
29 releaseRev = v: "V${v}";
30
31 release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";
32
33 configurePhase = ''
34 echo no configuration
35 '';
36 buildPhase = ''
37 echo building nothing
38 '';
39 installPhase = ''
40 echo installing nothing
41 '';
42
43 meta = {
44 description = "Compatibility metapackage for Coq Stdlib library after the Rocq renaming";
45 license = lib.licenses.lgpl21Only;
46 };
47
48}).overrideAttrs
49 (
50 o:
51 # stdlib is already included in Coq <= 8.20
52 if coq.version != null && coq.version != "dev" && lib.versions.isLt "8.21" coq.version then
53 {
54 installPhase = ''
55 touch $out
56 '';
57 }
58 else
59 { propagatedBuildInputs = [ rocqPackages.stdlib ]; }
60 )