Module Harpoon.Options

type interaction_mode = [
  1. | `stop
  2. | `go_on
]

The `stop and `go_on flags control what happens in the presence of errors. In particular, the `stop flag will cause Harpoon to exit as soon as an error in encountered instead of continuing to process commands which may not make sense anymore. This is especially important when running tests.

type save_mode = [
  1. | `save_back
  2. | `no_save_back
]

Controls the behaviour of saving sessions back to the signature when they are completed.

type test_kind = [
  1. | `incomplete
  2. | `complete
]
type test_file = private {
  1. filename : string;
  2. kind : test_kind;
}
type t = private {
  1. path : string;
    (*

    The path of the signature file to load. It is expected to be either a ".bel" or a ".cfg" file.

    *)
  2. test_file : test_file option;
    (*

    The Harpoon test file to load.

    *)
  3. test_start : int option;
    (*

    The first line from which the Harpoon test file is considered as input.

    *)
  4. test_stop : interaction_mode;
    (*

    Whether to stop a test if there's an error.

    *)
  5. load_holes : bool;
    (*

    Whether to begin immediately from holes in the file.

    *)
  6. save_back : save_mode;
    (*

    Whether to save finished theorems back to the file.

    *)
}

The command-line options specified to Harpoon.

val parse_arguments : string list -> t