README.md 2.35 KB
Newer Older
Kai Prott's avatar
Kai Prott committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
elm-verify
==========

A tool to verify user-defined conditions in Elm programs.

Prerequisites:
--------------

 * OS: Linux, Windows might not work
 * A working installation og GHC
 * A working installation of Stack or Cabal
 * Installed Z3-library version 4.6.0 (https://github.com/Z3Prover/z3/releases)
    * All header files must be at `/usr/include`
    * All `*.a` and `*.so` files must be at `/usr/lib`
    
Building:
---------

**With stack:**

  1. Change to the `elm-verify` subdirectory 
  2. Execute `stack install`
 
**With cabal version 2.\* or 3.\***

This uses cabal's new build system and will not infer with your 
globally installed Haskell packages.

  1. Change to the `elm-verify` subdirectory 
  2. Execute `cabal v2-install elm-verify-external`
     * The `v2` prefix can be omitted in cabal version 3.
     * In both versions you might need to specify where to put the final executable. 
     * Currently only elm-verify-external can be built this way. This is a limitation of the elm-compiler-library

**With cabal version 1.\***

We do not recommend this approach, as this might infer with your
globally installed Haskell packages, unless you use a sandbox.

  1. Change to the `elm-verify` subdirectory
  2. In each of the subdirectories execute `cabal configure` and `cabal install`
     Make sure that you do it in the following order:
     * elm-compiler-library
     * elm-verify-ast
     * z3-transformation
     * elm-verify
     * elm-verify-external
     * elm-verify-integrated
     * elm-compiler

Testing:
--------

This will test all files specified in `elm-verify/elm-verify/test/Spec.hs`

   1. Change to the `elm-verify` subdirectory 
   2. Execute `stack test elm-verify`

Optional command line parameters: TODO

Usage:
------

There are two different executables to verify Elm Programs with elm-verify:
   1. `elm`
   2. `elm-verify` (also called elm-verify-external)
   
The first one is a modified elm compiler that also does a verification 
during compilation if the user passes the `--verify` flag to it.
Otherwise it behaves just like the standard Elm compiler

The second one is a standalone tool that can only do the verification.
To use it, just execute `elm-verify` in the directory of an Elm project
or specify a source file to verify. (E.g. `elm-verify src/Main.elm`.)
To enable debug output one can pass `-v` as the first parameter to elm-verify.