first
This commit is contained in:
commit
06557200bc
|
|
@ -0,0 +1 @@
|
|||
build
|
||||
|
|
@ -0,0 +1,292 @@
|
|||
module TAP
|
||||
|
||||
import public TAP.Options
|
||||
import public Control.Monad.Either
|
||||
import Data.String
|
||||
import Data.List
|
||||
import Data.List.Elem
|
||||
import Data.SnocList
|
||||
import Control.Monad.Reader
|
||||
import Control.Monad.State
|
||||
import Control.ANSI
|
||||
import System
|
||||
|
||||
%default total
|
||||
|
||||
|
||||
public export
|
||||
Info : Type
|
||||
Info = List (String, String)
|
||||
|
||||
private
|
||||
data Result = Tried Bool Info | Skip String | Todo String
|
||||
|
||||
private
|
||||
record TestBase where
|
||||
constructor MakeTest
|
||||
label : String
|
||||
run : IO Result
|
||||
|
||||
|
||||
private
|
||||
toLines1 : (String, String) -> List String
|
||||
toLines1 (k, v) =
|
||||
let vs = lines v in
|
||||
if length vs == 1
|
||||
then ["\{k}: \{v}"]
|
||||
else "\{k}: |" :: map (indent 2) vs
|
||||
|
||||
private
|
||||
toLines : Info -> List String
|
||||
toLines [] = []
|
||||
toLines xs = "---" :: concatMap toLines1 xs <+> ["..."]
|
||||
|
||||
|
||||
public export interface ToInfo e where toInfo : e -> Info
|
||||
|
||||
export ToInfo () where toInfo () = []
|
||||
|
||||
export Show a => ToInfo (List (String, a)) where toInfo = map (map show)
|
||||
|
||||
|
||||
export
|
||||
data Test
|
||||
= One TestBase
|
||||
| Group String (List Test)
|
||||
| Note String
|
||||
|
||||
|
||||
export
|
||||
isRealTest : Test -> Bool
|
||||
isRealTest (One _) = True
|
||||
isRealTest (Group _ _) = True
|
||||
isRealTest (Note _) = False
|
||||
|
||||
|
||||
private
|
||||
result : ToInfo a => Bool -> a -> IO Result
|
||||
result ok = pure . Tried ok . toInfo
|
||||
|
||||
private
|
||||
lazyToIO : Lazy a -> IO a
|
||||
lazyToIO val = primIO $ \w => MkIORes (force val) w
|
||||
|
||||
export
|
||||
testIO : (ToInfo e, ToInfo a) => String -> EitherT e IO a -> Test
|
||||
testIO label act = One $ MakeTest label $ do
|
||||
case !(runEitherT act) of
|
||||
Right val => result True val
|
||||
Left err => result False err
|
||||
|
||||
export
|
||||
test : (ToInfo e, ToInfo a) => String -> Lazy (Either e a) -> Test
|
||||
test label val = testIO label $ MkEitherT $ lazyToIO val
|
||||
|
||||
export
|
||||
todoWith : String -> String -> Test
|
||||
todoWith label reason = One $ MakeTest label $ pure $ Todo reason
|
||||
|
||||
export
|
||||
todo : String -> Test
|
||||
todo label = todoWith label ""
|
||||
|
||||
private
|
||||
makeSkip : String -> String -> Test
|
||||
makeSkip label reason = One $ MakeTest label $ pure $ Skip reason
|
||||
|
||||
export
|
||||
skipWith : Test -> String -> Test
|
||||
skipWith (One t) reason = makeSkip t.label reason
|
||||
skipWith (Group l _) reason = makeSkip l reason
|
||||
skipWith (Note n) _ = Note n
|
||||
|
||||
export
|
||||
skip : Test -> Test
|
||||
skip test = skipWith test ""
|
||||
|
||||
export
|
||||
testThrows : (ToInfo e, Show a) =>
|
||||
String -> (e -> Bool) -> Lazy (Either e a) -> Test
|
||||
testThrows label p act = One $ MakeTest label $ do
|
||||
case !(lazyToIO act) of
|
||||
Left err => if p err then result True () else result False err
|
||||
Right val => result False [("success", val)]
|
||||
|
||||
infix 1 :-
|
||||
export
|
||||
(:-) : String -> List Test -> Test
|
||||
(:-) = Group
|
||||
|
||||
export
|
||||
bailOut : Test
|
||||
bailOut = One $ MakeTest "bail out" $ do
|
||||
putStrLn "Bail out!"
|
||||
exitFailure
|
||||
|
||||
export
|
||||
note : String -> Test
|
||||
note = Note
|
||||
|
||||
|
||||
|
||||
export
|
||||
header : List Test -> String
|
||||
header tests =
|
||||
let count = length $ filter isRealTest tests in
|
||||
"1..\{show count}"
|
||||
|
||||
|
||||
private
|
||||
withPrefix : SnocList String -> TestBase -> Test
|
||||
withPrefix pfx = One . {label $= (makePrefix pfx ++)}
|
||||
where makePrefix = concatMap $ \s => "\{s} ⟫ "
|
||||
|
||||
mutual
|
||||
export
|
||||
flattenWith : SnocList String -> List Test -> List Test
|
||||
flattenWith pfx tests =
|
||||
concatMap (\t => flatten1With pfx (assert_smaller tests t)) tests
|
||||
|
||||
export
|
||||
flatten1With : SnocList String -> Test -> List Test
|
||||
flatten1With pfx (One t) = [withPrefix pfx t]
|
||||
flatten1With pfx (Group x ts) = flattenWith (pfx :< x) ts
|
||||
flatten1With pfx (Note n) = [Note n]
|
||||
|
||||
export
|
||||
flatten : List Test -> List Test
|
||||
flatten = flattenWith [<]
|
||||
|
||||
export
|
||||
flatten1 : Test -> List Test
|
||||
flatten1 = flatten1With [<]
|
||||
|
||||
|
||||
private
|
||||
record RunnerEnv where
|
||||
constructor RE
|
||||
indent : Nat
|
||||
color : Bool
|
||||
|
||||
|
||||
private
|
||||
Runner : Type -> Type
|
||||
Runner = ReaderT RunnerEnv IO
|
||||
|
||||
private
|
||||
putIndentLines : List String -> Runner ()
|
||||
putIndentLines xs = traverse_ (putStrLn . indent (!ask).indent) xs
|
||||
|
||||
private
|
||||
isOk : Bool -> String
|
||||
isOk b = if b then "ok" else "not ok"
|
||||
|
||||
private
|
||||
toBool : Result -> Bool
|
||||
toBool (Tried ok _) = ok
|
||||
toBool _ = True
|
||||
|
||||
|
||||
private
|
||||
numbered : (a -> Bool) -> List a -> List (Nat, a)
|
||||
numbered p = go 1 where
|
||||
go : Nat -> List a -> List (Nat, a)
|
||||
go _ [] = []
|
||||
go i (x :: xs) =
|
||||
if p x then (i, x) :: go (S i) xs
|
||||
else (0, x) :: go i xs
|
||||
|
||||
|
||||
private
|
||||
col : Color -> String -> Runner String
|
||||
col c str = pure $ if (!ask).color then show $ colored c str else str
|
||||
|
||||
private
|
||||
putColor : Color -> String -> Runner ()
|
||||
putColor c str = putIndentLines [!(col c str)]
|
||||
|
||||
private
|
||||
okCol : Bool -> Color
|
||||
okCol True = Green
|
||||
okCol False = Red
|
||||
|
||||
private
|
||||
putOk' : Color -> Bool -> Nat -> String -> Runner ()
|
||||
putOk' c ok index label =
|
||||
putIndentLines [!(col c "\{isOk ok} \{show index}") ++ " - \{label}"]
|
||||
|
||||
private
|
||||
putOk : Bool -> Nat -> String -> Runner ()
|
||||
putOk ok = putOk' (okCol ok) ok
|
||||
|
||||
private
|
||||
putVersion : TAPVersion -> Runner ()
|
||||
putVersion ver = putColor Cyan "TAP version \{show ver}"
|
||||
|
||||
private
|
||||
run1' : (Nat, TestBase) -> Runner Bool
|
||||
run1' (index, test) = do
|
||||
res <- liftIO test.run
|
||||
case res of
|
||||
Tried ok info => do
|
||||
putOk ok index test.label
|
||||
local {indent $= plus 2} $ putIndentLines $ toLines info
|
||||
Skip reason =>
|
||||
putOk' Yellow True index "\{test.label} # skip \{reason}"
|
||||
Todo reason =>
|
||||
putOk' Yellow True index "\{test.label} # todo \{reason}"
|
||||
pure $ toBool res
|
||||
|
||||
mutual
|
||||
private
|
||||
run' : (Nat, Test) -> Runner Bool
|
||||
run' (index, One test) = run1' (index, test)
|
||||
run' (index, Group label tests) = do
|
||||
putIndentLines [!(col Magenta "# Subtest: ") ++ label]
|
||||
res <- local {indent $= plus 4} $ runList tests
|
||||
putOk res index label
|
||||
pure res
|
||||
run' (_, Note note) = do
|
||||
putIndentLines [!(col Magenta "# ") ++ note]
|
||||
pure True
|
||||
|
||||
private
|
||||
runList : List Test -> Runner Bool
|
||||
runList tests = do
|
||||
putColor Cyan $ header tests
|
||||
let tests' = numbered isRealTest tests
|
||||
all id <$> traverse (\t => run' (assert_smaller tests t)) tests'
|
||||
|
||||
|
||||
mutual
|
||||
export
|
||||
filterMatch : Maybe String -> List Test -> List Test
|
||||
filterMatch Nothing tests = tests
|
||||
filterMatch (Just pat) tests =
|
||||
mapMaybe (\t => filterMatch1 pat (assert_smaller tests t)) tests
|
||||
|
||||
export
|
||||
filterMatch1 : String -> Test -> Maybe Test
|
||||
filterMatch1 pat test@(One base) =
|
||||
guard (pat `isInfixOf` base.label) $> test
|
||||
filterMatch1 pat all@(Group label tests) =
|
||||
if pat `isInfixOf` label then Just all else
|
||||
case filterMatch (Just pat) tests of
|
||||
[] => Nothing
|
||||
res => Just $ Group label res
|
||||
filterMatch1 pat note@(Note _) = Just note
|
||||
|
||||
|
||||
export
|
||||
main' : Options -> List Test -> IO ExitCode
|
||||
main' opts tests = do
|
||||
let tests = filterMatch opts.pattern $
|
||||
case opts.version of V13 => flatten tests; V14 => tests
|
||||
let act = do putVersion opts.version; runList tests
|
||||
pure $ if !(runReaderT (RE 0 opts.color) act)
|
||||
then ExitSuccess
|
||||
else ExitFailure 70
|
||||
|
||||
export
|
||||
main : Options -> List Test -> IO ()
|
||||
main opts tests = exitWith !(main' opts tests)
|
||||
|
|
@ -0,0 +1,113 @@
|
|||
module TAP.Options
|
||||
|
||||
import Data.String
|
||||
import System
|
||||
import System.Console.GetOpt
|
||||
|
||||
%default total
|
||||
|
||||
|
||||
public export
|
||||
data TAPVersion = V13 | V14
|
||||
|
||||
export
|
||||
readVersion : String -> Maybe TAPVersion
|
||||
readVersion "13" = Just V13
|
||||
readVersion "14" = Just V14
|
||||
readVersion _ = Nothing
|
||||
|
||||
export Show TAPVersion where show V13 = "13"; show V14 = "14"
|
||||
|
||||
|
||||
public export
|
||||
record Options where
|
||||
constructor Opts
|
||||
version : TAPVersion
|
||||
pattern : Maybe String
|
||||
color : Bool
|
||||
|
||||
export
|
||||
defaultOpts : Options
|
||||
defaultOpts = Opts {
|
||||
version = V13,
|
||||
pattern = Nothing,
|
||||
color = False
|
||||
}
|
||||
|
||||
public export
|
||||
Mod : Type
|
||||
Mod = Options -> IO Options
|
||||
|
||||
|
||||
export
|
||||
failureWith : List String -> IO a
|
||||
failureWith msgs = do
|
||||
traverse_ (\s => putStrLn "# \{s}") msgs
|
||||
putStrLn "\nBail out!"
|
||||
exitFailure
|
||||
|
||||
private
|
||||
setTapVer : String -> Mod
|
||||
setTapVer ver opts =
|
||||
case readVersion ver of
|
||||
Just v => pure $ {version := v} opts
|
||||
Nothing => failureWith ["unrecognised TAP version '\{ver}'"]
|
||||
|
||||
private
|
||||
setPat : String -> Mod
|
||||
setPat str opts = pure $ {pattern := Just str} opts
|
||||
|
||||
mutual
|
||||
export
|
||||
opts : List (OptDescr Mod)
|
||||
opts =
|
||||
[ MkOpt {
|
||||
description = "show this help",
|
||||
shortNames = ['h', '?'], longNames = ["help"],
|
||||
argDescr = NoArg $ const $ failureWith usage
|
||||
},
|
||||
MkOpt {
|
||||
description = "TAP version to output (13 or 14, default 13)",
|
||||
shortNames = ['V'], longNames = ["version"],
|
||||
argDescr = ReqArg setTapVer "VERSION"
|
||||
},
|
||||
MkOpt {
|
||||
description = "only run tests containing STR in their group or label",
|
||||
shortNames = ['F'], longNames = ["filter"],
|
||||
argDescr = ReqArg setPat "STR"
|
||||
},
|
||||
MkOpt {
|
||||
description = "don't colour-code results (default)",
|
||||
shortNames = ['C'], longNames = ["no-color", "no-colour"],
|
||||
argDescr = NoArg $ pure . {color := False}
|
||||
},
|
||||
MkOpt {
|
||||
description = "colour-code results (not TAP compliant)",
|
||||
shortNames = ['c'], longNames = ["color", "colour"],
|
||||
argDescr = NoArg $ pure . {color := True}
|
||||
}
|
||||
]
|
||||
|
||||
export
|
||||
usage : List String
|
||||
usage = assert_total $ "quox test suite" :: lines (usageInfo "" opts)
|
||||
|
||||
|
||||
export
|
||||
makeOpts : List Mod -> IO Options
|
||||
makeOpts = foldlM (\x, f => f x) defaultOpts
|
||||
|
||||
|
||||
export
|
||||
getArgs1 : IO (List String)
|
||||
getArgs1 =
|
||||
case !getArgs of
|
||||
_ :: args => pure args
|
||||
[] => failureWith ["expected getArgs to start with exe name"]
|
||||
|
||||
export
|
||||
getTestOpts : IO Options
|
||||
getTestOpts =
|
||||
case getOpt Permute opts !getArgs1 of
|
||||
MkResult opts [] [] [] => makeOpts opts
|
||||
res => failureWith $ res.errors ++ usage
|
||||
|
|
@ -0,0 +1,34 @@
|
|||
ANTI-CAPITALIST SOFTWARE LICENSE (v 1.4)
|
||||
|
||||
Copyright © 2021 rhiannon morris
|
||||
|
||||
This is anti-capitalist software, released for free use by individuals and
|
||||
organizations that do not operate by capitalist principles.
|
||||
|
||||
Permission is hereby granted, free of charge, to any person or organization
|
||||
(the “User”) obtaining a copy of this software and associated documentation
|
||||
files (the “Software”), to use, copy, modify, merge, distribute, and/or sell
|
||||
copies of the Software, subject to the following conditions:
|
||||
|
||||
1. The above copyright notice and this permission notice shall be included in
|
||||
all copies or modified versions of the Software.
|
||||
|
||||
2. The User is one of the following:
|
||||
a. An individual person, laboring for themselves
|
||||
b. A non-profit organization
|
||||
c. An educational institution
|
||||
d. An organization that seeks shared profit for all of its members, and
|
||||
allows non-members to set the cost of their labor
|
||||
|
||||
3. If the User is an organization with owners, then all owners are workers and
|
||||
all workers are owners with equal equity and/or equal vote.
|
||||
|
||||
4. If the User is an organization, then the User is not law enforcement or
|
||||
military, or working for or under either.
|
||||
|
||||
THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT EXPRESS OR IMPLIED WARRANTY OF ANY
|
||||
KIND, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
|
||||
FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS BE
|
||||
LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF
|
||||
CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
|
||||
SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
|
|
@ -0,0 +1,3 @@
|
|||
(import (fetchTarball "https://github.com/edolstra/flake-compat/archive/master.tar.gz") {
|
||||
src = ./.;
|
||||
}).defaultNix
|
||||
|
|
@ -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": 1652776076,
|
||||
"narHash": "sha256-gzTw/v1vj4dOVbpBSJX4J0DwUR6LIyXo7/SuuTJp1kM=",
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"rev": "04c1b180862888302ddfb2e3ad9eaa63afc60cf8",
|
||||
"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
|
||||
}
|
||||
|
|
@ -0,0 +1,26 @@
|
|||
{ description = "basic test framework for idris 2";
|
||||
|
||||
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 }:
|
||||
flake-utils.lib.eachSystem [ "x86_64-darwin" "x86_64-linux" "i686-linux" ]
|
||||
(system:
|
||||
let
|
||||
pkgs = import nixpkgs {
|
||||
inherit system;
|
||||
overlays = [ idris2-pkgs.overlay ];
|
||||
};
|
||||
inherit (pkgs.idris2-pkgs._builders) idrisPackage devEnv;
|
||||
|
||||
tap = idrisPackage ./. { };
|
||||
in {
|
||||
defaultPackage = tap;
|
||||
packages = { inherit tap; };
|
||||
devShell = pkgs.mkShell { buildInputs = [ (devEnv tap) ]; };
|
||||
}
|
||||
);
|
||||
}
|
||||
Loading…
Reference in New Issue