mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-11 08:55:23 +03:00
Added simple benchmark system
This commit is contained in:
parent
029da074db
commit
86fc1a193c
1
benchmarks/ALL
Normal file
1
benchmarks/ALL
Normal file
@ -0,0 +1 @@
|
||||
trivial/sortvec 2000
|
21
benchmarks/README
Normal file
21
benchmarks/README
Normal file
@ -0,0 +1,21 @@
|
||||
Benchmarks
|
||||
----------
|
||||
|
||||
To run:
|
||||
|
||||
$ ./build.pl -- builds all benchmark binaries
|
||||
$ ./run.pl -- runs all benchmarks
|
||||
|
||||
Adding a test
|
||||
-------------
|
||||
|
||||
Add a line to the 'ALL' file of the following form:
|
||||
|
||||
dir/main arg
|
||||
|
||||
where 'dir' is the directory the benchmark lives in, 'main' is the name of the
|
||||
ipkg file and executable (these must be the same), 'arg' is the input to give
|
||||
to the binary.
|
||||
|
||||
It is assumed that all benchmarks take exactly one argument, which helps to
|
||||
ensure that they are not simply doing all the work at compile time.
|
14
benchmarks/build.pl
Executable file
14
benchmarks/build.pl
Executable file
@ -0,0 +1,14 @@
|
||||
#!/usr/bin/perl
|
||||
|
||||
$bmarks = `cat ALL`;
|
||||
@bm = split(/\n/, $bmarks);
|
||||
|
||||
foreach $b (@bm) {
|
||||
if ($b =~ /([a-zA-Z0-9]+)\/([a-zA-Z0-9]+)\s+(.*)/) {
|
||||
print "Building $1 / $2\n";
|
||||
chdir $1;
|
||||
system("idris --clean $2.ipkg");
|
||||
system("idris --build $2.ipkg");
|
||||
chdir "..";
|
||||
}
|
||||
}
|
24
benchmarks/run.pl
Executable file
24
benchmarks/run.pl
Executable file
@ -0,0 +1,24 @@
|
||||
#!/usr/bin/perl
|
||||
|
||||
$bmarks = `cat ALL`;
|
||||
@bm = split(/\n/, $bmarks);
|
||||
|
||||
$total = 0;
|
||||
|
||||
foreach $b (@bm) {
|
||||
if ($b =~ /([a-zA-Z0-9]+)\/([a-zA-Z0-9]+)\s+(.*)/) {
|
||||
#print "Running $1 $2\n";
|
||||
chdir $1;
|
||||
$result = `/usr/bin/time ./$2 $3 2> .times`;
|
||||
$time = `cat .times`;
|
||||
chdir "..";
|
||||
#print $time;
|
||||
@timeflds = split(/\s+/, $time);
|
||||
$user = $timeflds[3];
|
||||
print "$1 / $2 $user\n";
|
||||
$total += $user;
|
||||
}
|
||||
}
|
||||
|
||||
print "\nTOTAL $total\n";
|
||||
|
24
benchmarks/trivial/sortvec.idr
Normal file
24
benchmarks/trivial/sortvec.idr
Normal file
@ -0,0 +1,24 @@
|
||||
module Main
|
||||
|
||||
import System
|
||||
import Effect.Random
|
||||
|
||||
total
|
||||
insert : Ord a => a -> Vect n a -> Vect (S n) a
|
||||
insert x [] = [x]
|
||||
insert x (y :: ys) = if (x < y) then x :: y :: ys else y :: insert x ys
|
||||
|
||||
vsort : Ord a => Vect n a -> Vect n a
|
||||
vsort [] = []
|
||||
vsort (x :: xs) = insert x (vsort xs)
|
||||
|
||||
mkSortVec : (n : Nat) -> Eff m [RND] (Vect n Int)
|
||||
mkSortVec Z = return []
|
||||
mkSortVec (S k) = return (fromInteger !(rndInt 0 10000) :: !(mkSortVec k))
|
||||
|
||||
main : IO ()
|
||||
main = do (_ :: arg :: _) <- getArgs
|
||||
let vec = runPure [123456789] (mkSortVec (fromInteger (cast arg)))
|
||||
putStrLn "Made vector"
|
||||
print (vsort vec)
|
||||
|
8
benchmarks/trivial/sortvec.ipkg
Normal file
8
benchmarks/trivial/sortvec.ipkg
Normal file
@ -0,0 +1,8 @@
|
||||
package sort
|
||||
|
||||
modules = sortvec
|
||||
opts = "-p effects"
|
||||
|
||||
executable = sortvec
|
||||
main = sortvec
|
||||
|
Loading…
Reference in New Issue
Block a user