From 1ad210cbb2b8b99c999f093fc9e5217fab761434 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Tue, 31 Oct 2023 13:09:48 +0100 Subject: [PATCH 1/2] Build the nix derivation in CI I use my own fork of `cache-install` to cache the Nix store because the current release of `rikhuijzer/cache-install` doesn't cache the `/nix/var/nix/db/db.sqlite` database. Hence, Nix will treat all paths in `/nix/store` as invalid and rebuild all store paths. Warning: there are files will will *not* get compiled by Agda. Only Main and its dependencies are checked and compiled. --- .github/workflows/build.yml | 22 +++ default.nix | 23 ++-- nix/github-workflow-dependencies.nix | 15 ++ nix/sources.json | 14 ++ nix/sources.nix | 198 +++++++++++++++++++++++++++ 5 files changed, 261 insertions(+), 11 deletions(-) create mode 100644 .github/workflows/build.yml create mode 100644 nix/github-workflow-dependencies.nix create mode 100644 nix/sources.json create mode 100644 nix/sources.nix diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 00000000..ad8e454e --- /dev/null +++ b/.github/workflows/build.yml @@ -0,0 +1,22 @@ +name: Build the nix derivation + +on: + push: + branches: [ "main", "develop" ] + pull_request: + branches: + +jobs: + build: + + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v4 + - name: Install Nix with cached packages + uses: ibbem/cache-install@b5946e901c509f3478455a3f315e887e254bd36b + with: + key: nix-${{ hashFiles('.github/workflows/build.yml', 'default.nix', 'nix/**') }} + nix_file: nix/github-workflow-dependencies.nix + - name: Build + run: nix-build diff --git a/default.nix b/default.nix index b0c60748..335d351c 100644 --- a/default.nix +++ b/default.nix @@ -1,13 +1,14 @@ -# Goals -# Dependencies: agda-2.6.3, agda standard library at commit 177dc9e -# The standard library is part of this repository as a submodule in agda-stdlib. -# The submodule points at the standard library in the right version. -# To make it available while building and to editors, we have to set the AGDA_DIR -# environment variable to point to the "libs" directory in this repository -# export AGDA_DIR="path/to/this/repository/libs" -# I have documented more details on the setup in the README.md -{ pkgs ? import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/refs/tags/23.05.tar.gz") {} }: -pkgs.agdaPackages.mkDerivation { +{ + sources ? import ./nix/sources.nix, + system ? builtins.currentSystem, + pkgs ? + import sources.nixpkgs { + overlays = []; + config = {}; + inherit system; + }, +}: +pkgs.agdaPackages.mkDerivation rec { version = "1.0"; pname = "EPVL"; src = ./.; @@ -33,5 +34,5 @@ pkgs.agdaPackages.mkDerivation { install -D src/Main "$out/bin/$pname" ''; - meta = { description = "On the Expressive Power of Programming Languages"; }; + meta = {description = "On the Expressive Power of Programming Languages";}; } diff --git a/nix/github-workflow-dependencies.nix b/nix/github-workflow-dependencies.nix new file mode 100644 index 00000000..ef62453a --- /dev/null +++ b/nix/github-workflow-dependencies.nix @@ -0,0 +1,15 @@ +{ + sources ? import ./sources.nix, + system ? builtins.currentSystem, + pkgs ? + import sources.nixpkgs { + overlays = []; + config = {}; + inherit system; + }, +}: let + EPVL = import ../default.nix {}; +in + pkgs.mkShell { + inputsFrom = [EPVL]; + } diff --git a/nix/sources.json b/nix/sources.json new file mode 100644 index 00000000..bdc4c657 --- /dev/null +++ b/nix/sources.json @@ -0,0 +1,14 @@ +{ + "nixpkgs": { + "branch": "nixos-unstable", + "description": "Nix Packages collection", + "homepage": null, + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "4ecab3273592f27479a583fb6d975d4aba3486fe", + "sha256": "10wn0l08j9lgqcw8177nh2ljrnxdrpri7bp0g7nvrsn9rkawvlbf", + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/4ecab3273592f27479a583fb6d975d4aba3486fe.tar.gz", + "url_template": "https://github.com///archive/.tar.gz" + } +} diff --git a/nix/sources.nix b/nix/sources.nix new file mode 100644 index 00000000..fe3dadf7 --- /dev/null +++ b/nix/sources.nix @@ -0,0 +1,198 @@ +# This file has been generated by Niv. + +let + + # + # The fetchers. fetch_ fetches specs of type . + # + + fetch_file = pkgs: name: spec: + let + name' = sanitizeName name + "-src"; + in + if spec.builtin or true then + builtins_fetchurl { inherit (spec) url sha256; name = name'; } + else + pkgs.fetchurl { inherit (spec) url sha256; name = name'; }; + + fetch_tarball = pkgs: name: spec: + let + name' = sanitizeName name + "-src"; + in + if spec.builtin or true then + builtins_fetchTarball { name = name'; inherit (spec) url sha256; } + else + pkgs.fetchzip { name = name'; inherit (spec) url sha256; }; + + fetch_git = name: spec: + let + ref = + spec.ref or ( + if spec ? branch then "refs/heads/${spec.branch}" else + if spec ? tag then "refs/tags/${spec.tag}" else + abort "In git source '${name}': Please specify `ref`, `tag` or `branch`!" + ); + submodules = spec.submodules or false; + submoduleArg = + let + nixSupportsSubmodules = builtins.compareVersions builtins.nixVersion "2.4" >= 0; + emptyArgWithWarning = + if submodules + then + builtins.trace + ( + "The niv input \"${name}\" uses submodules " + + "but your nix's (${builtins.nixVersion}) builtins.fetchGit " + + "does not support them" + ) + { } + else { }; + in + if nixSupportsSubmodules + then { inherit submodules; } + else emptyArgWithWarning; + in + builtins.fetchGit + ({ url = spec.repo; inherit (spec) rev; inherit ref; } // submoduleArg); + + fetch_local = spec: spec.path; + + fetch_builtin-tarball = name: throw + ''[${name}] The niv type "builtin-tarball" is deprecated. You should instead use `builtin = true`. + $ niv modify ${name} -a type=tarball -a builtin=true''; + + fetch_builtin-url = name: throw + ''[${name}] The niv type "builtin-url" will soon be deprecated. You should instead use `builtin = true`. + $ niv modify ${name} -a type=file -a builtin=true''; + + # + # Various helpers + # + + # https://github.com/NixOS/nixpkgs/pull/83241/files#diff-c6f540a4f3bfa4b0e8b6bafd4cd54e8bR695 + sanitizeName = name: + ( + concatMapStrings (s: if builtins.isList s then "-" else s) + ( + builtins.split "[^[:alnum:]+._?=-]+" + ((x: builtins.elemAt (builtins.match "\\.*(.*)" x) 0) name) + ) + ); + + # The set of packages used when specs are fetched using non-builtins. + mkPkgs = sources: system: + let + sourcesNixpkgs = + import (builtins_fetchTarball { inherit (sources.nixpkgs) url sha256; }) { inherit system; }; + hasNixpkgsPath = builtins.any (x: x.prefix == "nixpkgs") builtins.nixPath; + hasThisAsNixpkgsPath = == ./.; + in + if builtins.hasAttr "nixpkgs" sources + then sourcesNixpkgs + else if hasNixpkgsPath && ! hasThisAsNixpkgsPath then + import { } + else + abort + '' + Please specify either (through -I or NIX_PATH=nixpkgs=...) or + add a package called "nixpkgs" to your sources.json. + ''; + + # The actual fetching function. + fetch = pkgs: name: spec: + + if ! builtins.hasAttr "type" spec then + abort "ERROR: niv spec ${name} does not have a 'type' attribute" + else if spec.type == "file" then fetch_file pkgs name spec + else if spec.type == "tarball" then fetch_tarball pkgs name spec + else if spec.type == "git" then fetch_git name spec + else if spec.type == "local" then fetch_local spec + else if spec.type == "builtin-tarball" then fetch_builtin-tarball name + else if spec.type == "builtin-url" then fetch_builtin-url name + else + abort "ERROR: niv spec ${name} has unknown type ${builtins.toJSON spec.type}"; + + # If the environment variable NIV_OVERRIDE_${name} is set, then use + # the path directly as opposed to the fetched source. + replace = name: drv: + let + saneName = stringAsChars (c: if (builtins.match "[a-zA-Z0-9]" c) == null then "_" else c) name; + ersatz = builtins.getEnv "NIV_OVERRIDE_${saneName}"; + in + if ersatz == "" then drv else + # this turns the string into an actual Nix path (for both absolute and + # relative paths) + if builtins.substring 0 1 ersatz == "/" then /. + ersatz else /. + builtins.getEnv "PWD" + "/${ersatz}"; + + # Ports of functions for older nix versions + + # a Nix version of mapAttrs if the built-in doesn't exist + mapAttrs = builtins.mapAttrs or ( + f: set: with builtins; + listToAttrs (map (attr: { name = attr; value = f attr set.${attr}; }) (attrNames set)) + ); + + # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/lists.nix#L295 + range = first: last: if first > last then [ ] else builtins.genList (n: first + n) (last - first + 1); + + # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/strings.nix#L257 + stringToCharacters = s: map (p: builtins.substring p 1 s) (range 0 (builtins.stringLength s - 1)); + + # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/strings.nix#L269 + stringAsChars = f: s: concatStrings (map f (stringToCharacters s)); + concatMapStrings = f: list: concatStrings (map f list); + concatStrings = builtins.concatStringsSep ""; + + # https://github.com/NixOS/nixpkgs/blob/8a9f58a375c401b96da862d969f66429def1d118/lib/attrsets.nix#L331 + optionalAttrs = cond: as: if cond then as else { }; + + # fetchTarball version that is compatible between all the versions of Nix + builtins_fetchTarball = { url, name ? null, sha256 }@attrs: + let + inherit (builtins) lessThan nixVersion fetchTarball; + in + if lessThan nixVersion "1.12" then + fetchTarball ({ inherit url; } // (optionalAttrs (name != null) { inherit name; })) + else + fetchTarball attrs; + + # fetchurl version that is compatible between all the versions of Nix + builtins_fetchurl = { url, name ? null, sha256 }@attrs: + let + inherit (builtins) lessThan nixVersion fetchurl; + in + if lessThan nixVersion "1.12" then + fetchurl ({ inherit url; } // (optionalAttrs (name != null) { inherit name; })) + else + fetchurl attrs; + + # Create the final "sources" from the config + mkSources = config: + mapAttrs + ( + name: spec: + if builtins.hasAttr "outPath" spec + then + abort + "The values in sources.json should not have an 'outPath' attribute" + else + spec // { outPath = replace name (fetch config.pkgs name spec); } + ) + config.sources; + + # The "config" used by the fetchers + mkConfig = + { sourcesFile ? if builtins.pathExists ./sources.json then ./sources.json else null + , sources ? if sourcesFile == null then { } else builtins.fromJSON (builtins.readFile sourcesFile) + , system ? builtins.currentSystem + , pkgs ? mkPkgs sources system + }: rec { + # The sources, i.e. the attribute set of spec name to spec + inherit sources; + + # The "pkgs" (evaluated nixpkgs) to use for e.g. non-builtin fetchers + inherit pkgs; + }; + +in +mkSources (mkConfig { }) // { __functor = _: settings: mkSources (mkConfig settings); } From 4948c2b744808130784b969d51a8a47300b1e464 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Sat, 4 Nov 2023 23:30:46 +0100 Subject: [PATCH 2/2] Improve CI feedback latency by only checking the Agda files The output of the test cases aren't checked anyways so we don't have to waste resources to compile and run `Main`. --- .github/workflows/{build.yml => check.yml} | 8 ++++---- makefile | 3 +++ 2 files changed, 7 insertions(+), 4 deletions(-) rename .github/workflows/{build.yml => check.yml} (70%) diff --git a/.github/workflows/build.yml b/.github/workflows/check.yml similarity index 70% rename from .github/workflows/build.yml rename to .github/workflows/check.yml index ad8e454e..d7c25e7b 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/check.yml @@ -1,4 +1,4 @@ -name: Build the nix derivation +name: Check the Agda files on: push: @@ -16,7 +16,7 @@ jobs: - name: Install Nix with cached packages uses: ibbem/cache-install@b5946e901c509f3478455a3f315e887e254bd36b with: - key: nix-${{ hashFiles('.github/workflows/build.yml', 'default.nix', 'nix/**') }} + key: nix-${{ hashFiles('.github/workflows/check.yml', 'default.nix', 'nix/**') }} nix_file: nix/github-workflow-dependencies.nix - - name: Build - run: nix-build + - name: Check Agda files + run: nix-shell --run 'make check' diff --git a/makefile b/makefile index 99d68ed8..0da7e2f3 100644 --- a/makefile +++ b/makefile @@ -1,5 +1,8 @@ andrun : build run +check: + env AGDA_DIR="./libs" agda src/Main.agda + build: env AGDA_DIR="./libs" agda --compile src/Main.agda