derive latest_version from tarball folder name

[digama0]

Fix for #3734 (comment)

[wlammen]

This is a quick fix, helping a pending pull request, so I don't object to adding it as is.

The core problem here is, from an architectural point of view, that the code creating the metamath zip file is detached from the users expanding it. The silent agreement encoded here is, that

• the first file in the packed source is metamath.exe, even more specific metamath/metamath.exe.VERSION.

The creating part is now responsible for providing a ZIP file of exactly this format. It previously was responsible to provide the packed source in a looser format (I presume), and additionally a separate hidden text file .latest-version which somehow got not transferred properly. It is a bit optimistic to assume that this time everything works well in the long run.

How can one ensure that at least the information flow is not disturbed by future modifications? Put the packer and unpacker into a separate do_zip_unzip.sh script, and let the packer and unpacker (or verifier) call respective functions in it. Of course you can still botch the process, but this is more difficult, when complementary operations are encoded in the same file.

[digama0]

The core problem here is, from an architectural point of view, that the code creating the metamath zip file is detached from the users expanding it. The silent agreement encoded here is, that

• the first file in the packed source is metamath.exe, even more specific metamath/metamath.exe.VERSION.

The creating part is now responsible for providing a ZIP file of exactly this format. It previously was responsible to provide the packed source in a looser format (I presume), and additionally a separate hidden text file .latest-version which somehow got not transferred properly. It is a bit optimistic to assume that this time everything works well in the long run.

This is incorrect. The .latest-version file was previously created by the download-metamath script which is part of the very same CI process here. Yes, it's in a separate file, but the two work together and both are hosted in this repo.

In the new setup, the commit revision is extracted from the folder name, which is stored in the tarball we get from github. This is not a property of the metamath-exe repo, this is something github does automatically to tarballs and specifies as such. (It's not the metamath.exe file that contains the version, it is the root folder. When you unpack the zip file everything is in the metamath-metamath-exe-NNNN/ subfolder.) We were previously working around this fact and changing the name to just metamath/ to match older scripts (and we are still doing that), but the -NNNN part is useful, since there isn't any other natural way to get the current master commit SHA without another request (and I don't think there are any other ways that aren't subject to TOCTOU although that's probably not a huge issue here).

---

If we wanted to have both parts in the same file, which is understandable, there are two options, both with downsides:

1. Put download-metamath contents in the .yml. This is unfortunate because it is a somewhat large file (although most of it is comments), and moreover it is duplicated twice because there are two CI jobs that need metamath (although maybe they should be done in the same job to avoid the overhead?).

2. Put the code that writes to GITHUB_ENV in download-metamath. This is also unfortunate because it assumes GITHUB_ENV exists or is passed in in some way, which means the script is not usable outside of github CI runners. Or we could back up one stage and have it print METAMATH_LATEST_VERSION=NNNN to stdout? It still seems like a bit of a weird factoring and it's still distributing work across two files.