Rework all unit tests, which depend on `APALACHE_HOME`

[Kukovec]

Following a Slack troubleshooting session, it seems to be a QoL barrier for first-time users, since Apalache reports test failures if one simply runs make on a freshly cloned repository, without first configuring the home variable. To avoid this, we should either turn affected unit tests into integration tests, or embed the files, which are now being read from the folder.

[thpani]

To avoid this, we should either turn affected unit tests into integration tests, or embed the files, which are now being read from the folder.

The affected unit tests are for SanyImporter, not sure how we would get equivalent tests for this.

IMO it would be better to copy and adept the provisions in TestTypeCheckerTool to print a helpful error message:

https://github.com/informalsystems/apalache/blob/20b0c4fdaff09686bbedba479a1866b46012394a/passes/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestTypeCheckerTool.scala#L45-L52

[thpani]

Also, FWIW, our install-from-source instructions cover this:

https://github.com/informalsystems/apalache/blob/20b0c4fdaff09686bbedba479a1866b46012394a/docs/src/apalache/installation/source.md?plain=1#L13

https://github.com/informalsystems/apalache/blob/20b0c4fdaff09686bbedba479a1866b46012394a/CONTRIBUTING.md?plain=1#L154-L160

[Kukovec]

The affected unit tests are for SanyImporter, not sure how we would get equivalent tests for this.

You can import from an embedded string, that avoids looking up anything in the filesystem and the need for the home variable.

Also, FWIW, our install-from-source instructions cover this:

You shouldn't have to use direnv when first installing IMO. It should be made possible to just run make and then <dir>/bin/apalache-mc .... Advanced/efficient invocations should be the next step, once you realize how tedious the alternative is.

[thpani]

You can import from an embedded string, that avoids looking up anything in the filesystem and the need for the home variable.

afaict these instance/extend standard modules, how do you load those from a string?

You shouldn't have to use direnv when first installing IMO

you don't have to use direnv, one can simply source the file as it says in the installation docs. this is not about advanced/efficient invocation, simply setting up the build env.

[Kukovec]

afaict these instance/extend standard modules, how do you load those from a string?

You don't have to at all, because the tests (at least in passes, I have to look at the other one) don't actually do MC (just typechecking). For that purpose, std. module operators get parsed as internal operators, so you have type info.

you don't have to use direnv, one can simply source the file as it says in the installation docs. this is not about advanced/efficient invocation, simply setting up the build env.

You shouldn't have to do that manually either. If it really is necessary, then it should happen as part of make automagically.

[Kukovec]

It's less about what is in the docs (after all, the docs do mention setting APALACHE_HOME), and more about what the most streamlined new-user experience is.