Commit c65ac9a0 authored by Kai Prott's avatar Kai Prott
Browse files


parent e73a11cc
A tool to verify user-defined conditions in Elm programs.
* 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 (
* All header files must be at `/usr/include`
* All `*.a` and `*.so` files must be at `/usr/lib`
**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
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
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.
\ No newline at end of file
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment