-
Notifications
You must be signed in to change notification settings - Fork 0
List of current tests
Ryan Scott edited this page Jun 2, 2015
·
2 revisions
Example / Test | Haskell File | HERMIT File | Options / Notes / Status |
---|---|---|---|
concatVanishes | Flatten.hs | Flatten.hss | -safety=unsafe |
concatVanishes | QSort.hs | QSort.hss | -safety=unsafe |
concatVanishes | Rev.hs | Rev.hss | -safety=unsafe |
evaluation | Eval.hs | Eval.hss | |
factorial | Fac.hs | Fac.hss | Broken in GHC 7.10 (but not in 7.8) due to let/app invariant issue |
fib-stream | Fib.hs | Fib.hss | broken due to Core Parser |
fib-tuple | Fib.hs | Fib.hss" | |
flatten | Flatten.hs | Flatten.hec | -safety=unsafe |
hanoi | Hanoi.hs | Hanoi.hss | For some reason loops in testsuite but not normally |
last | Last.hs | "Last.hss" | -safety=unsafe |
last | Last.hs | NewLast.hss | -safety=strict |
map | Map.hs | Map.hss | broken due to Core Parser |
mean | Mean.hs | Mean.hs | |
nub | Nub.hs | Nub.hss | |
qsort | QSort.hs | QSort.hss | |
reverse | Reverse.hs | Reverse.hss | -safety=unsafe |
new_reverse | Reverse.hs | Reverse.hec |
How to run an example in HERMIT. Make sure you are in your sandbox, then yo can run hermit
> cd hermit-shell
> cabal exec bash
> cd ..
> cd hermit/examples/reverse/
> hermit Reverse.hs Reverse.hss +Main -safety=unsafe resume
... lots of output ...
The tests actually use a small script:
set-auto-corelint True
set-pp-type Show
set-fail-hard True
load-and-run "Reverse.hss"
top ; prog
display
show-lemmas
resume