Add a flake

.github/workflows/nix-ci.yml

@@ -0,0 +1,22 @@
+name: "CI"
+on:
+  pull_request:
+  push:
+jobs:
+  nix-build:
+    name: ${{ matrix.pretty }} with nix (${{ matrix.derivation }})
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        derivation: [scope-hs, scope-lib]
+        include:
+          - pretty: "Build Haskell library"
+            derivation: scope-hs
+          - pretty: "Typecheck with Agda"
+            derivation: scope-lib
+    steps:
+    - uses: actions/checkout@v3
+    - uses: cachix/install-nix-action@v22
+    - uses: DeterminateSystems/magic-nix-cache-action@v2
+    - run: nix build .#${{ matrix.derivation }} --print-build-logs

Makefile

@@ -0,0 +1,32 @@
+AGDA2HS = agda2hs
+FLAGS =
+LIBRARIES =
+
+.PHONY: app alllib clean clean-lib clean-agdai nix-tc nix-build
+
+alllib: lib lib/Scope.hs lib/Scope/All.hs lib/Scope/Core.hs lib/Scope/Diff.hs lib/Scope/In.hs lib/Scope/Split.hs lib/Scope/Sub.hs
+
+# alllib: lib lib/*.hs
+
+lib:
+	mkdir lib
+
+lib/%.hs: src/%.agda
+	$(AGDA2HS) $(FLAGS) $(LIBRARIES) $< -o lib
+
+clean: clean-lib clean-agdai
+
+clean-lib:
+	rm -rf lib
+
+clean-agdai:
+	rm -f src/*.agdai
+
+cabal-build: alllib
+	cabal build
+
+nix-tc:
+	nix build .#scope-lib --print-build-logs
+
+nix-build:
+	nix build .#scope-hs --print-build-logs

flake.nix

@@ -0,0 +1,49 @@
+{
+  description = "Agda scope library";
+
+  inputs.nixpkgs.url = github:NixOS/nixpkgs;
+  inputs.flake-utils.url = github:numtide/flake-utils;
+  inputs.agda2hs = {
+    url = "github:agda/agda2hs";
+    inputs.nixpkgs.follows = "nixpkgs";
+    inputs.flake-utils.follows = "flake-utils";
+  };
+
+  outputs = {self, nixpkgs, flake-utils, agda2hs}:
+    flake-utils.lib.eachDefaultSystem (system:
+      let
+        pkgs = import nixpkgs {inherit system;};
+        agda2hs-lib = agda2hs.packages.${system}.agda2hs-lib;
+        scope-lib = pkgs.agdaPackages.mkDerivation
+          { pname = "scope";
+            meta = {};
+            version = "0.1.0.0";
+            buildInputs = [
+              agda2hs.packages.${system}.agda2hs-lib
+            ];
+            preBuild = ''
+              echo "module Everything where" > Everything.agda
+              find src -name '*.agda' | sed -e 's/src\///;s/\//./g;s/\.agda$//;s/^/import /' >> Everything.agda
+            '';
+            src = ./.;
+          };
+        helper = agda2hs.lib.${system};
+        hpkgs = pkgs.haskell.packages.ghc96;
+        agda2hs-ghc96 = pkgs.callPackage (helper.agda2hs-expr) {
+          inherit self;
+          agda2hs = hpkgs.callPackage (helper.agda2hs-pkg "--jailbreak") {};
+          inherit (hpkgs) ghcWithPackages;
+        };
+        agda2hs-custom = agda2hs-ghc96.withPackages [agda2hs-lib];
+        scope-pkg = import ./scope.nix;
+        scope-hs = pkgs.haskell.packages.ghc94.callPackage scope-pkg {agda2hs = agda2hs-custom;};
+      in {
+        packages = {
+          inherit scope-hs scope-lib;
+          default = scope-hs;
+        };
+        lib = {
+          inherit scope-pkg;
+        };
+      });
+}

scope.nix

@@ -0,0 +1,15 @@
+# this package is produced by calling cabal2nix . in the parent directory
+# and then doing the following:
+# add an agda2hs argument
+# add buildTools = [agda2hs];
+# add preBuild = ''make alllib'';
+{ mkDerivation, base, lib, agda2hs }:
+mkDerivation {
+  pname = "scope";
+  version = "0.1.0.0";
+  src = ./.;
+  buildTools = [agda2hs];
+  preBuild = ''make alllib'';
+  libraryHaskellDepends = [ base ];
+  license = lib.licenses.unlicense;
+}