Fingerprinting variables and bound identifiers

[johnyf]

Fingerprinting of variables and bound constants could lead to coincidence of fingerprints for different expressions. An example test case is added. Please find more details in the commit messages. The expressions used to create the fingerprints can be read with the function print_fp that is added by the first commit, after uncommenting the call to this function.

[damiendoligez]

Nice catch, and the fix looks good.

But I think we should also invalidate all the fingerprint files that were generated before the fix. One way to do this would be to insert a version number right (followed by some punctuation) after creating the buffer in fp_sequent, to make the new fingerprints different from the old ones.

[johnyf]

I pushed a commit that adds the version number of tlapm in the fingerprint (there is also the version of the fingerprints file format, defined in src/backend/fpfile.ml, but this version can remain unchanged when src/backend/fingerprints.ml changes between tlapm versions). An alternative would be to define a new version number to characterize the fingerprinting algorithm.

[johnyf]

There is a build failure that appears unrelated to the changes in this pull request. Only the macOS build fails when packaging Isabelle in the installer (in particular when downloading Isabelle):

2. Downloading and packaging Isabelle2011-1

Error: Process completed with exit code 4.

The same failure occurred when building another commit: https://github.com/tlaplus/tlapm/runs/1570729628

[johnyf]

The URL from where Isabelle is downloaded is currently unreachable, which may explain the installer packaging failures (interestingly, the Ubuntu runs succeeded, with the message "Isabelle2011-1 ALREADY downloaded" when downloading Isabelle).

[lemmy]

To not hammer the upstream download sites, the build caches artifacts. Perhaps, this Github action cache task isn't working on macOS.

---

There is a new version of this cache action that supposedly fixes the problem on macOS. I will update the Github action once tum.de site is back up.

[muenchnerkindl]

Indeed, the entire site isabelle.in.tum.de <http://isabelle.in.tum.de/> is currently down. Should be a temporary issue.There are mirrors at https://www.cl.cam.ac.uk/research/hvg/Isabelle/download_past.html <https://www.cl.cam.ac.uk/research/hvg/Isabelle/download_past.html> and https://mirror.cse.unsw.edu.au/pub/isabelle/download_past.html <https://mirror.cse.unsw.edu.au/pub/isabelle/download_past.html>, perhaps one could use them in the installer script.

…

On 17 Dec 2020, at 17:55, Ioannis Filippidis ***@***.***> wrote: The URL from where Isabelle is downloaded is currently unreachable, which may explain the installer packaging failures (interestingly, the Ubuntu runs succeeded, with the message "Isabelle2011-1 ALREADY downloaded" when downloading Isabelle). — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#23 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABZCW5NRVTAP425K3BRDCGTSVIZYPANCNFSM4UU73DVA>.

[lemmy]

There is a new version of this cache action that supposedly fixes the problem on macOS. I will update the Github action once tum.de site is back up.

Done in f827e37

[johnyf]

Thank you for fixing the cache action.

[damiendoligez]

Inserting the TLAPM version number means that all fingerprint files will be invalidated at each new release. This is probably OK but we should discuss it with the other developers.

[johnyf]

I force-pushed a commit that changes the number that is placed at the start of the fingerprints file, and removes the code for the older versions of the fingerprints. The previously pushed commit that inserted the version of tlapm within the strings that are used to produce the fingerprints has been removed.

[damiendoligez]

Have you tried this version in a directory that contains fingerprint files from an older version? As far as I can tell, this will complain that it cannot load the fingerprint file, then stop. If the file contains the old magic number, it would be better to rename it (to *.old) and continue with an empty FP table. Maybe also print a warning.

obsolete

[johnyf]

I had not tried the revised fingerprinting in the presence of fingerprint files from an older version, thank you for suggesting trying this, renaming the old fingerprints file, and printing a warning.

I tried now, first with:

• a fingerprints file from an older version present
• no fingerprints file present under the directory tree with root at
  .tlacache/Test.tlaps/fingerprints.history
  The script test.sh that I used is:

set -x
rm -rf .tlacache fingerprints_old
cat Test.tla
tlapm_old Test.tla
tree .tlacache
cp .tlacache/Test.tlaps/fingerprints fingerprints_old
tlapm_new Test.tla
tree .tlacache
diff -s fingerprints_old .tlacache/Test.tlaps/fingerprints.corrupted

and the result of bash test.sh is:

+ rm -rf .tlacache fingerprints_old
+ cat Test.tla
---- MODULE Test ----
f == [x \in {1} |-> x]

THEOREM f[1] = 1
BY DEF f
=====================
+ tlapm_old Test.tla
** Unexpanded symbols: ---

(* created new ".tlacache/Test.tlaps/Test.thy" *)
(* fingerprints written in ".tlacache/Test.tlaps/fingerprints" *)
File "./Test.tla", line 1, character 1 to line 6, character 21:
[INFO]: All 1 obligation proved.
+ tree .tlacache
.tlacache
└── Test.tlaps
    ├── Test.thy
    ├── fingerprints
    └── fingerprints.history
        └── 2021-05-12_22_41_26
            └── Test.tla

3 directories, 3 files
+ cp .tlacache/Test.tlaps/fingerprints fingerprints_old
+ tlapm_new Test.tla
(* loading fingerprints in ".tlacache/Test.tlaps/fingerprints" *)
ls: .tlacache/Test.tlaps/fingerprints.history/*/*.fp: No such file or directory
Cannot load fingerprints file: Failure("corrupted fingerprint file")
Cannot load older file: End_of_file

** Unexpanded symbols: ---

(* created new ".tlacache/Test.tlaps/Test.thy" *)
(* fingerprints written in ".tlacache/Test.tlaps/fingerprints" *)
File "./Test.tla", line 1, character 1 to line 6, character 21:
[INFO]: All 1 obligation proved.
+ tree .tlacache
.tlacache
└── Test.tlaps
    ├── Test.thy
    ├── fingerprints
    ├── fingerprints.corrupted
    └── fingerprints.history
        ├── 2021-05-12_22_41_26
        │   └── Test.tla
        └── 2021-05-12_22_41_29
            └── Test.tla

4 directories, 5 files
+ diff -s fingerprints_old .tlacache/Test.tlaps/fingerprints.corrupted
Files fingerprints_old and .tlacache/Test.tlaps/fingerprints.corrupted are identical

In this case tlapm_new appears to first try to load the file fingerprints within the function load_fingerprints below, it fails due to the old magic number not matching the new magic number (in the function load_fingerprints_aux below, the failure happens at failwith "corrupted fingerprint file" and is reported as Failure("corrupted fingerprint file") in the output above, on the line with Cannot load fingerprints file:, which comes from the secon Errors.err in the function load_fingerprints), then tlapm_new renames the old file fingerprints to fingerprints.corrupted (this happens within the first with inside the function load_fingerprints), then tlapm_new runs ls: .tlacache/Test.tlaps/fingerprints.history/*/*.fp inside the function previous_fp_file. The command ls fails to find a file, and tlapm_new tries Unix.open_process_in with the line read from ls, which raises End_of_file. This exception message is printed on the line that starts with Cannot load older file: above, from the second Errors.err inside the second with inside the function load_fingerprints below.

After this failure to load the old fingerprints file, declaring it as corrupted (it is an old fingerprints file, but not corrupted), and moving the old fingerprints file to fingerprints.corrupted, tlapm_new continues by creating a new fingerprints file. The diff above confirms that the old fingerprints file has been moved to fingerprints.corrupted.

Second, I tried with both:

• a fingerprints file from an older version, and
• a fingerprints file under the directory tree with root at
  .tlacache/Test.tlaps/fingerprints.history
  Using the script:

set -x
rm -rf .tlacache fingerprints_old
cat Test.tla
tlapm_old Test.tla
tree .tlacache
tlapm_old Test.tla
tree .tlacache
cp .tlacache/Test.tlaps/fingerprints fingerprints_old
tlapm_new Test.tla
tree .tlacache
diff -s fingerprints_old .tlacache/Test.tlaps/fingerprints.corrupted

the result is:

+ rm -rf .tlacache fingerprints_old
+ cat Test.tla
---- MODULE Test ----
f == [x \in {1} |-> x]

THEOREM f[1] = 1
BY DEF f
=====================
+ tlapm_old Test.tla
** Unexpanded symbols: ---

(* created new ".tlacache/Test.tlaps/Test.thy" *)
(* fingerprints written in ".tlacache/Test.tlaps/fingerprints" *)
File "./Test.tla", line 1, character 1 to line 6, character 21:
[INFO]: All 1 obligation proved.
+ tree .tlacache
.tlacache
└── Test.tlaps
    ├── Test.thy
    ├── fingerprints
    └── fingerprints.history
        └── 2021-05-12_22_51_07
            └── Test.tla

3 directories, 3 files
+ tlapm_old Test.tla
(* loading fingerprints in ".tlacache/Test.tlaps/fingerprints" *)
(* created new ".tlacache/Test.tlaps/Test.thy" *)
(* fingerprints written in ".tlacache/Test.tlaps/fingerprints" *)
File "./Test.tla", line 1, character 1 to line 6, character 21:
[INFO]: All 1 obligation proved.
+ tree .tlacache
.tlacache
└── Test.tlaps
    ├── Test.thy
    ├── fingerprints
    └── fingerprints.history
        ├── 2021-05-12_22_51_07
        │   └── Test.tla
        └── 2021-05-12_22_51_09
            ├── Test.tla
            └── fingerprints

4 directories, 5 files
+ cp .tlacache/Test.tlaps/fingerprints fingerprints_old
+ tlapm_new Test.tla
(* loading fingerprints in ".tlacache/Test.tlaps/fingerprints" *)
ls: .tlacache/Test.tlaps/fingerprints.history/*/*.fp: No such file or directory
Cannot load fingerprints file: Failure("corrupted fingerprint file")
Cannot load older file: End_of_file

** Unexpanded symbols: ---

(* created new ".tlacache/Test.tlaps/Test.thy" *)
(* fingerprints written in ".tlacache/Test.tlaps/fingerprints" *)
File "./Test.tla", line 1, character 1 to line 6, character 21:
[INFO]: All 1 obligation proved.
+ tree .tlacache
.tlacache
└── Test.tlaps
    ├── Test.thy
    ├── fingerprints
    ├── fingerprints.corrupted
    └── fingerprints.history
        ├── 2021-05-12_22_51_07
        │   └── Test.tla
        ├── 2021-05-12_22_51_09
        │   ├── Test.tla
        │   └── fingerprints
        └── 2021-05-12_22_51_10
            └── Test.tla

5 directories, 7 files
+ diff -s fingerprints_old .tlacache/Test.tlaps/fingerprints.corrupted
Files fingerprints_old and .tlacache/Test.tlaps/fingerprints.corrupted are identical

The resulting behavior of tlapm_new is the same.

When tlapm attempts to find a fingerprints file under the fingerprints history directory tree, it expects the filename suffix .fp. I searched the code of tlapm for this suffix (ag "\.fp" .), and it appears that tlapm does not write any files with this suffix. So the ls command invocation might need to change to search for files named fingerprints under the fingerprints directory tree (based also on the contents of that tree in the second experiment above).

Even with this modification to tlapm to search for fingerprint history files named fingerprints, it seems that tlapm will then find the file .tlacache/Test.tlaps/fingerprints.history/2021-05-12_22_51_09/fingerprints in the second experiment above, and attempt to load it, but fail inside the function load_fingerprints_aux due to reading an old magic number. tlapm would then output Cannot load older file: Failure("corrupted fingerprint file") instead of Cannot load older file: End_of_file, and continue again to create a new fingerprints file. Also, it would again have renamed the old file fingerprints to fingerprints.corrupted.

The older version of tlapm above, tlapm_old was built from 7e16045 (the next-to-last commit among the commits currently in this pull request).
The newer version of tlapm above, tlapm_new was built from 5209885 (the last commit among the commits currently in this pull request).

I think that the relevant lines of code are:

tlapm/src/backend/fpfile.ml

Lines 548 to 602 in 5209885

	let load_fingerprints_aux file =
	if Sys.file_exists file then begin
	let ic = open_in_bin file in
	let magic = Marshal.from_channel ic in
	if magic <> magic_number then failwith "corrupted fingerprint file";
	let v = Marshal.from_channel ic in
	if v >= FPunknown ()
	then Errors.fatal "fingerprint file is from a newer version of tlapm";
	translate v ic;
	close_in ic;
	if !Params.safefp then begin
	(* Erase fingerprints from other versions of Zenon and Isabelle. *)
	let oldtbl = !fptbl in
	fptbl := Hashtbl.create 500;
	let zv0 = Params.get_zenon_verfp () in
	let iv0 = Params.get_isabelle_version () in
	let keep (st, _, _, zv, iv) =
	match st with
	| NTriv (_, Zenon _) -> zv = zv0
	| NTriv (_, Isabelle _) -> iv = iv0
	| _ -> true
	in
	let process fp r =
	let l = List.filter keep (record_to_list r) in
	Hashtbl.add !fptbl fp (list_to_record l);
	in
	Hashtbl.iter process oldtbl;
	end;
	end;
	;;
	let previous_fp_file file =
	let histdir = file ^ ".history" in
	let cmd = sprintf "ls -td %s/*/*.fp" (FN.quote histdir) in
	let ic = Unix.open_process_in cmd in
	let prev = input_line ic in
	close_in ic;
	prev
	;;
	let load_fingerprints file =
	try
	load_fingerprints_aux file
	with e1 ->
	try
	Sys.rename file (file ^ ".corrupted");
	let prev = previous_fp_file file in
	load_fingerprints_aux prev;
	Errors.err "Cannot load fingerprints file: %s\n\
	previous file (%s) loaded\n" (Printexc.to_string e1) prev;
	with e2 ->
	Errors.err "Cannot load fingerprints file: %s\n\
	Cannot load older file: %s\n" (Printexc.to_string e1)
	(Printexc.to_string e2);
	;;

From the above observations, I think that it would be better to change tlapm so that it detects old fingerprints files (identified as those that contain the old magic number), and distinguish them from fingerprints files that are reported as corrupted (those that contain neither the old nor new magic number).

tlapm can then rename the old fingerprints file to fingerprints.old (instead of fingerprints.corrupted), and continue similarly to how it does above, with the difference that the error message will inform that an old fingerprints file has been found, and that it has been renamed to .tlacache/*.tlaps/fingerprints.old.

Also, updating the filename searched for in the invocation of ls seems relevant. It seems also possible to read the exit code of ls, and not attempt to load a file if ls exited with an error code, instead failing with a message informing that no fingerprints file was found under the fingerprints history directory (this message would replace the error message End_of_file in the first experiment above).

The error message about the corrupted fingerprints file could be extended to mention also that the corrupted fingerprints file has been moved to .tlacache/*.tlaps/fingerprints.corrupted.

It is imaginable that .tlacache/*.tlaps/fingerprints could be from an older tlapm version (like tlapm_old above), and .tlacache/*.tlaps/fingerprints.history/*/fingerprints could be from a newer tlapm version (like tlapm_new above). In that case, tlapm would:

• detect that the file .tlacache/*.tlaps/fingerprints is old
• move .tlacache/*.tlaps/fingerprints to .tlacache/*.tlaps/fingerprints.old
• print a message that informs about the old fingerprints file found and the renaming
• find the older fingerprints file .tlacache/*.tlaps/fingerprints.history/*/fingerprints (newest from the fingerprints files stored under the fingerprints history directory, due to the argument -t given to ls, which is described in the ls documentation starting with "-t Sort by time modified (most recently modified first)")
• successfully load the older fingerprints file, because it contains the new magic number (was created with tlapm_new).

This execution of tlapm could be a little counterintuitive, though it seems reasonable.
The error message within the first with inside the function load_fingerprints could be augmented in the line previous file (%s) loaded to note that a file with matching magic number has been loaded.

[damiendoligez]

Thanks for running the experiments. The current behavior is good enough as far as I'm concerned, but if you want to fix the error messages ("corrupted" -> "old" and "End_of_file") and it's easy to do, why not. In any case I don't think we should spend too much time on this part of the system.

[johnyf]

Thank you for the feedback. I added commits that change this behavior by:

• calling ls to search for files named fingerprints
• distinguishing between corrupted fingerprint files and fingerprint files with an old magic number
• handling of exceptions when calling ls (e.g., due to nonexistent files)
• adding more information to error messages.

The exception handling ended up being somewhat complex. Also, errors that may arise when renaming an existing fingerprints file (Sys.rename) are raised. I think that issues mentioned above have now been addressed. A few scripts that show the new behavior follow.

The following script first creates a fingerprints file with an older version of tlapm, then the newer version renames it by appending .old to the filename.

PS4="> "
set -x
rm -rf .tlacache fingerprints_old
cat Test.tla
tlapm_old Test.tla
tree .tlacache
cp .tlacache/Test.tlaps/fingerprints fingerprints_old
tlapm_new Test.tla
tree .tlacache
diff -s fingerprints_old .tlacache/Test.tlaps/fingerprints.old

The output from this script is:

> rm -rf .tlacache fingerprints_old
> cat Test.tla
---- MODULE Test ----
f == [x \in {1} |-> x]

THEOREM f[1] = 1
BY DEF f
=====================
> tlapm_old Test.tla
** Unexpanded symbols: ---

(* created new ".tlacache/Test.tlaps/Test.thy" *)
(* fingerprints written in ".tlacache/Test.tlaps/fingerprints" *)
File "./Test.tla", line 1, character 1 to line 6, character 21:
[INFO]: All 1 obligation proved.
> tree .tlacache
.tlacache
└── Test.tlaps
    ├── Test.thy
    ├── fingerprints
    └── fingerprints.history
        └── 2021-05-20_14_03_42
            └── Test.tla

3 directories, 3 files
> cp .tlacache/Test.tlaps/fingerprints fingerprints_old
> tlapm_new Test.tla
(* loading fingerprints in ".tlacache/Test.tlaps/fingerprints" *)
ls: .tlacache/Test.tlaps/fingerprints.history/*/fingerprints: No such file or directory
Cannot load fingerprints file: Failure("fingerprint file with an older magic number"), so moved fingerprints file by appending `.old` (.tlacache/Test.tlaps/fingerprints -> .tlacache/Test.tlaps/fingerprints.old)
Cannot load older fingerprints file: Failure("`ls` returned no stdout  when looking for older fingerprints file, so it appears that there are no older fingerprints files.")

** Unexpanded symbols: ---

(* created new ".tlacache/Test.tlaps/Test.thy" *)
(* fingerprints written in ".tlacache/Test.tlaps/fingerprints" *)
File "./Test.tla", line 1, character 1 to line 6, character 21:
[INFO]: All 1 obligation proved.
> tree .tlacache
.tlacache
└── Test.tlaps
    ├── Test.thy
    ├── fingerprints
    ├── fingerprints.history
    │   ├── 2021-05-20_14_03_42
    │   │   └── Test.tla
    │   └── 2021-05-20_14_03_49
    │       └── Test.tla
    └── fingerprints.old

4 directories, 5 files
> diff -s fingerprints_old .tlacache/Test.tlaps/fingerprints.old
Files fingerprints_old and .tlacache/Test.tlaps/fingerprints.old are identical

The following script first runs the old version of tlapm, then corrupts the fingerprints file, and then runs the newer version of tlapm, which renames the corrupted fingerprints file by appending .corrupted to the filename.

PS4="> "
set -x
rm -rf .tlacache fingerprints_corrupted
cat Test.tla
tlapm_old Test.tla
tree .tlacache
echo "corrupted" > .tlacache/Test.tlaps/fingerprints
cp .tlacache/Test.tlaps/fingerprints fingerprints_corrupted
tlapm_new Test.tla
tree .tlacache
diff -s fingerprints_corrupted .tlacache/Test.tlaps/fingerprints.corrupted

The output from this script is:

> rm -rf .tlacache fingerprints_corrupted
> cat Test.tla
---- MODULE Test ----
f == [x \in {1} |-> x]

THEOREM f[1] = 1
BY DEF f
=====================
> tlapm_old Test.tla
** Unexpanded symbols: ---

(* created new ".tlacache/Test.tlaps/Test.thy" *)
(* fingerprints written in ".tlacache/Test.tlaps/fingerprints" *)
File "./Test.tla", line 1, character 1 to line 6, character 21:
[INFO]: All 1 obligation proved.
> tree .tlacache
.tlacache
└── Test.tlaps
    ├── Test.thy
    ├── fingerprints
    └── fingerprints.history
        └── 2021-05-20_14_08_42
            └── Test.tla

3 directories, 3 files
> echo corrupted
> cp .tlacache/Test.tlaps/fingerprints fingerprints_corrupted
> tlapm_new Test.tla
(* loading fingerprints in ".tlacache/Test.tlaps/fingerprints" *)
ls: .tlacache/Test.tlaps/fingerprints.history/*/fingerprints: No such file or directory
Cannot load fingerprints file: Failure("input_value: truncated object"), so moved fingerprints file by appending `.corrupted` (.tlacache/Test.tlaps/fingerprints -> .tlacache/Test.tlaps/fingerprints.corrupted)
Cannot load older fingerprints file: Failure("`ls` returned no stdout  when looking for older fingerprints file, so it appears that there are no older fingerprints files.")

** Unexpanded symbols: ---

(* created new ".tlacache/Test.tlaps/Test.thy" *)
(* fingerprints written in ".tlacache/Test.tlaps/fingerprints" *)
File "./Test.tla", line 1, character 1 to line 6, character 21:
[INFO]: All 1 obligation proved.
> tree .tlacache
.tlacache
└── Test.tlaps
    ├── Test.thy
    ├── fingerprints
    ├── fingerprints.corrupted
    └── fingerprints.history
        ├── 2021-05-20_14_08_42
        │   └── Test.tla
        └── 2021-05-20_14_08_45
            └── Test.tla

4 directories, 5 files
> diff -s fingerprints_corrupted .tlacache/Test.tlaps/fingerprints.corrupted
Files fingerprints_corrupted and .tlacache/Test.tlaps/fingerprints.corrupted are identical

The following scipt first runs the older version of tlapm twice, which creates both an old fingerprints file and a fingerprints file under the directory of fingerprints history. The script then runs the newer version of tlapm, which tries to load both existing fingerprints files, identifies them as old, and renames one of them by appending .old to the filename.

PS4="> "
set -x
rm -rf .tlacache fingerprints_old
cat Test.tla
tlapm_old Test.tla
tree .tlacache
tlapm_old Test.tla
tree .tlacache
cp .tlacache/Test.tlaps/fingerprints fingerprints_old
tlapm_new Test.tla
tree .tlacache
diff -s fingerprints_old .tlacache/Test.tlaps/fingerprints.old

The output from this script is:

> rm -rf .tlacache fingerprints_old
> cat Test.tla
---- MODULE Test ----
f == [x \in {1} |-> x]

THEOREM f[1] = 1
BY DEF f
=====================
> tlapm_old Test.tla
** Unexpanded symbols: ---

(* created new ".tlacache/Test.tlaps/Test.thy" *)
(* fingerprints written in ".tlacache/Test.tlaps/fingerprints" *)
File "./Test.tla", line 1, character 1 to line 6, character 21:
[INFO]: All 1 obligation proved.
> tree .tlacache
.tlacache
└── Test.tlaps
    ├── Test.thy
    ├── fingerprints
    └── fingerprints.history
        └── 2021-05-20_14_14_13
            └── Test.tla

3 directories, 3 files
> tlapm_old Test.tla
(* loading fingerprints in ".tlacache/Test.tlaps/fingerprints" *)
(* created new ".tlacache/Test.tlaps/Test.thy" *)
(* fingerprints written in ".tlacache/Test.tlaps/fingerprints" *)
File "./Test.tla", line 1, character 1 to line 6, character 21:
[INFO]: All 1 obligation proved.
> tree .tlacache
.tlacache
└── Test.tlaps
    ├── Test.thy
    ├── fingerprints
    └── fingerprints.history
        ├── 2021-05-20_14_14_13
        │   └── Test.tla
        └── 2021-05-20_14_14_15
            ├── Test.tla
            └── fingerprints

4 directories, 5 files
> cp .tlacache/Test.tlaps/fingerprints fingerprints_old
> tlapm_new Test.tla
(* loading fingerprints in ".tlacache/Test.tlaps/fingerprints" *)
Cannot load fingerprints file: Failure("fingerprint file with an older magic number"), so moved fingerprints file by appending `.old` (.tlacache/Test.tlaps/fingerprints -> .tlacache/Test.tlaps/fingerprints.old)
Cannot load older fingerprints file: Failure("fingerprint file with an older magic number")

** Unexpanded symbols: ---

(* created new ".tlacache/Test.tlaps/Test.thy" *)
(* fingerprints written in ".tlacache/Test.tlaps/fingerprints" *)
File "./Test.tla", line 1, character 1 to line 6, character 21:
[INFO]: All 1 obligation proved.
> tree .tlacache
.tlacache
└── Test.tlaps
    ├── Test.thy
    ├── fingerprints
    ├── fingerprints.history
    │   ├── 2021-05-20_14_14_13
    │   │   └── Test.tla
    │   └── 2021-05-20_14_14_15
    │       ├── Test.tla
    │       └── fingerprints
    └── fingerprints.old

4 directories, 6 files
> diff -s fingerprints_old .tlacache/Test.tlaps/fingerprints.old
Files fingerprints_old and .tlacache/Test.tlaps/fingerprints.old are identical

The following script first runs the older version of tlapm twice, then corrupts the latest fingerprints file, then runs the newer version of tlapm, which identifies the latest fingerprints file as corrupted and renames it by appending .corrupted to the file name, and identifies also the older fingerprints file under the fingerprints history directory as from an old version, and does not load it.

PS4="> "
set -x
rm -rf .tlacache fingerprints_corrupted
cat Test.tla
tlapm_old Test.tla
tree .tlacache
tlapm_old Test.tla
tree .tlacache
echo "corrupted" > .tlacache/Test.tlaps/fingerprints
cp .tlacache/Test.tlaps/fingerprints fingerprints_corrupted
tlapm_new Test.tla
tree .tlacache
diff -s fingerprints_corrupted .tlacache/Test.tlaps/fingerprints.corrupted

The output from this script is:

> rm -rf .tlacache fingerprints_corrupted
> cat Test.tla
---- MODULE Test ----
f == [x \in {1} |-> x]

THEOREM f[1] = 1
BY DEF f
=====================
> tlapm_old Test.tla
** Unexpanded symbols: ---

(* created new ".tlacache/Test.tlaps/Test.thy" *)
(* fingerprints written in ".tlacache/Test.tlaps/fingerprints" *)
File "./Test.tla", line 1, character 1 to line 6, character 21:
[INFO]: All 1 obligation proved.
> tree .tlacache
.tlacache
└── Test.tlaps
    ├── Test.thy
    ├── fingerprints
    └── fingerprints.history
        └── 2021-05-20_14_17_48
            └── Test.tla

3 directories, 3 files
> tlapm_old Test.tla
(* loading fingerprints in ".tlacache/Test.tlaps/fingerprints" *)
(* created new ".tlacache/Test.tlaps/Test.thy" *)
(* fingerprints written in ".tlacache/Test.tlaps/fingerprints" *)
File "./Test.tla", line 1, character 1 to line 6, character 21:
[INFO]: All 1 obligation proved.
> tree .tlacache
.tlacache
└── Test.tlaps
    ├── Test.thy
    ├── fingerprints
    └── fingerprints.history
        ├── 2021-05-20_14_17_48
        │   └── Test.tla
        └── 2021-05-20_14_17_51
            ├── Test.tla
            └── fingerprints

4 directories, 5 files
> echo corrupted
> cp .tlacache/Test.tlaps/fingerprints fingerprints_corrupted
> tlapm_new Test.tla
(* loading fingerprints in ".tlacache/Test.tlaps/fingerprints" *)
Cannot load fingerprints file: Failure("input_value: truncated object"), so moved fingerprints file by appending `.corrupted` (.tlacache/Test.tlaps/fingerprints -> .tlacache/Test.tlaps/fingerprints.corrupted)
Cannot load older fingerprints file: Failure("fingerprint file with an older magic number")

** Unexpanded symbols: ---

(* created new ".tlacache/Test.tlaps/Test.thy" *)
(* fingerprints written in ".tlacache/Test.tlaps/fingerprints" *)
File "./Test.tla", line 1, character 1 to line 6, character 21:
[INFO]: All 1 obligation proved.
> tree .tlacache
.tlacache
└── Test.tlaps
    ├── Test.thy
    ├── fingerprints
    ├── fingerprints.corrupted
    └── fingerprints.history
        ├── 2021-05-20_14_17_48
        │   └── Test.tla
        ├── 2021-05-20_14_17_51
        │   ├── Test.tla
        │   └── fingerprints
        └── 2021-05-20_14_17_52
            └── Test.tla

5 directories, 7 files
> diff -s fingerprints_corrupted .tlacache/Test.tlaps/fingerprints.corrupted
Files fingerprints_corrupted and .tlacache/Test.tlaps/fingerprints.corrupted are identical

The older version of tlapm above, tlapm_old was built from 7e16045.
The newer version of tlapm above, tlapm_new was built from a1ec54a.

[damiendoligez]

This looks really good now.

[damiendoligez]

Suggested change

	failwith ("`ls` returned no stdout " ^
	" when looking for older fingerprints file, " ^
	"so it appears that there are no older fingerprints files.")
	failwith ("`ls` returned no stdout \
	when looking for older fingerprints file, \
	so it appears that there are no older fingerprints files.")

[damiendoligez]

Suggested change

	" when looking for older fingerprints file, " ^
	"so it appears that there are no older fingerprints files.")
	" when looking for older fingerprints file, \
	so it appears that there are no older fingerprints files.")

[damiendoligez]

Suggested change

	| _ -> failwith ("`ls` stopped by a signal while " ^
	"looking for older fingerprints file")
	| _ -> failwith ("`ls` stopped by a signal while \
	looking for older fingerprints file")

[johnyf]

Thank you for the comments and approving the changes. I applied the suggested changes.

[johnyf]

Thank you for merging these changes.