-
Notifications
You must be signed in to change notification settings - Fork 19
Debugging and Testing Hets
If Hets does not compile: try make distclean
Important: Hets is quite a large system. It is useful to first understand the central data structures of Hets by following the sample ghci session below.
Hets may be tested and debugged
- in a top-down manner, by calling hets on some libraries and inserting some trace output, or by simulating the hets command line with ghci, see below,
- or in a bottom-up manner, by testing and debugging individual modules.
Which way is better depends on the nature of your specific task, and on your personal preferences. Generally, bottom up should be prefered if this is possible, because this reduces complexity.
There are several tools for debugging and testing Hets:
- Interactive evaluation with ghci
- Tracing
- Regression tests
- Standalone versions of Hets
- Profiling
- Quick Check
- Debugger
- Interactive Tests
With make ghci, you can call the interactive Haskell interpreter ghci. Use :l filename.hs to load your specific module (use :r to reload the module if you have changed the sources). Then you can interactively test individual functions of your module.
You also can simulate the hets command line. Type in:
:l Scratch.hs
Just (ln,libenv) <- process "test/Sorting1.casl"
and your file gets analysed and you can inspect the resulting data structures. Therefore, you probably need to load modules like Common/Id.hs as well:
:m +Common.Id
A sample session is stored in the file sample-ghci-script that can be pointed to by a .ghci file. Look into Static/DevGraph.hs (and also into Logic/Grothendieck.hs and CASL/Sign.hs) to understand the data structures involved.
It is advisable not to look into the (rather large) data structures directly, but instead inspect their types by:
:browse Main
:browse Common.Id
:t showId
and then further decompose them, as shown in the sample file.
If you have written a parser, you can test it by adding two lines to your source file:
import Common.AnnoState
parse p inp = runParser p (emptyAnnos ()) "" inp
Then call at the ghci command prompt:
parse myParser myInputString
With the Debug.Trace.trace function, you can output trace information. Use show or Common.DocUtils.showDoc for converting a value to a string. For example:
import Debug.Trace
import Common.DocUtils
f :: Show a => [a] -> [a]
f x = trace ("x=" ++ show x) $ reverse x
g :: Pretty a => [a] -> [a]
g x = trace ("x=" ++ showDoc x "") $ reverse x
make check runs various regression tests partly using the following standalone programs.
There are various standalone versions covering specific aspects of Hets:
- Parser:
make test_parser - CASL parser:
make capa - HasCASL parser:
make hacapa - Haskell analysis:
make hana - HasCASL to Haskell translation:
make h2h - HetCASL parser:
make hetpa - HetCASL analysis:
make hetana - ATC test system:
make atctest - ATerm.Lib test system:
make atermlibtest,make hatermdiff
In order to translate hets with profiling, move away the uni and programatica directories. Call
make PROFILE=on restack
make PROFILE=on hets # or hets_server
The resulting hets binary now creates a file hets.prof for inspection if executed with additional final arguments +RTS -p.
hets -v2 -o prf Basic/Numbers.casl +RTS -p
If ghc complains that a dyn_o file is missing, it can be necessary to call
make restack
make hets # or hets_server
beforehand.
Additional Resources:
- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/profiling.html
- https://www.fpcomplete.com/blog/2015/04/ghc-prof-flamegraph/
We have a single file Common/Lib/RelCheck.hs with quick check properties. We have not yet worked on writing HUnit tests.
The GHCi debugger does not seem to be working. Other tools are usually restricted to Haskell98 sources.