Build failure in 32-bit mode: Structure (Word64) has not been declared

[someplaceguy]

When building the HOL trindemossen-2 release in 32-bit mode, the following build failure occurred, which was did not occur with the trindemossen-1 release:

Building directory src/portableML/rawtheory [27 Sep, 12:34:37]
theorytool                                                          (1s)FAIL<1>
         ...
         ) end
 ../poly/SHA1_ML.sml:34: error: Structure (Word64) has not been declared
 Found near
   let val s7 = Word64.>> (... ..., ...); val s6 = Word64.>> (...);
      val s5 = ... ...; val ... = ...; val ...; ... in
      (
         Word8.fromLarge (Word64.toLarge s0),
         Word8.fromLarge (Word64.toLarge s1),
         Word8.fromLarge (... ...),
         ... ...,
         ...
         ) end
 ../poly/SHA1_ML.sml:35: error: Structure (Word64) has not been declared
 Found near
   let val s7 = Word64.>> (... ..., ...); val s6 = Word64.>> (...);
      val s5 = ... ...; val ... = ...; val ...; ... in
      (
         Word8.fromLarge (Word64.toLarge s0),
         Word8.fromLarge (Word64.toLarge s1),
         Word8.fromLarge (... ...),
         ... ...,
         ...
         ) end
 ../poly/SHA1_ML.sml:36: error: Structure (Word64) has not been declared
 Found near
   let val s7 = Word64.>> (... ..., ...); val s6 = Word64.>> (...);
      val s5 = ... ...; val ... = ...; val ...; ... in
      (
         Word8.fromLarge (Word64.toLarge s0),
         Word8.fromLarge (Word64.toLarge s1),
         Word8.fromLarge (... ...),
         ... ...,
         ...
         ) end
 ../poly/SHA1_ML.sml:93: error: Structure (Word64) has not been declared
 Found near
   datatype
      'a
         ChunkReaderState
         =
         Reading of 'a byte_reader * 'a * Word64.word |
         PadChunk of Word8Vector.vector |
         Empty
 ../poly/SHA1_ML.sml:109: error: Structure (Word64) has not been declared
 Found near Word64.+ (Word64.fromInt chunkSize, totalBytesRead)
 ../poly/SHA1_ML.sml:109: error: Structure (Word64) has not been declared
 Found near Word64.+ (Word64.fromInt chunkSize, totalBytesRead)
 Exception- Fail "Static Errors" raised
 Exception- Fail "Static Errors" raised

I'm guessing this is due to recent changes in src/portableML/rawtheory/* which make use of src/portableML/poly/SHA1_ML.sml. The latter uses Word64 which is not available in 32-bit Poly/ML builds, according to the documentation:

(...) Word64 is only available on 64-bit architectures. (...)

[mn200]

Ha! Thanks for the report; I hadn't appreciated this might be a problem. I will have to detect the build-time information about the build size, and then make the code fall back to the "shell out to shasum" approach that was being used universally before.

[someplaceguy]

Ha! Thanks for the report; I hadn't appreciated this might be a problem. I will have to detect the build-time information about the build size, and then make the code fall back to the "shell out to shasum" approach that was being used universally before.

Something like that should work, I think.

However, on Linux the right tool name is probably sha1sum rather than shasum (the former exists in coreutils but not the latter). Therefore, it might be good to detect the tool name in the configure script, as well as its path (similar to how it's done for the cp and mv utilities), as e.g. /usr/bin doesn't even exist on NixOS.