Setup and portable mode

At this point, you have a (hopefully recent) matla binary in your path.

> matla help
matla 0.1.0

Manager for TLA+ projects.

USAGE:
    matla [FLAGS] [OPTIONS] [SUBCOMMAND]

FLAGS:
    -p, --portable    Infer toolchain from environment, load no user configuration
    -v                Increases verbosity, capped at 3
    -h, --help        Prints help information
    -V, --version     Prints version information

OPTIONS:
    -c, --color <true|on|false|off>    (De)activates colored output [default: on]

SUBCOMMANDS:
    clean        Cleans the current project: deletes the `target` directory.
    help         Prints this message or the help of the given subcommand(s)
    init         Initializes an existing directory as a matla project.
    run          Runs TLC on a TLA module in a project directory.
    setup        Performs this initial matla setup, required before running matla.
    test         Run the tests of a project.
    tlc          Calls TLC with some arguments.
    uninstall    Deletes your matla user directory (cannot be undone).
    update       Updates the `tla2tools` jar in the matla user directory.

Obviously, everything works out of the box:

> matla init
Error: have you run `matla setup` yet?

Caused by:
    0: if you have, your user directory might be corrupted
    1: just re-run `matla setup` to make sure
    2: failed to load configuration
    3: failed to load user configuration
    4: failed to load file `~/.config/matla/matla.toml`
    5: No such file or directory (os error 2)

except it actually does not. Matla does let us know some setup is needed and how to perform it, so let's discuss that.

By default, matla requires a setup step before running which we present below. This setup will create a directory where matla can store your user configuration which controls the underlying TLC configuration among other things. If that is not something you are comfortable with, do read the following sections as the last one discusses matla's portable mode which does not need any user configuration files/directories to be created.

Also, if at any point you want matla to remove all user configuration data you can simply run matla uninstall. There is no functional difference with manually deleting matla's user configuration directory, which we discuss next.

$HOME/.config/matla

Following modern unix-flavored conventions, matla's configuration directory is $HOME/.config/matla.

For Windows users, $HOME is your user account's Documents folder. Well, we're a 100% almost sure it's probably that, but definitely do check just in case. And let us know if we were right if you feel like receiving our eternal (intangible) gratitude!

Previously, we ran matla init and caused matla to complain that we need to run matla setup. Doing so causes matla to ask a few questions as we are going to see now, but you can check the setup options with matla help setup if you already know the kind of setup you want.

> matla setup
|===| TLA+ toolchain setup
| Config will live in `~/.config/matla`, okay to create this directory? [Yn]

If you decide to answer no, then your only option is portable mode. Say we agree:

| y
|
| Matla can either:
| - retrieve the tla2tools jar from your environment, or
| - download it for you.
| Download the tla2tools to `~/.config/matla`? If not, matla will attempt to find it in your path [Yn]

Answering no at this point causes matla to look for the TLA+ toolbox in your path, and fail if it cannot find one. Having matla handle the toolbox for us is arguably more convenient, so let's do that:

| y
| Downloading toolbox from `https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar`...
| Download completed successfully.
| Writing downloaded file to `~/.config/matla/tla2tools.jar`...

Nice, the TLA+ toolbox is now in the matla user configuration directory. Matla's setup is done at this point, right after it displays the contents of your user (default, here) configuration file:

|
| Writing configuration file to user directory, its content is:
|
| ```
| [config]
| tla2tools = '/Users/adrien/.config/matla/tla2tools.jar'
| [tlc_cla]
| # # Full configuration for TLC runtime arguments customization
| #
| # # Sets the number of workers, `0` or `auto` for `auto`.
| # workers = 'auto' # <int|'auto'>#
| # # If active, counterexample traces will only display state variables when they change.
| # diff_cexs = 'on' # <'on'|'off'|'true'|'false'>#
| # # Sets the seed when running TLC, random if none.
| # seed = 0 # <int|'random'>#
| # # If active, TLC will not output print statements.
| # terse = 'off' # <'on'|'off'|'true'|'false'>#
| # # Maximum size of the sets TLC is allowed to enumerate.
| # max_set_size = 'default' # <u64|'default'>#
| # # If active, TLC will check for (and fail on) deadlocks.
| # check_deadlocks = 'on' # <'on'|'off'|'true'|'false'>#
| # # If active, matla will present the callstack on errors, whenever possible.
| # print_callstack = 'off' # <'on'|'off'|'true'|'false'>#
| # # If active, matla will present time statistics during runs.
| # print_timestats = 'on' # <'on'|'off'|'true'|'false'>
| ```
|
| Configuration regarding `tlc_cla` (TLC command-line arguments) corresponds to
| options for `matla run`. You can check them out with `matla help run`.
| The configuration above corresponds to matla's defaults, and all items are optional.
|
| Setup complete, matla is ready to go.
|===|

If you are familiar with TLC, you probably see right away what the [tlc_cla] TOML-section deals with. It specifies your user-level TLC options; we will see later that this is a first level of configuration, the other two being project-level configuration (a TOML file in your project directory) and command-line-level configuration (options passed to matla run). Basically, your user-level configuration is always used except for options specified in the project-level configuration, except for options specified at command-line level.

You can uncomment any of the items in this file, change them, and thus decide what the default behavior of TLC (through matla) should be. Just keep in mind that project configuration can preempt these settings, as can matla's command-line arguments.

We also see that your user configuration file stores the path to the TLA+ toolbox, which is the jar downloaded during setup. If you had asked matla not to download it but instead retrieve it from the environment, then assuming it found some/path/tla2tools.jar somewhere that's what the value of the tla2tools item of the configuration file would be.

At this point everything is in place and you can move on to the next chapters of this manual. The section below is for users that do not want matla to create a user configuration directory for some reason.

Portable mode

Some readers might not like this "hidden configuration directory" approach and prefer a portable solution, where matla has no such impact on your home directory. Although it is not the intended way to use matla, such readers will be glad to know they can run matla in portable mode with the --portable (-p for short) flag.

In portable mode, matla does not look for $HOME/.config/matla (which would fail) and instead scans the environment it's running in (mostly your $PATH environment variable) for tla2tools.jar. Assuming it finds one, matla will just use that and run normally. Obviously, running in portable mode means you will not be able to have a user configuration file.