|
| 1 | +with builtins; with (import <nixpkgs> {}).lib; |
| 2 | +{ |
| 3 | + ## DO NOT CHANGE THIS |
| 4 | + format = "1.0.0"; |
| 5 | + ## unless you made an automated or manual update |
| 6 | + ## to another supported format. |
| 7 | + |
| 8 | + ## The attribute to build from the local sources, |
| 9 | + ## either using nixpkgs data or the overlays located in `.nix/coq-overlays` |
| 10 | + ## Will determine the default main-job of the bundles defined below |
| 11 | + attribute = "stdlib"; |
| 12 | + |
| 13 | + ## If you want to select a different attribute (to build from the local sources as well) |
| 14 | + ## when calling `nix-shell` and `nix-build` without the `--argstr job` argument |
| 15 | + # shell-attribute = "{{nix_name}}"; |
| 16 | + |
| 17 | + ## Maybe the shortname of the library is different from |
| 18 | + ## the name of the nixpkgs attribute, if so, set it here: |
| 19 | + # pname = "{{shortname}}"; |
| 20 | + |
| 21 | + ## Lists the dependencies, phrased in terms of nix attributes. |
| 22 | + ## No need to list Coq, it is already included. |
| 23 | + ## These dependencies will systematically be added to the currently |
| 24 | + ## known dependencies, if any more than Coq. |
| 25 | + ## /!\ Remove this field as soon as the package is available on nixpkgs. |
| 26 | + ## /!\ Manual overlays in `.nix/coq-overlays` should be preferred then. |
| 27 | + # buildInputs = [ ]; |
| 28 | + |
| 29 | + ## Indicate the relative location of your _CoqProject |
| 30 | + ## If not specified, it defaults to "_CoqProject" |
| 31 | + coqproject = "theories/_CoqProject"; |
| 32 | + |
| 33 | + ## Cachix caches to use in CI |
| 34 | + ## Below we list some standard ones |
| 35 | + cachix.coq = {}; |
| 36 | + cachix.math-comp = {}; |
| 37 | + # cachix.coq-community = {}; |
| 38 | + |
| 39 | + ## If you have write access to one of these caches you can |
| 40 | + ## provide the auth token or signing key through a secret |
| 41 | + ## variable on GitHub. Then, you should give the variable |
| 42 | + ## name here. For instance, coq-community projects can use |
| 43 | + ## the following line instead of the one above: |
| 44 | + cachix.coq-community.authToken = "CACHIX_AUTH_TOKEN"; |
| 45 | + |
| 46 | + ## Or if you have a signing key for a given Cachix cache: |
| 47 | + # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY" |
| 48 | + |
| 49 | + ## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY |
| 50 | + ## are the names of secret variables. They are set in |
| 51 | + ## GitHub's web interface. |
| 52 | + |
| 53 | + ## select an entry to build in the following `bundles` set |
| 54 | + ## defaults to "default" |
| 55 | + default-bundle = "coq-master"; |
| 56 | + |
| 57 | + ## write one `bundles.name` attribute set per |
| 58 | + ## alternative configuration |
| 59 | + ## When generating GitHub Action CI, one workflow file |
| 60 | + ## will be created per bundle |
| 61 | + bundles = let |
| 62 | + ## In some cases, light overrides are not available/enough |
| 63 | + ## in which case you can use either |
| 64 | + # coqPackages.<coq-pkg>.overrideAttrs = o: <overrides>; |
| 65 | + ## or a "long" overlay to put in `.nix/coq-overlays |
| 66 | + ## you may use `nix-shell --run fetchOverlay <coq-pkg>` |
| 67 | + ## to automatically retrieve the one from nixpkgs |
| 68 | + ## if it exists and is correctly named/located |
| 69 | + |
| 70 | + ## You can override Coq and other coqPackages |
| 71 | + ## through the following attribute |
| 72 | + ## If <ocaml-pkg> does not support light overrides, |
| 73 | + ## you may use `overrideAttrs` or long overlays |
| 74 | + ## located in `.nix/ocaml-overlays` |
| 75 | + ## (there is no automation for this one) |
| 76 | + # ocamlPackages.<ocaml-pkg>.override.version = "x.xx"; |
| 77 | + |
| 78 | + ## You can also override packages from the nixpkgs toplevel |
| 79 | + # <nix-pkg>.override.overrideAttrs = o: <overrides>; |
| 80 | + ## Or put an overlay in `.nix/overlays` |
| 81 | + |
| 82 | + ## you may mark a package as a main CI job (one to take deps and |
| 83 | + ## rev deps from) as follows |
| 84 | + # coqPackages.<main-pkg>.main-job = true; |
| 85 | + ## by default the current package and its shell attributes are main jobs |
| 86 | + |
| 87 | + ## you may mark a package as a CI job as follows |
| 88 | + # coqPackages.<another-pkg>.job = "test"; |
| 89 | + ## It can then built through |
| 90 | + ## nix-build --argstr bundle "default" --arg job "test"; |
| 91 | + ## in the absence of such a directive, the job "another-pkg" will |
| 92 | + ## is still available, but will be automatically included in the CI |
| 93 | + ## via the command genNixActions only if it is a dependency or a |
| 94 | + ## reverse dependency of a job flagged as "main-job" (see above). |
| 95 | + |
| 96 | + ## Run on push on following branches (default [ "master" ]) |
| 97 | + # push-branches = [ "master" "branch2" ]; |
| 98 | + |
| 99 | + master = [ |
| 100 | + "stdlib" |
| 101 | + "mathcomp" |
| 102 | + "fourcolor" |
| 103 | + "odd-order" |
| 104 | + "mathcomp-zify" |
| 105 | + "mathcomp-finmap" |
| 106 | + "mathcomp-bigenough" |
| 107 | + "mathcomp-analysis" |
| 108 | + # TODO unimath |
| 109 | + "unicoq" |
| 110 | + # "math-classes" -> overlay |
| 111 | + # "corn" -> overlay |
| 112 | + "stdpp" |
| 113 | + # "iris" -> overlay |
| 114 | + # "autosubst" -> overlay |
| 115 | + # TODO tests from iris/examples |
| 116 | + # "coq-hammer" -> overlay |
| 117 | + # "flocq" -> overlay |
| 118 | + # TODO coq-performance-tests |
| 119 | + # TODO coq-tools |
| 120 | + "coquelicot" |
| 121 | + # "compcert" -> overlay |
| 122 | + # "vst" -> overlay |
| 123 | + # TODO cross-crypto |
| 124 | + # TODO rewriter |
| 125 | + # TODO fiat_parsers |
| 126 | + # TODO fiat_crypto_legacy |
| 127 | + # TODO fiat_crypto |
| 128 | + # TODO rupicola |
| 129 | + # TODO bedrock2 |
| 130 | + # TODO coqutil |
| 131 | + # TODO kami |
| 132 | + # TODO riscv_coq |
| 133 | + "CoLoR" |
| 134 | + "bignums" |
| 135 | + "coqprime" |
| 136 | + # TODO bbv |
| 137 | + # TODO coinduction |
| 138 | + # "coq-elpi" -> overlay |
| 139 | + "hierarchy-builder" |
| 140 | + # TODO engine bench |
| 141 | + # TODO fcsl_pcm |
| 142 | + # "coq-ext-lib" -> overlay |
| 143 | + # "simple-io" -> overlay |
| 144 | + # "QuickChick" -> overlay |
| 145 | + # TODO reduction_effects |
| 146 | + # TODO menhirlib |
| 147 | + # TODO neural_net_interp |
| 148 | + # "aac-tactics" -> overlay |
| 149 | + "paco" |
| 150 | + # "ITree" -> overlay |
| 151 | + # TODO itree_io |
| 152 | + "ceres" |
| 153 | + "parsec" |
| 154 | + # TODO json |
| 155 | + # TODO async_test |
| 156 | + # TODO http |
| 157 | + "paramcoq" |
| 158 | + # "relation-algebra" -> overlay |
| 159 | + "StructTact" |
| 160 | + "InfSeqExt" |
| 161 | + "Cheerios" |
| 162 | + "Verdi" |
| 163 | + # TODO verdi-raft |
| 164 | + # TODO stdlib2 |
| 165 | + # TODO argosy |
| 166 | + # TODO atbr |
| 167 | + # TODO perennial |
| 168 | + # TODO sf |
| 169 | + # TODO Coqtail |
| 170 | + "deriving" |
| 171 | + # TODO vscoq (is vscoq-language-server enough?) |
| 172 | + # "category-theory" -> overlay |
| 173 | + "itauto" |
| 174 | + # TODO jasmin |
| 175 | + # TODO coq-lean-importer |
| 176 | + # TODO smtcoq_trakt |
| 177 | + # TODO stalmarck |
| 178 | + # TODO tactician |
| 179 | + # TODO ltac2_compiler |
| 180 | + # TODO waterproof |
| 181 | + # TODO autosubst OCaml |
| 182 | + ]; |
| 183 | + coq-master = [ |
| 184 | + "dpdgraph" |
| 185 | + # "smtcoq" -> overlay |
| 186 | + "trakt" |
| 187 | + ]; |
| 188 | + main = [ |
| 189 | + "coq-lsp" |
| 190 | + # "equations" -> overlay |
| 191 | + # "metacoq" -> overlay |
| 192 | + # "serapi" -> overlay |
| 193 | + "mathcomp-word" |
| 194 | + ]; |
| 195 | + common-bundles = listToAttrs (forEach master (p: |
| 196 | + { name = p; value.override.version = "master"; })) |
| 197 | + // listToAttrs (forEach coq-master (p: |
| 198 | + { name = p; value.override.version = "coq-master"; })) |
| 199 | + // listToAttrs (forEach main (p: |
| 200 | + { name = p; value.override.version = "main"; })) |
| 201 | + // { |
| 202 | + coq-elpi.override.version = "proux01:split_stdlib"; |
| 203 | + mathcomp.override.version = "proux01:split_stdlib"; |
| 204 | + # tlc.override.version = "master-for-coq-ci"; -> overlay |
| 205 | + tlc.override.version = "proux01:split_stdlib"; |
| 206 | + flocq.override.version = "split_stdlib"; |
| 207 | + coq-ext-lib.override.version = "split_stdlib"; |
| 208 | + aac-tactics.override.version = "split_stdlib"; |
| 209 | + coq-hammer.override.version = "proux01:split_stdlib"; |
| 210 | + math-classes.override.version = "split_stdlib"; |
| 211 | + corn.override.version = "split_stdlib"; |
| 212 | + equations.override.version = "proux01:split_stdlib"; |
| 213 | + autosubst.override.version = "split_stdlib"; |
| 214 | + relation-algebra.override.version = "proux01:split_stdlib"; |
| 215 | + category-theory.override.version = "proux01:split_stdlib"; |
| 216 | + metacoq.override.version = "proux01:split_stdlib"; |
| 217 | + compcert.override.version = "proux01:split_stdlib"; |
| 218 | + simple-io.override.version = "proux01:split_stdlib"; |
| 219 | + QuickChick.override.version = "proux01:split_stdlib"; |
| 220 | + serapi.override.version = "proux01:coq_19310"; |
| 221 | + iris.override.version = "proux:split_stdlib"; |
| 222 | + vst.override.version = "proux01:split_stdlib"; |
| 223 | + smtcoq.override.version = "split_stdlib"; |
| 224 | + CoLoR.override.version = "proux01:split_stdlib"; |
| 225 | + ITree.override.version = "proux01:split_stdlib"; |
| 226 | + }; |
| 227 | + in { |
| 228 | + "coq-master".coqPackages = common-bundles // { |
| 229 | + coq.override.version = "proux01:split_stdlib"; |
| 230 | + }; |
| 231 | + "coq-master".ocamlPackages = { elpi.override.version = "1.19.2"; }; |
| 232 | + }; |
| 233 | +} |
0 commit comments