How to change `__tlacache__` to e.g. `.tlacache`?

[lemmy]

Is it possible to change the name of __tlacache__ to e.g. .tlacache or even ~/.tlaplus as used by TLC and the Toolbox?

...
(* created new "__tlacache__/FiniteSets.tlaps/FiniteSets.thy" *)
(* fingerprints written in "__tlacache__/FiniteSets.tlaps/fingerprints" *)
...

[johnyf]

The definition currently can be changed at:

tlapm/src/tlapm.ml

Lines 61 to 66 in 9e9ae24

	let mkdir_tlaps t =
	let cachedir = "__tlacache__" in
	let tlapsdir = cachedir ^ "/" ^ t.core.name.core ^ ".tlaps" in
	if not (Sys.file_exists cachedir) then Unix.mkdir cachedir 0o777;
	if not (Sys.file_exists tlapsdir) then Unix.mkdir tlapsdir 0o777;
	(cachedir, tlapsdir)

In addition to changing the definition, one possibility could be to add a command-line argument for specifying the value of the variable cachedir.

[lemmy]

I'd suggest changing the default for the reasons discussed on the mailing list.

[johnyf]

I opened a pull request to address changing the default location of the auxiliary directory.

[johnyf]

The default name of the directory for auxiliary and temporary files has been changed in commit 7556ec5 (#20).

What remains is adding a command-line option for specifying the value of the variable cachedir (#16 (comment)).

[lemmy]

Have you considered reading cachedir from an environment variable => easily change it user/system-wide?

[johnyf]

Thank you for suggesting this, I had not thought of reading an environment variable, which is a better solution. It seems that reading of the environment variable could occur within the OCaml module src/params.ml.

Naming the new environment variable

Other environment variables that are read in that module are:

• PATH
• TLAPM_SMT_SOLVER
• TLAPM_FLATTEN
• TLAPM_NORMALIZE
• TLAPM_CACHE

The relevant lines of code are:

tlapm/src/params.ml

Line 75 in eb1c447

let path = Sys.getenv "PATH" in

tlapm/src/params.ml

Line 103 in eb1c447

then sprintf " in this PATH:\n%s%s\n" (Sys.getenv "PATH") extrapath

tlapm/src/params.ml

Lines 206 to 212 in eb1c447

	(* The default SMT solver is now Z3. The user can override it with:
	- environment variable TLAPM_SMT_SOLVER
	- command-line option --solver
	- explicit directive in the BY statement
	*)
	let smt =
	try ref (User (Sys.getenv "TLAPM_SMT_SOLVER"))

tlapm/src/params.ml

Line 323 in eb1c447

try match Sys.getenv "TLAPM_FLATTEN" with

tlapm/src/params.ml

Line 330 in eb1c447

try match Sys.getenv "TLAPM_NORMALIZE" with

tlapm/src/params.ml

Line 339 in eb1c447

try match Sys.getenv "TLAPM_CACHE" with

Following this naming scheme, the new environment variable could be named TLAPM_CACHE_DIR.

The environment variable TLAPM_CACHE appears to be specifying how *.xtla files are handled:

tlapm/src/params.ml

Lines 339 to 349 in eb1c447

	try match Sys.getenv "TLAPM_CACHE" with
	| "gen" ->
	xtla := true ;
	use_xtla := false
	| "use" ->
	xtla := true ;
	use_xtla:= true
	| _ ->
	xtla := false ;
	use_xtla := false
	with Not_found -> ()

tlapm/src/module/m_save.ml

Lines 83 to 84 in eb1c447

	| Some _, Some _ when not !Params.use_xtla ->
	really_load_module mn fn None

tlapm/src/module/m_save.ml

Lines 114 to 118 in eb1c447

	let load_module ?clock ?root:(r="") mn =
	clocking clock begin fun () ->
	let fn = (Filename.concat r (mn.core ^ ".tla")) @@ mn in
	let fnx = (Filename.concat r (mn.core ^ ".xtla")) @@ mn in
	really_load_module mn (file_search fn) (file_search fnx)

tlapm/src/module/m_save.ml

Line 129 in eb1c447

let fnx = file_search ((fn.core ^ ".xtla") @@ fn) in

tlapm/src/module/m_save.ml

Lines 236 to 240 in eb1c447

	let store_module ?clock mule =
	if !Params.xtla then
	clocking clock begin fun () ->
	let fn = (Util.get_locus mule).Loc.file in
	let fnx = Filename.chop_extension fn ^ ".xtla" in

Using ag in this repository, it appears that from the environment variables listed above, only the variable TLAPM_SMT_SOLVER is documented, at:

tlapm/doc/web/content/Documentation/Tutorial/Tactics.html

Lines 202 to 213 in eb1c447

	<li>Third option: permanently change the baseline SMT solver via an
	environment variable. This is done by setting
	the <code>TLAPM_SMT_SOLVER</code> environment variable to be the
	command line described above. For example, under Linux you should
	add the line
	<table>
	<tr><td>
	<span class="listing sole">export TLAPM_SMT_SOLVER='cvc4 -lang smt2 "$file"' </span>
	</td></tr></table>
	to your shell's startup file (<code>.bashrc</code>).</li>
	</p>
	</div>

Assertions about the value of the new environment variable

About the value of the variable TLAPM_CACHE_DIR, it could be required to be a relative path. If an absolute path were given, then runs of tlapm in different directories would store fingerprint files in the same directories. Using the current implementation, these directories would be named after the base name of the source TLA+ modules.

So if in different directories, TLA+ modules with the same name but different contents exist, then there would be a mismatch of the fingerprints file when calling tlapm on one of those TLA+ modules, after having called tlapm on another TLA+ module with the same name (contained in another directory). This sharing of a fingerprints file and its potential correctness is discussed more below.

About how to check, in a cross-platform way, that the given path is absolute, perhaps this could be done similarly to how the CPython function os.path.isabs works. Perhaps checking that the path starts with a shlash suffices, because in Windows tlapm would work in Cygwin (in WSL now that Cygwin has been deprecated--though I am considering the case of a user building tlapm within Windows), and tlapm is already using slashes as component separators in paths and Unix-like absolute paths:

tlapm/src/system.ml

Line 84 in eb1c447

let pid = Unix.create_process "/bin/sh" [| "/bin/sh"; "-c"; cmd |]

Another check would be to ensure that the given string can be a pathname (not the empty string, not containing characters that cannot be in a path). Or this check could be done indirectly, by letting an error arise when Unix.mkdir is called.

Regarding the implementation, intermediate directories that do not exist would need to be created (OCaml's standard library does not appear to have an implementation of mkdir -p, as discussed in this thread).

In any case, I wrote a first implementation (at: https://github.com/johnyf/tlapm/tree/env_var_cache_dir) that does not have these checks yet.

Sharing of fingerprints file between TLA+ modules with the same name

It seems to me that even in the case of an absolute path for TLAPM_CACHE_DIR, correctness would be ensured, because a fingerprints file stores fingerprints of proof obligations, so the only way for a proof obligation to match a fingerprinted result is for the proof obligation to be exactly the same as the proof obligation that generated the fingerprinted result (modulo bugs: after the branch updated_enabled_cdot is merged, specifically the change: 987e425#diff-2b4e2d1877c6eb74da968a48d115ca813636ff6901d3dbc68ec70920d778d3c2R447). To put it differently, running tlapm on another TLA+ file with the same name is equivalent to running tlapm on the same TLA+ file after changing the contents of the TLA+ file. tlapm should work correctly in this case, therefore also in the case of using the same fingerprints file for two TLA+ files with the same name but different contents.

It might even be the case that the single fingerprints file would accumulate the fingerprints for the proof obligations from the two different TLA+ modules, and stabilize, and then work as a "shared" fingerprints file. I am not completely sure about this, in particular whether the fingerprints file would stabilize, instead of oscillating between two different states.

Global fingerprinting

If such a shared fingerprints file stabilized, then in principle there could be a single global fingerprints file that would be used by tlapm whenever tlapm is invoked, for all TLA+ files that tlapm works with. That global fingerprints file would enable reusing results that have already been proved for another TLA+ module that happened to give rise to the same proof obligation.

An issue that would remain with such an approach would be that the entire-module's temporal file *.thy (for example, .tlacache/Foo.tlaps/Foo.thy) would be overwritten by subsequent runs of tlapm.

The other temporary files (*.smt, *.smt.out, *.thy, *.thy.out, *.znn, and *.znn.out), which are generated when tlapm is given the option --debug=tempfiles, include in their filenames a number that is selected so that:

The file is guaranteed to be different from any other file that existed when temp_file was called.

quoting the documentation of the OCaml function https://ocaml.org/api/Filename.html#VALtemp_file, which applies also to the OCaml function https://ocaml.org/api/Filename.html#VALopen_temp_file, which is called to form these filenames, from the function Util.temp_file:

tlapm/src/util/util.ml

Line 180 in eb1c447

Filename.open_temp_file ~temp_dir:!Params.output_dir ~mode:[Open_binary]

which is called from the function Backend.Prep.mk_temps:

tlapm/src/backend/prep.ml

Line 181 in eb1c447

let (inf, inc) = Util.temp_file cleanup suffix in

Even though these temporary files have unique names, they would accumulate from different files, in case the option --debug=tempfiles is used in different source directories. This observation suggests that it might be useful to separate the storage of fingerprints from where temporary files generated by --debug=tempfiles are stored. In particular, the temporary files could be stored in another directory, always local to the TLA+ file being proved. This other directory could be a visible directory (i.e., not with a name starting with .), because when --debug=tempfiles is used, the purpose is typically to inspect the generated files.

If so, then copying of the temporary files would ensure that the generated files remain also in the directory where they were created, so that new temporary files created by OCaml will be guaranteed to have different names (I am writing this because I do not know what algorithm OCaml is using to decide how to name the new files, and so whether the naming depends on what files are found to exist in the target directory).

Another observation about a global fingerprints file is that the option tlapm --printfp would be less useful for such a global fingerprints file, because such a file would contain fingerprints from many different files, and even from identically-named files.

These observations suggest that in case global fingerprinting is ever implemented, it might be useful to add to tlapm an option --local-files that would make tlapm use a local directory for auxiliary and temporary files, i.e., what tlapm is currently doing.

Using an absolute path for TLAPM_CACHE_DIR but different directories for identically-named TLA+ modules

Even if this stabilization of the fingerprints file is not true for the current fingerprinting algorithm (implemented in the OCaml module https://github.com/tlaplus/tlapm/blob/eb1c447fff944342ad51b237ade35a05964bb19d/src/backend/fingerprints.ml), a global directory for storing fingerprinting and temporal files could still be used, after a modification to tlapm to name the per-module directories (those directories that are currently named like .tlacache/Foo.tlaps) using the TLA+ file's absolute path (for example this approach would create the directory absolute/path/to/Foo.tlaps within the directory specified by the value of the environment variable TLAPM_CACHE_DIR).

[lemmy]

Env variables might not be such a good idea unless the Toolbox passes environment variables on macOS, Linux, and Windows. Perhaps, env vars and command-line params?

[johnyf]

Yes, I added a command-line option --set-cache-dir and pushed the changes to the branch mentioned above.

[johnyf]

Note: document the new environment variable TLAPM_CACHE_DIR, in the website and in the message of tlapm --help. The new command-line option is documented in the message printed by tlapm --help.

[johnyf]

About points that I noted above (#16 (comment)):

Checking whether the given string is a path

This is a question that relates to the operating system. The check will be by trial: try to pass the given string to the Unix module of OCaml, and catch any exceptions.

Creating intermediate directories

The user will be responsible for creating any intermediate directories that appear in the string (path) that the user
gives as argument to the command-line parameter --set-cache-dir, or to the associated variable of the runtime environment (TLAPM_CACHE_DIR).

Creating intermediate directories from within tlapm diverges from the functionality of tlapm, and is implicit.

Checking whether the given path is relative

Checking that a path is relative does not prevent the issues that arise with a common directory: relative paths can still be used to point to the same directory, from different tlapm runs in different directories (each directory containing different files with a name coincidence).

So there is no way to prevent this issue, and thus the user is responsible for what paths they choose to pass to tlapm. No checking of the form of the given path will be implemented.