diff --git a/.nix/auto-config.nix b/.nix/auto-config.nix new file mode 100644 index 0000000..640999c --- /dev/null +++ b/.nix/auto-config.nix @@ -0,0 +1,149 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. +# this config parser reads a config file with its format attributes +# (or default to the last available format) +prefix: +with builtins; +let + optionalImport = f: d: + if (isPath f || isString f) && pathExists f then import f else d; + get-path = f: let local = prefix + "/.nix/${f}"; in + if pathExists local then local else ./. + "/${f}"; +in +{ + config-file ? get-path "config.nix", + fallback-file ? get-path "fallback-config.nix", + nixpkgs-file ? get-path "nixpkgs.nix", + shellHook-file ? get-path "shellHook.sh", + overlays-dir ? get-path "overlays", + coq-overlays-dir ? get-path "coq-overlays", + ocaml-overlays-dir ? get-path "ocaml-overlays", + config ? {}, + withEmacs ? false, + print-env ? false, + do-nothing ? false, + update-nixpkgs ? false, + ci ? false, + inNixShell ? null +}@args: +let + do-nothing = (args.do-nothing or false) || update-nixpkgs; + input = { + config = optionalImport config-file (optionalImport fallback-file {}) ; + nixpkgs = optionalImport nixpkgs-file (throw "cannot find nixpkgs"); + }; +in +let tmp-pkgs = import input.nixpkgs {}; in +with (tmp-pkgs.coqPackages.lib or tmp-pkgs.lib); +if (input.config.format or "1.0.0") == "1.0.0" then + let + inNixShell = args.inNixShell or trivial.inNixShell; + attribute-from = coq-attribute: "coqPackages.${coq-attribute}"; + logpath-from = namespace: concatStringsSep "/" (splitString "." namespace); + config = rec { + format = "1.0.0"; + coq-attribute = input.config.coq-attribute or "template"; + attribute = input.config.attribute or (attribute-from coq-attribute); + nixpkgs = input.config.nixpkgs or input.nixpkgs; + ppath = input.config.ppath or (splitString "." attribute); + pname = input.config.pname or (last ppath); + namespace = input.config.namespace or "."; + logpath = input.config.logpath or (logpath-from namespace); + realpath = input.config.realpath or "."; + select = input.config.select or 0; + inputs = input.config.inputs or [ {} ]; + override = input.config.override or {}; + src = input.config.src or fetchGit ( + if false # replace by a version check when supported + # cf https://github.com/NixOS/nix/issues/1837 + then { url = prefix; shallow = true; } else prefix); }; + in + with config; switch-if [ + { cond = attribute-from coq-attribute != attribute; + out = throw "One cannot set both `coq-attribute` and `attribute`."; } + { cond = logpath-from namespace != config.logpath; + out = throw "One cannot set both `namespace` and `logpath`."; } + ] (let + mk-overlays = path: callPackage: + if !pathExists path then {} + else mapAttrs (x: _v: callPackage (path + "/${x}") {}) (readDir path); + # preparing inputs + inputs = forEach config.inputs + (i: foldl recursiveUpdate {} [ + (setAttrByPath ppath { override.version = "${src}"; ci = true; }) + i config.override + ]); + do-override = pkg: cfg: + let pkg' = if cfg?override + then pkg.override or (x: pkg) cfg.override else pkg; in + if cfg?overrideAttrs + then pkg'.overrideAttrs cfg.overrideAttrs else pkg'; + mk-instance = input: let + nixpkgs-overrides = + self: super: mapAttrs (n: ov: do-override super.${n} ov) + (removeAttrs input [ "coqPackages" "ocamlPackages" ]); + ocaml-overrides = + self: super: mapAttrs (n: ov: do-override super.${n} ov) + (input.ocamlPackages or {}); + coq-overrides = + self: super: mapAttrs + (n: ov: do-override (super.${n} or + (makeOverridable self.mkCoqDerivation { + pname = "${n}"; version = "${src}"; + })) ov) + (input.coqPackages or {}); + fold-override = foldl (fpkg: override: fpkg.overrideScope' override); + overlays = [ + (self: super: mk-overlays overlays-dir self.callPackage) + nixpkgs-overrides + (self: super: { coqPackages = fold-override super.coqPackages ([ + (self: super: mk-overlays coq-overlays-dir self.callPackage) + coq-overrides + (self: super: { coq = super.coq.override { + customOCamlPackages = fold-override super.coq.ocamlPackages [ + (self: super: mk-overlays ocaml-overlays-dir self.callPackage) + ocaml-overrides + ];};}) + ]);}) + (self: super: { coqPackages = + super.coqPackages.filterPackages + (! (super.coqPackages.coq.dontFilter or false)); }) + ]; in rec { + inherit input; + pkgs = import config.nixpkgs { inherit overlays; }; + default-coq-derivation = + makeOverridable pkgs.coqPackages.mkCoqDerivation + { inherit pname; version = "${src}"; }; + this-pkg = attrByPath ppath default-coq-derivation pkgs; + emacs = with pkgs; emacsWithPackages + (epkgs: with epkgs.melpaStablePackages; [proof-general]); + ci-coqpkgs = + filterAttrs (n: v: input.coqPackages.${n}.ci or false) + pkgs.coqPackages; + json_input = toJSON input; + }; + instances = map mk-instance inputs; + selected-instance = elemAt instances select; + shellHook = readFile shellHook-file + + optionalString print-env "nixEnv" + + optionalString update-nixpkgs "updateNixPkgs; exit"; + nix-shell = with selected-instance; this-pkg.overrideAttrs (old: { + inherit json_input shellHook; + currentdir = prefix; + coq_version = pkgs.coqPackages.coq.coq-version; + inherit nixpkgs logpath realpath; + + buildInputs = optionals (!do-nothing) + (old.buildInputs or [] ++ optional withEmacs pkgs.emacs); + + propagatedBuildInputs = optionals (!do-nothing) + (old.propagatedBuildInputs or []); + }); + nix-ci = map (b: b.ci-coqpkgs) instances; + nix-default = selected-instance.this-pkg; + nix-auto = if inNixShell then nix-shell else + if ci then nix-ci else nix-default; + in {inherit nixpkgs config selected-instance instances shellHook + nix-shell nix-default nix-ci nix-auto; } + ) +else throw "Current config.format (${input.config.format}) not implemented" \ No newline at end of file diff --git a/.nix/nixpkgs.nix b/.nix/nixpkgs.nix new file mode 100644 index 0000000..c5647f4 --- /dev/null +++ b/.nix/nixpkgs.nix @@ -0,0 +1,4 @@ +fetchTarball { + url = https://github.com/NixOS/nixpkgs/archive/6dbcdd2bc19d4377a250c73e658445426de64957.tar.gz; + sha256 = "1gaba2csw6p6mdx2q8qnxd18bzz4kfjgfgsvy1vb3nrp9qd6iiv9"; + } diff --git a/.nix/shellHook.sh b/.nix/shellHook.sh new file mode 100644 index 0000000..84fc30e --- /dev/null +++ b/.nix/shellHook.sh @@ -0,0 +1,104 @@ +#! /usr/bin/bash + +printNixEnv () { + echo "Here is your work environement" + echo "buildInputs:" + for x in $buildInputs; do printf " "; echo $x | cut -d "-" -f "2-"; done + echo "propagatedBuildInputs:" + for x in $propagatedBuildInputs; do printf " "; echo $x | cut -d "-" -f "2-"; done + echo "you can pass option --arg config '{coq = \"x.y\"; ...}' to nix-shell to change packages versions" +} +catNixEnv () { + for x in $buildInputs; do echo $x; done + for x in $propagatedBuildInputs; do echo $x; done +} + +upateNixDefault () { + cat $currentdir/default.nix +} > default.nix + +updateNixPkgs (){ + HASH=$(git ls-remote https://github.com/NixOS/nixpkgs refs/heads/nixpkgs-unstable | cut -f1); + URL=https://github.com/NixOS/nixpkgs/archive/$HASH.tar.gz + SHA256=$(nix-prefetch-url --unpack $URL) + echo "fetchTarball { + url = $URL; + sha256 = \"$SHA256\"; + }" > .nix/nixpkgs.nix +} + +updateNixPkgsMaster (){ + HASH=$(git ls-remote https://github.com/NixOS/nixpkgs refs/heads/master | cut -f1) + URL=https://github.com/NixOS/nixpkgs/archive/$HASH.tar.gz + SHA256=$(nix-prefetch-url --unpack $URL) + echo "fetchTarball { + url = $URL; + sha256 = \"$SHA256\"; + }" > .nix/nixpkgs.nix +} + +updateNixPkgsCustom (){ + if [[ -n "$1" ]] + then if [[ -n "$2" ]]; then B=$2; else B="master"; fi + HASH=$(git ls-remote https://github.com/$1/nixpkgs refs/heads/$B | cut -f1) + URL=https://github.com/$1/nixpkgs/archive/$HASH.tar.gz + SHA256=$(nix-prefetch-url --unpack $URL) + echo "fetchTarball { + url = $URL; + sha256 = \"$SHA256\"; + }" > .nix/nixpkgs.nix + else echo "error: usage: updateNixPkgsCustom [branch]" + fi +} + +printNixInputs (){ + echo current input: $json_input +} + +initNixConfig (){ + F=./.nix/config.nix; + if [[ -f $F ]] + then echo "$F already exists" + else if [[ -n "$1" ]] + then echo "{" > $F + echo " coq-attribute = \"$1\";" >> $F + echo " overrides = {};" >> $F + echo "}" >> $F + chmod u+w $F + else echo "usage: initNixConfig pname" + fi + fi +} + +fetchCoqOverlay (){ + F=$nixpkgs/pkgs/development/coq-modules/$1/default.nix + D=./.nix/coq-overlays/$1/ + if [[ -f "$F" ]] + then mkdir -p $D; cp $F $D; chmod u+w ${D}default.nix; + git add ${D}default.nix + echo "You may now amend ${D}default.nix" + else echo "usage: fetchCoqOverlay pname" + fi +} + +cachedMake (){ + vopath="$(env -i nix-build)/lib/coq/$coq_version/user-contrib/$logpath" + dest="$(git rev-parse --show-toplevel)/$realpath" + echo "Compiling/Fetching and copying vo from $vopath to $realpath" + rsync -r --ignore-existing --include=*/ $vopath/* $dest +} + +nixHelp (){ + cat < {}), coq-version-or-url, shell ? false }: - -let - coq-version-parts = builtins.match "([0-9]+).([0-9]+)" coq-version-or-url; - coqPackages = - if coq-version-parts == null then - pkgs.mkCoqPackages (import (fetchTarball coq-version-or-url) {}) - else - pkgs."coqPackages_${builtins.concatStringsSep "_" coq-version-parts}"; -in - -with coqPackages; - -pkgs.stdenv.mkDerivation { - - name = "{{ shortname }}"; - -{{# plugin }} - buildInputs = with coq.ocamlPackages; [ ocaml findlib ] - ++ pkgs.lib.optionals shell [ merlin ocp-indent ocp-index ]; - -{{/ plugin }} - propagatedBuildInputs = [ - coq -{{# dependencies }} - {{ nix }} -{{/ dependencies }} - ]; - - src = if shell then null else ./.; - - installFlags = "COQMF_COQLIB=$(out)/lib/coq/${coq.coq-version}/"; -} diff --git a/fallback-config.nix.mustache b/fallback-config.nix.mustache new file mode 100644 index 0000000..d462cc2 --- /dev/null +++ b/fallback-config.nix.mustache @@ -0,0 +1,3 @@ +{ + coq-attribute = "{{nix_name}}"; +} diff --git a/generate.sh b/generate.sh index 0402135..91fd27e 100755 --- a/generate.sh +++ b/generate.sh @@ -95,20 +95,29 @@ for f in "$srcdir"/{,.}*.mustache; do continue fi ;; - config.yml) - mustache='{{ circleci }}' - bool=$(get_yaml meta.yml <<<"$mustache") + config.yml) + mustache='{{ circleci }}' + bool=$(get_yaml meta.yml <<<"$mustache") + if [ -n "$bool" ] && [ "$bool" != false ]; then + mkdir -p -v .circleci && target=".circleci/$target" + else + continue + fi + ;; + default.nix) + mustache='{{ nix }}' + bool=$(get_yaml meta.yml <<<"$mustache") if [ -n "$bool" ] && [ "$bool" != false ]; then - mkdir -p -v .circleci && target=".circleci/$target" + : noop else continue fi ;; - default.nix) + fallback-config.nix) mustache='{{ nix }}' bool=$(get_yaml meta.yml <<<"$mustache") if [ -n "$bool" ] && [ "$bool" != false ]; then - : noop + mkdir -p -v .nix && target=".nix/$target" else continue fi diff --git a/nix-action.yml.mustache b/nix-action.yml.mustache index 68b52fa..cc31694 100644 --- a/nix-action.yml.mustache +++ b/nix-action.yml.mustache @@ -13,27 +13,31 @@ on: jobs: build: runs-on: ubuntu-latest - strategy: - matrix: - version_or_url: -{{# tested_coq_nix_versions }} - - '{{ version_or_url }}' -{{/ tested_coq_nix_versions }}{{^ tested_coq_nix_versions }} - 'https://github.com/coq/coq-on-cachix/tarball/master' -{{/ tested_coq_nix_versions }} - fail-fast: false steps: - uses: cachix/install-nix-action@v12 with: nix_path: nixpkgs=channel:nixpkgs-unstable +{{# cachix}} - uses: cachix/cachix-action@v8 with: # Name of a cachix cache to pull/substitute - name: coq + name: {{name}} +{{=<% %>=}} +<%# key%> + signingKey: '${{ secrets.<%key%> }}' +<%/ key%> +<%# token%> + authToken: '${{ secrets.<%token%> }}' +<%/ token%> +<%={{ }}=%> +{{/ cachix}} - uses: actions/checkout@v2 + with: + fetch-depth: 0 {{# submodule }} - name: Checkout submodules uses: textbook/git-checkout-submodule-action@2.1.1 {{/ submodule }} {{! Change delimiters to avoid the next line being parsed as mustache syntax. }} {{=<% %>=}} - - run: nix-build --argstr coq-version-or-url "${{ matrix.version_or_url }}" + - run: nix-build --arg ci true diff --git a/ref.yml b/ref.yml index 19d4325..8141543 100644 --- a/ref.yml +++ b/ref.yml @@ -40,6 +40,11 @@ fields: - docker-action.yml - dune-project - dune + - nix_name: + required: false + default: "{{ shortname }}" + used: + - fallback-config.nix - organization: required: true used: @@ -392,29 +397,22 @@ fields: used: - coq.opam - .travis.yml - - tested_coq_nix_versions: + - cachix: type: list - description: If empty, the master branch of Coq will be tested. + description: Cachix repositories to use item_fields: - - version_or_url: + - name: required: true - description: > - This can be a version number of a version packaged in - nixpkgs (example: 8.5, 8.11). Cf. the coqPackages_8_XX - attributes defined at the end of this file: - https://github.com/NixOS/nixpkgs/blob/nixpkgs-unstable/pkgs/top-level/coq-packages.nix - (Quote the version number, otherwise '8.10' becomes '8.1'.) - - Or this can be a URL, to test your project with a - version of Coq under development. Typically this is - https://github.com/coq/coq-on-cachix/tarball/master but - 'master' may be replaced by any valid reference like one - of the branches available at - https://github.com/coq/coq-on-cachix/branches or a valid - commit hash. - used: - - .travis.yml - - nix-action.yml + description: Name of the cachix repository + examples: + - "coq" + - "math-comp" + - key: + required: false + description: Secret signingKey for the repository + - token: + required: false + description: Secret authToken for the repository - tested_coq_opam_versions: type: list item_fields: