diff --git a/Makefile b/Makefile deleted file mode 100644 index b0a3136..0000000 --- a/Makefile +++ /dev/null @@ -1,39 +0,0 @@ -all: quox - -NIXFLAGS := --no-warn-dirty - -# these two are real files, but always ask nix if they need remaking -.PHONY: quox -quox: - @echo [build] quox - nix build $(NIXFLAGS) --no-link '.#quox' - ln -sfL $$(nix path-info $(NIXFLAGS) '.#quox')/bin/quox quox - -.PHONY: quox-tests -quox-tests: - @echo [build] quox-tests - nix build $(NIXFLAGS) --no-link '.#quox-tests' - ln -sfL $$(nix path-info $(NIXFLAGS) '.#quox-tests')/bin/quox-tests quox-tests - - -.PHONY: lib -lib: - @echo [build] quox-lib - nix build $(NIXFLAGS) --no-link '.#quox-lib' - -.PHONY: test -test: - nix run $(NIXFLAGS) -- '.#quox-tests' -V 14 -c - -.PHONY: prove -prove: - nix build $(NIXFLAGS) --no-link '.#quox-tests' - prove $$(nix path-info $(NIXFLAGS) '.#quox-tests')/bin/quox-tests - -.PHONY: clean -clean: - @echo [clean] - rm -f quox quox-tests result - rm -rf lib/build main/build tests/build - -.SILENT: diff --git a/default.nix b/default.nix deleted file mode 100644 index c490468..0000000 --- a/default.nix +++ /dev/null @@ -1 +0,0 @@ -(import (fetchTarball "https://github.com/edolstra/flake-compat/archive/master.tar.gz") { src = ./.; }).defaultNix diff --git a/flake.lock b/flake.lock deleted file mode 100644 index f34177c..0000000 --- a/flake.lock +++ /dev/null @@ -1,605 +0,0 @@ -{ - "nodes": { - "Prettier": { - "flake": false, - "locked": { - "lastModified": 1641402353, - "narHash": "sha256-gUE4aoLfXC4FTZWqCj5fAk6PTy/2Z/NihSuspRrDaOk=", - "owner": "Z-snails", - "repo": "prettier", - "rev": "0222ada0be5f6abf5528c8513181f2f4ad117b4b", - "type": "github" - }, - "original": { - "owner": "Z-snails", - "repo": "prettier", - "type": "github" - } - }, - "algae": { - "flake": false, - "locked": { - "lastModified": 1663891753, - "narHash": "sha256-J8tJDJ5xeIMBnTH1Otk/K/ZJJroG8GYUpUMRi0FWuJ8=", - "owner": "avidela", - "repo": "algebraic-data", - "rev": "9b998adc729c4521a3744aa7ba6b1d698d89f588", - "type": "gitlab" - }, - "original": { - "owner": "avidela", - "repo": "algebraic-data", - "type": "gitlab" - } - }, - "collie": { - "flake": false, - "locked": { - "lastModified": 1642687104, - "narHash": "sha256-0GziqzEUDs1tFd5yiu5NECV0nP1aMPe2QxS9oqhmW6I=", - "owner": "ohad", - "repo": "collie", - "rev": "46bff04a8d9a1598fec9b19f515541df16dc64ef", - "type": "github" - }, - "original": { - "owner": "ohad", - "repo": "collie", - "type": "github" - } - }, - "comonad": { - "flake": false, - "locked": { - "lastModified": 1654185277, - "narHash": "sha256-+/sVUjGBU81VKDbZM/Ot4Xi/AqPSFbHQvj29jkYV5aM=", - "owner": "stefan-hoeck", - "repo": "idris2-comonad", - "rev": "35a6e7c2243e73e9c63340e532adaf3197cea3d3", - "type": "github" - }, - "original": { - "owner": "stefan-hoeck", - "repo": "idris2-comonad", - "type": "github" - } - }, - "dom": { - "flake": false, - "locked": { - "lastModified": 1655723854, - "narHash": "sha256-eeKcB+rd0cgp0XRrKKI+Io5nW0Ld45DQu6EOnmCzsR4=", - "owner": "stefan-hoeck", - "repo": "idris2-dom", - "rev": "7916d7a744fa3ec39c4d547de659e0740c98407c", - "type": "github" - }, - "original": { - "owner": "stefan-hoeck", - "repo": "idris2-dom", - "type": "github" - } - }, - "dot-parse": { - "flake": false, - "locked": { - "lastModified": 1653991491, - "narHash": "sha256-zZjgdCHYK8AoDupWjio21uYI1XeupVyhL+V/kzgi/qw=", - "owner": "CodingCellist", - "repo": "idris2-dot-parse", - "rev": "121a46b72f886b52314c858eddda05fbe56a78ac", - "type": "github" - }, - "original": { - "owner": "CodingCellist", - "repo": "idris2-dot-parse", - "type": "github" - } - }, - "effect": { - "flake": false, - "locked": { - "lastModified": 1652479904, - "narHash": "sha256-52rVYBfly6bRY6l48INum+l5kLIHBvoDpCc1veyofaw=", - "owner": "russoul", - "repo": "idris2-effect", - "rev": "b76dce14b79a5f743243a294c3474c6f113f8e3a", - "type": "github" - }, - "original": { - "owner": "russoul", - "repo": "idris2-effect", - "type": "github" - } - }, - "elab-util": { - "flake": false, - "locked": { - "lastModified": 1663162336, - "narHash": "sha256-D7p5CRJ02t/6h4ybnwzPZ8JKzuver+zUrw9tjmFelRI=", - "owner": "stefan-hoeck", - "repo": "idris2-elab-util", - "rev": "e2b9dc3ac5f75286089e48f34223022f2a12d332", - "type": "github" - }, - "original": { - "owner": "stefan-hoeck", - "repo": "idris2-elab-util", - "type": "github" - } - }, - "flake-utils": { - "locked": { - "lastModified": 1676283394, - "narHash": "sha256-XX2f9c3iySLCw54rJ/CZs+ZK6IQy7GXNY4nSOyu2QG4=", - "owner": "numtide", - "repo": "flake-utils", - "rev": "3db36a8b464d0c4532ba1c7dda728f4576d6d073", - "type": "github" - }, - "original": { - "owner": "numtide", - "repo": "flake-utils", - "type": "github" - } - }, - "frex": { - "flake": false, - "locked": { - "lastModified": 1651873603, - "narHash": "sha256-5+SL2WrwfA3P2pIAih7W3+nAPcawbkl0VSFG1JUjRWY=", - "owner": "frex-project", - "repo": "idris-frex", - "rev": "3c39392d088acda901c83af4d75cb3933b2427f9", - "type": "github" - }, - "original": { - "owner": "frex-project", - "repo": "idris-frex", - "type": "github" - } - }, - "fvect": { - "flake": false, - "locked": { - "lastModified": 1651523510, - "narHash": "sha256-h09sQOa2Vn3VQPVRlGi+ze+qShz8M0zoZdGlPbKBHyM=", - "owner": "mattpolzin", - "repo": "idris-fvect", - "rev": "d84969fce38ff8a10b9d261458f4d495e6e0f1ca", - "type": "github" - }, - "original": { - "owner": "mattpolzin", - "repo": "idris-fvect", - "type": "github" - } - }, - "hashable": { - "flake": false, - "locked": { - "lastModified": 1663865679, - "narHash": "sha256-dHRifrvrjSSVypJiKXrJNdl1pzxrfWKrG0EWKCPxDzo=", - "owner": "z-snails", - "repo": "idris2-hashable", - "rev": "5615bd4627fedcb6122e902ea3d4d18575459ceb", - "type": "github" - }, - "original": { - "owner": "z-snails", - "repo": "idris2-hashable", - "type": "github" - } - }, - "hedgehog": { - "flake": false, - "locked": { - "lastModified": 1655715979, - "narHash": "sha256-p0LwUmcxF2whqmku4q0YUYUoDZtutvYni1FbU4HzoWw=", - "owner": "stefan-hoeck", - "repo": "idris2-hedgehog", - "rev": "289c02636ea7a4510320077c81ec72743803a821", - "type": "github" - }, - "original": { - "owner": "stefan-hoeck", - "repo": "idris2-hedgehog", - "type": "github" - } - }, - "idrall": { - "flake": false, - "locked": { - "lastModified": 1661451973, - "narHash": "sha256-q3F55PCJpQu6s3vYzz6M9eP/Yp4mBS0wZRhdER+8Wkc=", - "owner": "alexhumphreys", - "repo": "idrall", - "rev": "86e43e48e5edfe2bafbccd1544777a6bea5eec59", - "type": "github" - }, - "original": { - "owner": "alexhumphreys", - "repo": "idrall", - "type": "github" - } - }, - "idris2": { - "flake": false, - "locked": { - "lastModified": 1667035002, - "narHash": "sha256-0jnBxLMj9b9rac19jIgo9RXkGl2Z0zUalfredKIX1NU=", - "owner": "idris-lang", - "repo": "idris2", - "rev": "c2bcc14e00794b19a7fc7ecc600f5a79b849f031", - "type": "github" - }, - "original": { - "owner": "idris-lang", - "repo": "idris2", - "type": "github" - } - }, - "idris2-pkgs": { - "inputs": { - "Prettier": "Prettier", - "algae": "algae", - "collie": "collie", - "comonad": "comonad", - "dom": "dom", - "dot-parse": "dot-parse", - "effect": "effect", - "elab-util": "elab-util", - "flake-utils": [ - "flake-utils" - ], - "frex": "frex", - "fvect": "fvect", - "hashable": "hashable", - "hedgehog": "hedgehog", - "idrall": "idrall", - "idris2": "idris2", - "indexed": "indexed", - "inigo": "inigo", - "ipkg-to-json": "ipkg-to-json", - "json": "json", - "katla": "katla", - "lsp": "lsp", - "nixpkgs": [ - "nixpkgs" - ], - "odf": "odf", - "pretty-show": "pretty-show", - "python": "python", - "recombine": "recombine", - "rhone": "rhone", - "rhone-js": "rhone-js", - "snocvect": "snocvect", - "sop": "sop", - "tailrec": "tailrec", - "xml": "xml" - }, - "locked": { - "lastModified": 1667146379, - "narHash": "sha256-qGDHORfRc8aamv2fdTqTlR1e6vLxctAfy3hXiUzqTcE=", - "owner": "lizard-business", - "repo": "idris2-pkgs", - "rev": "7f318b3f771e92bc306637dc54e9b0848b6ab244", - "type": "github" - }, - "original": { - "owner": "lizard-business", - "ref": "idris0.6.0", - "repo": "idris2-pkgs", - "type": "github" - } - }, - "indexed": { - "flake": false, - "locked": { - "lastModified": 1659316146, - "narHash": "sha256-xySH74mX3i0Xi7EjXpfr/IUWl8kyB5svV34FVuK3uEk=", - "owner": "mattpolzin", - "repo": "idris-indexed", - "rev": "eb1a019dddcf90412fa8ada1e14574b37a3539c3", - "type": "github" - }, - "original": { - "owner": "mattpolzin", - "repo": "idris-indexed", - "type": "github" - } - }, - "inigo": { - "flake": false, - "locked": { - "lastModified": 1667143799, - "narHash": "sha256-50AGHZ5B2tNaOGjNPt+32khudJxTxkGQ0/Vq4MCwsqE=", - "owner": "lizard-business", - "repo": "Inigo", - "rev": "8bae2a0c02cd88e6e27b98ea10953c86a383033f", - "type": "github" - }, - "original": { - "owner": "lizard-business", - "ref": "idrall-update", - "repo": "Inigo", - "type": "github" - } - }, - "ipkg-to-json": { - "flake": false, - "locked": { - "lastModified": 1634937414, - "narHash": "sha256-LhSmWRpI7vyIQE7QTo38ZTjlqYPVSvV/DIpIxzPmqS0=", - "owner": "claymager", - "repo": "ipkg-to-json", - "rev": "2969b6b83714eeddc31e41577a565778ee5922e6", - "type": "github" - }, - "original": { - "owner": "claymager", - "repo": "ipkg-to-json", - "type": "github" - } - }, - "json": { - "flake": false, - "locked": { - "lastModified": 1662978011, - "narHash": "sha256-G2jKYYZHp1bfM0XrS/f9Er/MGMtMq2VSQetC18VlTLI=", - "owner": "stefan-hoeck", - "repo": "idris2-json", - "rev": "23b925a6b68ba8bd2d0298fc4b94e5cb78242e80", - "type": "github" - }, - "original": { - "owner": "stefan-hoeck", - "repo": "idris2-json", - "type": "github" - } - }, - "katla": { - "flake": false, - "locked": { - "lastModified": 1661665759, - "narHash": "sha256-A+hLAdt6H5igJwooGSoIXm8Jq+iEQTdoNrQnajtdZ9A=", - "owner": "idris-community", - "repo": "katla", - "rev": "a7f9f6c5c605dda745c6a9d847e5cf728b011e6b", - "type": "github" - }, - "original": { - "owner": "idris-community", - "repo": "katla", - "type": "github" - } - }, - "lsp": { - "flake": false, - "locked": { - "lastModified": 1667002591, - "narHash": "sha256-pLh5qBKoi1phvoiaCbpgxs38xaXM1VfD5lQI70I5F38=", - "owner": "idris-community", - "repo": "idris2-lsp", - "rev": "a2603b83124818eedca072269e8883cf8b7a3223", - "type": "github" - }, - "original": { - "owner": "idris-community", - "repo": "idris2-lsp", - "type": "github" - } - }, - "nixpkgs": { - "locked": { - "lastModified": 1677050843, - "narHash": "sha256-3fcFxn58eCtrXrVPeW/nAg6NR5wUERVEf8zOtjPDzuM=", - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "9e0eed654c705c7cafe192a8eba1610217f70544", - "type": "github" - }, - "original": { - "id": "nixpkgs", - "type": "indirect" - } - }, - "odf": { - "flake": false, - "locked": { - "lastModified": 1643726384, - "narHash": "sha256-uIqsQXA/Aoat2snaQJaFqjhCs9gYH28UMS5Emc7Ipk0=", - "owner": "madman-bob", - "repo": "idris2-odf", - "rev": "5eb388c6a19534f9aa1bd24a3b5c42b4ebc1ad44", - "type": "github" - }, - "original": { - "owner": "madman-bob", - "repo": "idris2-odf", - "type": "github" - } - }, - "pretty-show": { - "flake": false, - "locked": { - "lastModified": 1660710482, - "narHash": "sha256-zctFDeFs4a6n3i/QzD+3263tMzJe9nZJQc69ustdfs0=", - "owner": "stefan-hoeck", - "repo": "idris2-pretty-show", - "rev": "f7383c098418e875b6896cd061861a5301bd67c2", - "type": "github" - }, - "original": { - "owner": "stefan-hoeck", - "repo": "idris2-pretty-show", - "type": "github" - } - }, - "python": { - "flake": false, - "locked": { - "lastModified": 1659367107, - "narHash": "sha256-KCc/8907hkJXs0GTKF6IIhss9He8qiClL7wZvyF87cM=", - "owner": "madman-bob", - "repo": "idris2-python", - "rev": "201eb3013600e14484585ba1aeca41936972d957", - "type": "github" - }, - "original": { - "owner": "madman-bob", - "repo": "idris2-python", - "type": "github" - } - }, - "recombine": { - "flake": false, - "locked": { - "lastModified": 1654557256, - "narHash": "sha256-EIatN8eunmLIemEnYCzTKO/sVla5N/OPs6nsB+JvHEw=", - "owner": "avidela", - "repo": "recombine", - "rev": "5ef9613d8df64d3886ded6a4052a0c4c8bc89c93", - "type": "gitlab" - }, - "original": { - "owner": "avidela", - "repo": "recombine", - "type": "gitlab" - } - }, - "rhone": { - "flake": false, - "locked": { - "lastModified": 1655717433, - "narHash": "sha256-ex5Rs6qA8hPD2NAokQtIQWVjsejuWWuruSvs5NmUOeU=", - "owner": "stefan-hoeck", - "repo": "idris2-rhone", - "rev": "a12fa1c65bbfb072e0a4e76e40cd0097d3c4c2e1", - "type": "github" - }, - "original": { - "owner": "stefan-hoeck", - "repo": "idris2-rhone", - "type": "github" - } - }, - "rhone-js": { - "flake": false, - "locked": { - "lastModified": 1666895711, - "narHash": "sha256-DdFrEWZk35VYlNMGAiiERzkDOlkQMAaJTzqjNxJ3EvM=", - "owner": "stefan-hoeck", - "repo": "idris2-rhone-js", - "rev": "528b9fd32ea632346764b1e70bebd3f50881330e", - "type": "github" - }, - "original": { - "owner": "stefan-hoeck", - "repo": "idris2-rhone-js", - "type": "github" - } - }, - "root": { - "inputs": { - "flake-utils": "flake-utils", - "idris2-pkgs": "idris2-pkgs", - "nixpkgs": "nixpkgs", - "tap": "tap" - } - }, - "snocvect": { - "flake": false, - "locked": { - "lastModified": 1651518488, - "narHash": "sha256-oIFb2yKKxIDHNCdr0ZkHPuV7KeX0m6m9xBwRFPqz7iw=", - "owner": "mattpolzin", - "repo": "idris-snocvect", - "rev": "f6148c3d06c7a9989062a2425f925fc844468215", - "type": "github" - }, - "original": { - "owner": "mattpolzin", - "repo": "idris-snocvect", - "type": "github" - } - }, - "sop": { - "flake": false, - "locked": { - "lastModified": 1660672216, - "narHash": "sha256-HO05C8KLmx9FIQDQ1IpSUZIDxL4oLPJNinbmCXgBZlk=", - "owner": "stefan-hoeck", - "repo": "idris2-sop", - "rev": "7b4c1189c8c9df5b34e5b4aec3aecef43dc8aa3c", - "type": "github" - }, - "original": { - "owner": "stefan-hoeck", - "repo": "idris2-sop", - "type": "github" - } - }, - "tailrec": { - "flake": false, - "locked": { - "lastModified": 1654185733, - "narHash": "sha256-ONcY1MFWtctuVM8RtIl6ikIOgqfdeV+ECJiNf1FfytM=", - "owner": "stefan-hoeck", - "repo": "idris2-tailrec", - "rev": "ae27e2ed09ef3d880801899cfc26f470f5b71332", - "type": "github" - }, - "original": { - "owner": "stefan-hoeck", - "repo": "idris2-tailrec", - "type": "github" - } - }, - "tap": { - "inputs": { - "flake-utils": [ - "flake-utils" - ], - "idris2-pkgs": [ - "idris2-pkgs" - ], - "nixpkgs": [ - "nixpkgs" - ] - }, - "locked": { - "lastModified": 1677099362, - "narHash": "sha256-egayKOaeCief0149Ht5tJlH6mu5GnP7mwjsX0GGOfxo=", - "ref": "main", - "rev": "4dba693a5fe47fc0304053c4c1237fa373379c4f", - "revCount": 14, - "type": "git", - "url": "https://git.rhiannon.website/rhi/idris2-tap" - }, - "original": { - "ref": "main", - "type": "git", - "url": "https://git.rhiannon.website/rhi/idris2-tap" - } - }, - "xml": { - "flake": false, - "locked": { - "lastModified": 1637939752, - "narHash": "sha256-yYJBhPfwYoi7amlHmeNGrVCOAc3BjZpKTCd9wDs3XEM=", - "owner": "madman-bob", - "repo": "idris2-xml", - "rev": "1292ccfcd58c551089ef699e4560343d5c473d64", - "type": "github" - }, - "original": { - "owner": "madman-bob", - "repo": "idris2-xml", - "type": "github" - } - } - }, - "root": "root", - "version": 7 -} diff --git a/flake.nix b/flake.nix deleted file mode 100644 index 1bd863e..0000000 --- a/flake.nix +++ /dev/null @@ -1,59 +0,0 @@ -{ description = "quox: quantitative extensional type theory"; - - inputs = { - nixpkgs.url = "nixpkgs"; - flake-utils.url = "github:numtide/flake-utils"; - - idris2-pkgs = { - url = "github:lizard-business/idris2-pkgs?ref=idris0.6.0"; # [fixme] - # url = "github:claymager/idris2-pkgs"; - inputs.nixpkgs.follows = "nixpkgs"; - inputs.flake-utils.follows = "flake-utils"; - }; - - tap = { - url = "git+https://git.rhiannon.website/rhi/idris2-tap?ref=main"; - inputs.nixpkgs.follows = "nixpkgs"; - inputs.flake-utils.follows = "flake-utils"; - inputs.idris2-pkgs.follows = "idris2-pkgs"; - }; - }; - - outputs = { self, nixpkgs, idris2-pkgs, flake-utils, tap }: - let - packagePaths = { - quox-lib = ./lib; - quox = ./exe; - quox-tests = ./tests; - }; - - extraDeps = [ tap ]; - - systems = with flake-utils.lib.system; - [ x86_64-darwin x86_64-linux i686-linux ]; - in - with builtins; - flake-utils.lib.eachSystem systems (system: - let - basePkgs = import nixpkgs { - inherit system; - overlays = [ idris2-pkgs.overlay ]; - }; - builders = basePkgs.idris2-pkgs._builders; - - extraDepPkgs = - foldl' (acc: pkg: acc // pkg.packages.${system}) { } extraDeps; - mkPackage = name: path: - builders.idrisPackage path { extraPkgs = extraDepPkgs // packages; }; - mkDevShell = _: pkg: - basePkgs.mkShell { buildInputs = [ (builders.devEnv pkg) ]; }; - - packages = mapAttrs mkPackage packagePaths; - devShells = mapAttrs mkDevShell packages; - in { - inherit packages devShells; - defaultPackage = packages.quox; - devShell = devShells.quox-lib; - } - ); -} diff --git a/pack.toml b/pack.toml new file mode 100644 index 0000000..92fe5db --- /dev/null +++ b/pack.toml @@ -0,0 +1,22 @@ +collection = "nightly-230301" + +[custom.all.tap] +type = "git" +url = "https://git.rhiannon.website/rhi/idris2-tap.git" +commit = "latest:main" +ipkg = "tap.ipkg" + +[custom.all.quox-lib] +type = "local" +path = "./lib" +ipkg = "quox-lib.ipkg" + +[custom.all.quox] +type = "local" +path = "./exe" +ipkg = "quox.ipkg" + +[custom.all.quox-tests] +type = "local" +path = "./tests" +ipkg = "quox-tests.ipkg"