git.iko.soy/Idris-dev
on master help sign in
Added simple benchmark system
86fc1a1Edwin Brady
benchmarks/ALLnew file+1
compare with master
unifiedsplit
@@ -0,0 +1 @@
1+trivial/sortvec 2000
benchmarks/READMEnew file+21
@@ -0,0 +1,21 @@
1+Benchmarks
2+----------
3+
4+To run:
5+
6+$ ./build.pl -- builds all benchmark binaries
7+$ ./run.pl -- runs all benchmarks
8+
9+Adding a test
10+-------------
11+
12+Add a line to the 'ALL' file of the following form:
13+
14+dir/main arg
15+
16+where 'dir' is the directory the benchmark lives in, 'main' is the name of the
17+ipkg file and executable (these must be the same), 'arg' is the input to give
18+to the binary.
19+
20+It is assumed that all benchmarks take exactly one argument, which helps to
21+ensure that they are not simply doing all the work at compile time.
benchmarks/build.plnew file+14
@@ -0,0 +1,14 @@
1+#!/usr/bin/perl
2+
3+$bmarks = `cat ALL`;
4+@bm = split(/\n/, $bmarks);
5+
6+foreach $b (@bm) {
7+ if ($b =~ /([a-zA-Z0-9]+)\/([a-zA-Z0-9]+)\s+(.*)/) {
8+ print "Building $1 / $2\n";
9+ chdir $1;
10+ system("idris --clean $2.ipkg");
11+ system("idris --build $2.ipkg");
12+ chdir "..";
13+ }
14+}
benchmarks/run.plnew file+24
@@ -0,0 +1,24 @@
1+#!/usr/bin/perl
2+
3+$bmarks = `cat ALL`;
4+@bm = split(/\n/, $bmarks);
5+
6+$total = 0;
7+
8+foreach $b (@bm) {
9+ if ($b =~ /([a-zA-Z0-9]+)\/([a-zA-Z0-9]+)\s+(.*)/) {
10+ #print "Running $1 $2\n";
11+ chdir $1;
12+ $result = `/usr/bin/time ./$2 $3 2> .times`;
13+ $time = `cat .times`;
14+ chdir "..";
15+ #print $time;
16+ @timeflds = split(/\s+/, $time);
17+ $user = $timeflds[3];
18+ print "$1 / $2 $user\n";
19+ $total += $user;
20+ }
21+}
22+
23+print "\nTOTAL $total\n";
24+
benchmarks/trivial/sortvec.idrnew file+24
@@ -0,0 +1,24 @@
1+module Main
2+
3+import System
4+import Effect.Random
5+
6+total
7+insert : Ord a => a -> Vect n a -> Vect (S n) a
8+insert x [] = [x]
9+insert x (y :: ys) = if (x < y) then x :: y :: ys else y :: insert x ys
10+
11+vsort : Ord a => Vect n a -> Vect n a
12+vsort [] = []
13+vsort (x :: xs) = insert x (vsort xs)
14+
15+mkSortVec : (n : Nat) -> Eff m [RND] (Vect n Int)
16+mkSortVec Z = return []
17+mkSortVec (S k) = return (fromInteger !(rndInt 0 10000) :: !(mkSortVec k))
18+
19+main : IO ()
20+main = do (_ :: arg :: _) <- getArgs
21+ let vec = runPure [123456789] (mkSortVec (fromInteger (cast arg)))
22+ putStrLn "Made vector"
23+ print (vsort vec)
24+
benchmarks/trivial/sortvec.ipkgnew file+8
@@ -0,0 +1,8 @@
1+package sort
2+
3+modules = sortvec
4+opts = "-p effects"
5+
6+executable = sortvec
7+main = sortvec
8+