From 7f415328a295d69f05350b833e18427ecd375335 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 4 May 2022 17:09:49 +0200 Subject: [PATCH] wip nix --- .gitignore | 1 - default.nix | 1 + exe/quox-exe.ipkg | 8 + exe/sirdi.json | 14 - exe/src/Main.idr | 1 + flake.lock | 575 ++++++++++++++++++++++++++++++++++++++++++ flake.nix | 30 +++ quox.ipkg | 37 +++ sirdi.json | 55 ---- tests/quox-tests.ipkg | 7 + tests/sirdi.json | 21 -- tests/src/Options.idr | 8 +- tests/src/TAP.idr | 1 + tests/src/Tests.idr | 2 +- 14 files changed, 667 insertions(+), 94 deletions(-) create mode 100644 default.nix create mode 100644 exe/quox-exe.ipkg delete mode 100644 exe/sirdi.json create mode 100644 flake.lock create mode 100644 flake.nix create mode 100644 quox.ipkg delete mode 100644 sirdi.json create mode 100644 tests/quox-tests.ipkg delete mode 100644 tests/sirdi.json diff --git a/.gitignore b/.gitignore index 202b75d..6c59b33 100644 --- a/.gitignore +++ b/.gitignore @@ -1,7 +1,6 @@ .build build depends -*.ipkg *~ quox quox-tests diff --git a/default.nix b/default.nix new file mode 100644 index 0000000..c490468 --- /dev/null +++ b/default.nix @@ -0,0 +1 @@ +(import (fetchTarball "https://github.com/edolstra/flake-compat/archive/master.tar.gz") { src = ./.; }).defaultNix diff --git a/exe/quox-exe.ipkg b/exe/quox-exe.ipkg new file mode 100644 index 0000000..0d38492 --- /dev/null +++ b/exe/quox-exe.ipkg @@ -0,0 +1,8 @@ +package quox-exe +version = 0 + +depends = base, contrib, elab-util, sop, quox + +executable = quox +sourcedir = "src" +main = Main diff --git a/exe/sirdi.json b/exe/sirdi.json deleted file mode 100644 index 54c64df..0000000 --- a/exe/sirdi.json +++ /dev/null @@ -1,14 +0,0 @@ -[ - { - "name" : "quox-exe", - - "deps" : [ - { "name" : "base", "legacy" : true }, - { "name" : "contrib", "legacy" : true }, - { "name" : "quox", "local" : ".." } - ], - - "main" : "Main", - "modules" : ["Main"] - } -] diff --git a/exe/src/Main.idr b/exe/src/Main.idr index 9544f88..a61a488 100644 --- a/exe/src/Main.idr +++ b/exe/src/Main.idr @@ -9,6 +9,7 @@ import public Quox.Typechecker import Data.Nat import Data.Vect +import Data.List import Control.ANSI diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..d2fb8af --- /dev/null +++ b/flake.lock @@ -0,0 +1,575 @@ +{ + "nodes": { + "Prettier": { + "flake": false, + "locked": { + "lastModified": 1639310097, + "narHash": "sha256-+eSLEJDuy2ZRkh1h0Y5IF6RUeHEcWhAHpWhwdwW65f0=", + "owner": "Z-snails", + "repo": "prettier", + "rev": "4a90663b1d586f6d6fce25873aa0f0d7bc633b89", + "type": "github" + }, + "original": { + "owner": "Z-snails", + "repo": "prettier", + "type": "github" + } + }, + "collie": { + "flake": false, + "locked": { + "lastModified": 1631011321, + "narHash": "sha256-goYctB+WBoLgsbjA0DlqGjD8i9wr1K0lv0agqpuwflU=", + "owner": "ohad", + "repo": "collie", + "rev": "ed2eda5e04fbd02a7728e915d396e14cc7ec298e", + "type": "github" + }, + "original": { + "owner": "ohad", + "repo": "collie", + "type": "github" + } + }, + "comonad": { + "flake": false, + "locked": { + "lastModified": 1638093386, + "narHash": "sha256-kxmN6XuszFLK2i76C6LSGHe5XxAURFu9NpzJbi3nodk=", + "owner": "stefan-hoeck", + "repo": "idris2-comonad", + "rev": "06d6b551db20f1f940eb24c1dae051c957de97ad", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-comonad", + "type": "github" + } + }, + "dom": { + "flake": false, + "locked": { + "lastModified": 1639041519, + "narHash": "sha256-4ZYc0qaUEVARxhWuH3JgejIeT+GEDNxdS6zIGhBCk34=", + "owner": "stefan-hoeck", + "repo": "idris2-dom", + "rev": "01ab52d0ffdb3b47481413a949b8f0c0688c97e4", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-dom", + "type": "github" + } + }, + "dot-parse": { + "flake": false, + "locked": { + "lastModified": 1638264571, + "narHash": "sha256-VJQITz+vuQgl5HwR5QdUGwN8SRtGcb2/lJaAVfFbiSk=", + "owner": "CodingCellist", + "repo": "idris2-dot-parse", + "rev": "48fbda8bf8adbaf9e8ebd6ea740228e4394154d9", + "type": "github" + }, + "original": { + "owner": "CodingCellist", + "repo": "idris2-dot-parse", + "type": "github" + } + }, + "effect": { + "flake": false, + "locked": { + "lastModified": 1637477153, + "narHash": "sha256-Ta2Vogg/IiSBkfhhD57jjPTEf3S4DOiVRmof38hmwlM=", + "owner": "russoul", + "repo": "idris2-effect", + "rev": "ea1daf53b2d7e52f9917409f5653adc557f0ee1a", + "type": "github" + }, + "original": { + "owner": "russoul", + "repo": "idris2-effect", + "type": "github" + } + }, + "elab-util": { + "flake": false, + "locked": { + "lastModified": 1639041013, + "narHash": "sha256-K61s/xifFiTDXJTak5NZmZL6757CTYCY+TGywRZMD7M=", + "owner": "stefan-hoeck", + "repo": "idris2-elab-util", + "rev": "7a381c7c5dc3adb7b97c8b8be17e4fb4cc63027d", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-elab-util", + "type": "github" + } + }, + "flake-utils": { + "locked": { + "lastModified": 1649676176, + "narHash": "sha256-OWKJratjt2RW151VUlJPRALb7OU2S5s+f0vLj4o1bHM=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "a4b154ebbdc88c8498a5c7b01589addc9e9cb678", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "flake-utils_2": { + "locked": { + "lastModified": 1638122382, + "narHash": "sha256-sQzZzAbvKEqN9s0bzWuYmRaA03v40gaJ4+iL1LXjaeI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "74f7e4319258e287b0f9cb95426c9853b282730b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "frex": { + "flake": false, + "locked": { + "lastModified": 1637410704, + "narHash": "sha256-BthU1t++n0ZvS76p0fCHsE33QSoXYxf0hMUSKajDY8w=", + "owner": "frex-project", + "repo": "idris-frex", + "rev": "22c480e879c757a5cebca7bb555ec3d21ae3ac28", + "type": "github" + }, + "original": { + "owner": "frex-project", + "repo": "idris-frex", + "type": "github" + } + }, + "fvect": { + "flake": false, + "locked": { + "lastModified": 1633247988, + "narHash": "sha256-zElIze03XpcrYL4H5Aj0ZGNplJGbtOx+iWnivJMzHm0=", + "owner": "mattpolzin", + "repo": "idris-fvect", + "rev": "1c5e3761e0cd83e711a3535ef9051bea45e6db3f", + "type": "github" + }, + "original": { + "owner": "mattpolzin", + "repo": "idris-fvect", + "type": "github" + } + }, + "hashable": { + "flake": false, + "locked": { + "lastModified": 1633965157, + "narHash": "sha256-Dggf5K//RCZ7uvtCyeiLNJS6mm+8/n0RFW3zAc7XqPg=", + "owner": "z-snails", + "repo": "idris2-hashable", + "rev": "d6fec8c878057909b67f3d4da334155de4f37907", + "type": "github" + }, + "original": { + "owner": "z-snails", + "repo": "idris2-hashable", + "type": "github" + } + }, + "hedgehog": { + "flake": false, + "locked": { + "lastModified": 1639041435, + "narHash": "sha256-893cPy7gGSQpVmm9co3QCpWsgjukafZHy8YFk9xts30=", + "owner": "stefan-hoeck", + "repo": "idris2-hedgehog", + "rev": "a66b1eb0bf84c4a7b743cfb217be69866bc49ad8", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-hedgehog", + "type": "github" + } + }, + "idrall": { + "flake": false, + "locked": { + "lastModified": 1636495701, + "narHash": "sha256-aOdCRd4XsSxwqVGta1adlZBy8TVTxTwFDnJ1dyMZK8M=", + "owner": "alexhumphreys", + "repo": "idrall", + "rev": "13ef174290169d05c9e9abcd77c53412e3e0c944", + "type": "github" + }, + "original": { + "owner": "alexhumphreys", + "ref": "13ef174", + "repo": "idrall", + "type": "github" + } + }, + "idris-server": { + "flake": false, + "locked": { + "lastModified": 1634507315, + "narHash": "sha256-ulo23yLJXsvImoMB/1C6yRRTqmn/Odo+aUaVi+tUhJo=", + "owner": "avidela", + "repo": "idris-server", + "rev": "661a4ecf0fadaa2bd79c8e922c2d4f79b0b7a445", + "type": "gitlab" + }, + "original": { + "owner": "avidela", + "repo": "idris-server", + "type": "gitlab" + } + }, + "idris2": { + "flake": false, + "locked": { + "lastModified": 1639427352, + "narHash": "sha256-C1K2FM1Kio8vi9FTrivdacYCX4cywIsLBeNCsZ6ft4g=", + "owner": "idris-lang", + "repo": "idris2", + "rev": "36918e618646177b1e0c2fd01f21cc8d04d9da30", + "type": "github" + }, + "original": { + "owner": "idris-lang", + "repo": "idris2", + "type": "github" + } + }, + "idris2-pkgs": { + "inputs": { + "Prettier": "Prettier", + "collie": "collie", + "comonad": "comonad", + "dom": "dom", + "dot-parse": "dot-parse", + "effect": "effect", + "elab-util": "elab-util", + "flake-utils": "flake-utils_2", + "frex": "frex", + "fvect": "fvect", + "hashable": "hashable", + "hedgehog": "hedgehog", + "idrall": "idrall", + "idris-server": "idris-server", + "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", + "rhone": "rhone", + "rhone-js": "rhone-js", + "snocvect": "snocvect", + "sop": "sop", + "tailrec": "tailrec", + "xml": "xml" + }, + "locked": { + "lastModified": 1642030375, + "narHash": "sha256-J1uXnpPR72mjFjLBuYcvDHStBxVya6/MjBNNwqxGeD0=", + "owner": "claymager", + "repo": "idris2-pkgs", + "rev": "ac33a49d4d4bd2b50fddb040cd889733a02c8f09", + "type": "github" + }, + "original": { + "owner": "claymager", + "repo": "idris2-pkgs", + "type": "github" + } + }, + "indexed": { + "flake": false, + "locked": { + "lastModified": 1638685238, + "narHash": "sha256-FceB7o88yKYzjTfRC6yfhOL6oDPMmCQAsJZu/pjE2uA=", + "owner": "mattpolzin", + "repo": "idris-indexed", + "rev": "ff3ba99b0063da6a74c96178e7f3c58a4ac1693e", + "type": "github" + }, + "original": { + "owner": "mattpolzin", + "repo": "idris-indexed", + "type": "github" + } + }, + "inigo": { + "flake": false, + "locked": { + "lastModified": 1637596767, + "narHash": "sha256-LNx30LO0YWDVSPTxRLWGTFL4f3d5ANG6c60WPdmiYdY=", + "owner": "idris-community", + "repo": "Inigo", + "rev": "57f5b5c051222d8c630010a0a3cf7d7138910127", + "type": "github" + }, + "original": { + "owner": "idris-community", + "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": 1639041459, + "narHash": "sha256-TP/V1jBBP1hFPm/cJ5O2EJiaNoZ19KvBOAI0S9lvAR4=", + "owner": "stefan-hoeck", + "repo": "idris2-json", + "rev": "7c0c028acad0ba0b63b37b92199f37e6ec73864a", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-json", + "type": "github" + } + }, + "katla": { + "flake": false, + "locked": { + "lastModified": 1636542431, + "narHash": "sha256-X83NA/P3k1iPcBa8g5z8JldEmFEz/jxVeViJX0/FikY=", + "owner": "idris-community", + "repo": "katla", + "rev": "d841ec243f96b4762074211ee81033e28884c858", + "type": "github" + }, + "original": { + "owner": "idris-community", + "repo": "katla", + "type": "github" + } + }, + "lsp": { + "flake": false, + "locked": { + "lastModified": 1639486283, + "narHash": "sha256-po396FnUu8iqiipwPxqpFZEU4rtpX3jnt3cySwjLsH8=", + "owner": "idris-community", + "repo": "idris2-lsp", + "rev": "7ebb6caf6bb4b57c5107579aba2b871408e6f183", + "type": "github" + }, + "original": { + "owner": "idris-community", + "repo": "idris2-lsp", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1639213685, + "narHash": "sha256-Evuobw7o9uVjAZuwz06Al0fOWZ5JMKOktgXR0XgWBtg=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "453bcb8380fd1777348245b3c44ce2a2b93b2e2d", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "nixpkgs-21.11-darwin", + "repo": "nixpkgs", + "type": "github" + } + }, + "odf": { + "flake": false, + "locked": { + "lastModified": 1638184051, + "narHash": "sha256-usSdPx+UqOGImHHdHcrytdzi2LXtIRZuUW0fkD/Wwnk=", + "owner": "madman-bob", + "repo": "idris2-odf", + "rev": "d2f532437321c8336f1ca786b44b6ebef4117126", + "type": "github" + }, + "original": { + "owner": "madman-bob", + "repo": "idris2-odf", + "type": "github" + } + }, + "pretty-show": { + "flake": false, + "locked": { + "lastModified": 1639041411, + "narHash": "sha256-BzEe1fpX+lqGEk8b1JZoQT1db5I7s7SZnLCttRVGXdY=", + "owner": "stefan-hoeck", + "repo": "idris2-pretty-show", + "rev": "a4bc6156b9dac43699f87504cbdb8dada5627863", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-pretty-show", + "type": "github" + } + }, + "python": { + "flake": false, + "locked": { + "lastModified": 1635936936, + "narHash": "sha256-c9mcMApN0qgu0AXQVu0V+NXt2poP258wCPkyvtQvv4I=", + "owner": "madman-bob", + "repo": "idris2-python", + "rev": "0eab028933c65bebe744e879881416f5136d6943", + "type": "github" + }, + "original": { + "owner": "madman-bob", + "repo": "idris2-python", + "type": "github" + } + }, + "rhone": { + "flake": false, + "locked": { + "lastModified": 1639041532, + "narHash": "sha256-2g43shlWQIT/1ogesUBUBV9N8YiD3RwaCbbhdKLVp1s=", + "owner": "stefan-hoeck", + "repo": "idris2-rhone", + "rev": "c4d828b0b8efea495d9a5f1e842a9c67cad57724", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-rhone", + "type": "github" + } + }, + "rhone-js": { + "flake": false, + "locked": { + "lastModified": 1639041546, + "narHash": "sha256-ddWVsSRbfA6ghmwiRMzDpHBPM+esGdutuqm1qQZgs88=", + "owner": "stefan-hoeck", + "repo": "idris2-rhone-js", + "rev": "520dd59549f5b14075045314b6805c7492ed636e", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-rhone-js", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "idris2-pkgs": "idris2-pkgs", + "nixpkgs": [ + "idris2-pkgs", + "nixpkgs" + ] + } + }, + "snocvect": { + "flake": false, + "locked": { + "lastModified": 1641633224, + "narHash": "sha256-6zTU4sDzd/R/dFCTNZaX41H4L3/USGLFghMS0Oc9liY=", + "owner": "mattpolzin", + "repo": "idris-snocvect", + "rev": "ff1e7afba360a62f7e522e9bbb856096a79702c4", + "type": "github" + }, + "original": { + "owner": "mattpolzin", + "repo": "idris-snocvect", + "type": "github" + } + }, + "sop": { + "flake": false, + "locked": { + "lastModified": 1639041379, + "narHash": "sha256-PDTf1Wx6EygiWszguvoVPiqIISYFLabI4e0lXHlrjcA=", + "owner": "stefan-hoeck", + "repo": "idris2-sop", + "rev": "e4354d1883cd73616019457cb9ebf864d99df6a0", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-sop", + "type": "github" + } + }, + "tailrec": { + "flake": false, + "locked": { + "lastModified": 1637146655, + "narHash": "sha256-0yi7MQIrISPvAwkgDC1M5PHDEeVyIaISF0HjKDaT0Rw=", + "owner": "stefan-hoeck", + "repo": "idris2-tailrec", + "rev": "dd0bc6381b3a2e69aa37f9a8c1b165d4b1516ad7", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-tailrec", + "type": "github" + } + }, + "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 new file mode 100644 index 0000000..8084b98 --- /dev/null +++ b/flake.nix @@ -0,0 +1,30 @@ +{ description = "quox: quantitative extensional type theory"; + + inputs = { + flake-utils.url = "github:numtide/flake-utils"; + idris2-pkgs.url = "github:claymager/idris2-pkgs"; + nixpkgs.follows = "idris2-pkgs/nixpkgs"; + }; + + outputs = { self, nixpkgs, idris2-pkgs, flake-utils }: + let systems = [ "x86_64-darwin" "x86_64-linux" "i686-linux" ]; in + flake-utils.lib.eachSystem systems (system: + let + pkgs = import nixpkgs { + inherit system; + overlays = [ idris2-pkgs.overlay ]; + }; + inherit (pkgs.idris2-pkgs._builders) idrisPackage devEnv; + quox = idrisPackage ./. { }; + quox-exe = idrisPackage ./exe { extraPkgs.quox = quox; }; + quox-tests = idrisPackage ./tests { extraPkgs.quox = quox; }; + in + { + defaultPackage = quox-exe; + + packages = { inherit quox quox-exe quox-tests; }; + + devShell = pkgs.mkShell { buildInputs = [ (devEnv quox) ]; }; + } + ); +} diff --git a/quox.ipkg b/quox.ipkg new file mode 100644 index 0000000..3a4b0d2 --- /dev/null +++ b/quox.ipkg @@ -0,0 +1,37 @@ +package quox +version = 0 + +authors = "rhiannon morris" +sourceloc = "https://git.rhiannon.website/rhi/quox" +license = "acsl" + +depends = base, contrib, elab-util, sop + +sourcedir = "src" +modules = + Quox.Error, + Quox.NatExtra, + Quox.OPE, + Quox.Pretty, + Quox.Syntax, + Quox.Syntax.Dim, + Quox.Syntax.DimEq, + Quox.Syntax.Qty, + Quox.Syntax.Shift, + Quox.Syntax.Subst, + Quox.Syntax.Term, + Quox.Syntax.Term.Base, + Quox.Syntax.Term.Pretty, + Quox.Syntax.Term.Reduce, + Quox.Syntax.Term.Split, + Quox.Syntax.Term.Subst, + Quox.Syntax.Universe, + Quox.Syntax.Var, + Quox.Token, + Quox.Lexer, + Quox.Context, + Quox.Equal, + Quox.Name, + Quox.Reduce, + Quox.Typing, + Quox.Typechecker diff --git a/sirdi.json b/sirdi.json deleted file mode 100644 index c84ae65..0000000 --- a/sirdi.json +++ /dev/null @@ -1,55 +0,0 @@ -[ - { - "name" : "quox", - "version" : "0.0.0", - "passthru": { - "license" : "acsl", - "authors" : ["rhiannon morris"], - "sourceloc" : "https://git.rhiannon.website/rhi/quox" - }, - - "deps" : [ - { "name" : "base", "legacy" : true }, - { "name" : "contrib", "legacy" : true }, - { "name" : "sop", - "git" : { - "url" : "https://git.rhiannon.website/rhi/idris2-sop", - "commit" : "defdbc74a28104a32149922ed9f9ee70099d4f59" - } - } - ], - - "modules" : [ - "Quox.Error", - "Quox.NatExtra", - "Quox.OPE", - "Quox.Pretty", - - "Quox.Syntax", - "Quox.Syntax.Dim", - "Quox.Syntax.DimEq", - "Quox.Syntax.Qty", - "Quox.Syntax.Shift", - "Quox.Syntax.Subst", - "Quox.Syntax.Term", - "Quox.Syntax.Term.Base", - "Quox.Syntax.Term.Pretty", - "Quox.Syntax.Term.Reduce", - "Quox.Syntax.Term.Split", - "Quox.Syntax.Term.Subst", - "Quox.Syntax.Universe", - "Quox.Syntax.Var", - - "Quox.Token", - "Quox.Lexer", - - "Quox.Context", - "Quox.Equal", - "Quox.Name", - "Quox.Reduce", - - "Quox.Typing", - "Quox.Typechecker" - ] - } -] diff --git a/tests/quox-tests.ipkg b/tests/quox-tests.ipkg new file mode 100644 index 0000000..1fd985e --- /dev/null +++ b/tests/quox-tests.ipkg @@ -0,0 +1,7 @@ +package quox-tests + +depends = base, contrib, elab-util, sop, quox + +executable = quox-tests +sourcedir = "src" +main = Tests diff --git a/tests/sirdi.json b/tests/sirdi.json deleted file mode 100644 index 58e730a..0000000 --- a/tests/sirdi.json +++ /dev/null @@ -1,21 +0,0 @@ -[ - { - "name" : "quox-tests", - - "deps" : [ - { "name" : "base", "legacy" : true }, - { "name" : "contrib", "legacy" : true }, - { "name" : "quox", "local" : ".." } - ], - - "main" : "Tests", - "modules" : [ - "Tests", - "Options", - "TAP", - - "Tests.Lexer", - "Tests.Equal" - ] - } -] diff --git a/tests/src/Options.idr b/tests/src/Options.idr index 5336560..969d6bf 100644 --- a/tests/src/Options.idr +++ b/tests/src/Options.idr @@ -30,11 +30,15 @@ getArgs1 : IO (List String) getArgs1 = case !getArgs of _ :: args => pure args - [] => die "expecting getArgs to start with exe name" + [] => do + putStrLn "expecting getArgs to start with exe name" + exitFailure export getTestOpts : IO Options getTestOpts = case getOpt Permute opts !getArgs1 of MkResult opts [] [] [] => pure $ makeOpts opts - res => die $ unlines $ res.errors ++ [usageInfo "quox test suite" opts] + res => do + traverse_ putStrLn $ res.errors ++ [usageInfo "quox test suite" opts] + exitFailure diff --git a/tests/src/TAP.idr b/tests/src/TAP.idr index 3f8d63d..0918201 100644 --- a/tests/src/TAP.idr +++ b/tests/src/TAP.idr @@ -5,6 +5,7 @@ import public Quox.Error import Data.String import Data.List.Elem +import Data.SnocList import Control.Monad.Reader import Control.Monad.State import System diff --git a/tests/src/Tests.idr b/tests/src/Tests.idr index b24b7fe..1a200ee 100644 --- a/tests/src/Tests.idr +++ b/tests/src/Tests.idr @@ -17,5 +17,5 @@ main = do go <- case opts.tapVersion of "13" => pure TAP.mainFlat "14" => pure TAP.main - _ => die "unrecognised TAP version; use 13 or 14" + _ => do putStrLn "unrecognised TAP version; use 13 or 14"; exitFailure go allTests