List of current tests - ku-fpg/hermit-shell GitHub Wiki

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