chore: CI: build 64-bit platforms consistently with GMP

.github/workflows/ci.yml

@@ -217,7 +217,7 @@ jobs:
                 "release": true,
                 "check-level": 2,
                 "shell": "msys2 {0}",
-                "CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF",
+                "CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
                 // for reasons unknown, interactivetests are flaky on Windows
                 "CTEST_OPTIONS": "--repeat until-pass:2",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
@@ -227,7 +227,7 @@ jobs:
               {
                 "name": "Linux aarch64",
                 "os": "nscloud-ubuntu-22.04-arm64-4x8",
-                "CMAKE_OPTIONS": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-linux_aarch64",
+                "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
                 "release": true,
                 "check-level": 2,
                 "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",

flake.nix

@@ -38,7 +38,11 @@
           # more convenient `ctest` output
           CTEST_OUTPUT_ON_FAILURE = 1;
         } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
-          GMP = pkgsDist.gmp.override { withStatic = true; };
+          GMP = (pkgsDist.gmp.override { withStatic = true; }).overrideAttrs (attrs:
+            pkgs.lib.optionalAttrs (pkgs.stdenv.system == "aarch64-linux") {
+              # would need additional linking setup on Linux aarch64, we don't use it anywhere else either
+              hardeningDisable = [ "stackprotector" ];
+            });
           LIBUV = pkgsDist.libuv.overrideAttrs (attrs: {
             configureFlags = ["--enable-static"];
             hardeningDisable = [ "stackprotector" ];

src/library/module.cpp

@@ -49,17 +49,30 @@ namespace lean {
 struct olean_header {
     // 5 bytes: magic number
     char marker[5] = {'o', 'l', 'e', 'a', 'n'};
-    // 1 byte: version, currently always `1`
-    uint8_t version = 1;
-    // 42 bytes: build githash, padded with `\0` to the right
-    char githash[42];
+    // 1 byte: version, incremented on structural changes to header
+    uint8_t version = 2;
+    // 1 byte of flags:
+    // * bit 0: whether persisted bignums use GMP or Lean-native encoding
+    // * bit 1-7: reserved
+    uint8_t flags =
+#ifdef LEAN_USE_GMP
+        0b1;
+#else
+        0b0;
+#endif
+    // 33 bytes: Lean version string, padded with '\0' to the right
+    // e.g. "4.12.0-nightly-2024-10-18". May not be null-terminated.
+    char lean_version[33];
+    // 81b008650766442a0dfa9faa796e4588c9d7d3a1
+    // 40 bytes: build githash, padded with `\0` to the right
+    char githash[40];
     // address at which the beginning of the file (including header) is attempted to be mmapped
     size_t base_addr;
     // payload, a serialize Lean object graph; `size_t` has same alignment requirements as Lean objects
     size_t data[];
 };
 // make sure we don't have any padding bytes, which also ensures `data` is properly aligned
-static_assert(sizeof(olean_header) == 5 + 1 + 42 + sizeof(size_t), "olean_header must be packed");
+static_assert(sizeof(olean_header) == 5 + 1 + 1 + 33 + 40 + sizeof(size_t), "olean_header must be packed");
 
 extern "C" LEAN_EXPORT object * lean_save_module_data(b_obj_arg fname, b_obj_arg mod, b_obj_arg mdata, object *) {
     std::string olean_fn(string_cstr(fname));
@@ -96,6 +109,7 @@ extern "C" LEAN_EXPORT object * lean_save_module_data(b_obj_arg fname, b_obj_arg
         // see/sync with file format description above
         olean_header header = {};
         header.base_addr = base_addr;
+        strncpy(header.lean_version, get_short_version_string().c_str(), sizeof(header.lean_version));
         strncpy(header.githash, LEAN_GITHASH, sizeof(header.githash));
         out.write(reinterpret_cast<char *>(&header), sizeof(header));
         out.write(static_cast<char const *>(compactor.data()), compactor.size());
@@ -140,16 +154,16 @@ extern "C" LEAN_EXPORT object * lean_read_module_data(object * fname, object *)
 
         olean_header default_header = {};
         olean_header header;
-        if (!in.read(reinterpret_cast<char *>(&header), sizeof(header))) {
+        if (!in.read(reinterpret_cast<char *>(&header), sizeof(header))
+            || memcmp(header.marker, default_header.marker, sizeof(header.marker)) != 0) {
             return io_result_mk_error((sstream() << "failed to read file '" << olean_fn << "', invalid header").str());
         }
-        if (memcmp(header.marker, default_header.marker, sizeof(header.marker)) != 0
-            || header.version != default_header.version
+        if (header.version != default_header.version || header.flags != default_header.flags
 #ifdef LEAN_CHECK_OLEAN_VERSION
             || strncmp(header.githash, LEAN_GITHASH, sizeof(header.githash)) != 0
 #endif
         ) {
-            return io_result_mk_error((sstream() << "failed to read file '" << olean_fn << "', invalid header").str());
+            return io_result_mk_error((sstream() << "failed to read file '" << olean_fn << "', incompatible header").str());
         }
         char * base_addr = reinterpret_cast<char *>(header.base_addr);
         char * buffer = nullptr;

src/library/util.cpp

@@ -816,6 +816,9 @@ optional<name> is_unsafe_rec_name(name const & n) {
     return option_ref<name>(lean_is_unsafe_rec_name(n.to_obj_arg())).get();
 }
 
+static std::string * g_short_version_string = nullptr;
+std::string const & get_short_version_string() { return *g_short_version_string; }
+
 static std::string * g_version_string = nullptr;
 std::string const & get_version_string() { return *g_version_string; }
 
@@ -863,6 +866,7 @@ void initialize_library_util() {
     if (std::strlen(LEAN_SPECIAL_VERSION_DESC) > 0) {
         out << "-" << LEAN_SPECIAL_VERSION_DESC;
     }
+    g_short_version_string = new std::string(out.str());
     if (std::strlen(LEAN_PLATFORM_TARGET) > 0) {
         out << ", " << LEAN_PLATFORM_TARGET;
     }

src/library/util.h

@@ -234,6 +234,7 @@ name mk_unsafe_rec_name(name const & n);
 /** Return some(n') if \c n is a name created using mk_unsafe_rec_name(n') */
 optional<name> is_unsafe_rec_name(name const & n);
 
+LEAN_EXPORT std::string const & get_short_version_string();
 LEAN_EXPORT std::string const & get_version_string();
 
 expr const & extract_mdata(expr const &);