chore: remove obsolete code

leanprover · Oct 25, 2023 · 0285878 · 0285878
1 parent a7323c9
commit 0285878
Show file tree

Hide file tree

Showing 3 changed files with 1 addition and 25 deletions.
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -63,9 +63,6 @@ option(RUNTIME_STATS       "RUNTIME_STATS" OFF)
 option(BSYMBOLIC "Link with -Bsymbolic to reduce call overhead in shared libraries (Linux)" ON)
 option(USE_GMP "USE_GMP" ON)
 
-# development-specific options
-option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" ON)
-
 set(LEAN_EXTRA_MAKE_OPTS  ""                           CACHE STRING "extra options to lean --make")
 set(LEANC_CC              "cc"                         CACHE STRING "C compiler to use in `leanc`")
 
@@ -93,10 +90,6 @@ if ("${RUNTIME_STATS}" MATCHES "ON")
   string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_RUNTIME_STATS")
 endif()
 
-if (NOT("${CHECK_OLEAN_VERSION}" MATCHES "ON"))
-  string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_IGNORE_OLEAN_VERSION")
-endif()
-
 if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
     # TODO(WN): code size/performance tradeoffs
     # - we're using -O3; it's /okay/
@@ -401,26 +394,17 @@ if(MULTI_THREAD AND NOT MSVC AND (NOT ("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin"))
 endif()
 
 # Git HASH
-set(LEAN_PACKAGE_VERSION "NOT-FOUND")
 if(USE_GITHASH)
   include(GetGitRevisionDescription)
   get_git_head_revision(GIT_REFSPEC GIT_SHA1)
   if(${GIT_SHA1} MATCHES "GITDIR-NOTFOUND")
     message(STATUS "Failed to read git_sha1")
     set(GIT_SHA1 "")
-    if(EXISTS "${LEAN_SOURCE_DIR}/bin/package_version")
-      file(STRINGS "${LEAN_SOURCE_DIR}/bin/package_version" LEAN_PACKAGE_VERSION)
-      message(STATUS "Package version detected: ${LEAN_PACKAGE_VERSION}")
-    endif()
   else()
     message(STATUS "git commit sha1: ${GIT_SHA1}")
   endif()
 else()
   set(GIT_SHA1 "")
-  if(EXISTS "${LEAN_SOURCE_DIR}/bin/package_version")
-    file(STRINGS "${LEAN_SOURCE_DIR}/bin/package_version" LEAN_PACKAGE_VERSION)
-    message(STATUS "Package version detected: ${LEAN_PACKAGE_VERSION}")
-  endif()
 endif()
 configure_file("${LEAN_SOURCE_DIR}/githash.h.in" "${LEAN_BINARY_DIR}/githash.h")
 

diff --git a/src/library/util.cpp b/src/library/util.cpp
@@ -873,11 +873,7 @@ void initialize_library_util() {
     if (std::strlen(LEAN_SPECIAL_VERSION_DESC) > 0) {
         out << "-" << LEAN_SPECIAL_VERSION_DESC;
     }
-    if (std::strlen(LEAN_GITHASH) == 0) {
-        if (std::strcmp(LEAN_PACKAGE_VERSION, "NOT-FOUND") != 0) {
-            out << ", package " << LEAN_PACKAGE_VERSION;
-        }
-    } else {
+    if (std::strlen(LEAN_GITHASH) > 0) {
         out << ", commit " << std::string(LEAN_GITHASH).substr(0, 12);
     }
     g_version_string = new std::string(out.str());

diff --git a/src/version.h.in b/src/version.h.in
@@ -6,7 +6,3 @@
 
 // Additional version description like "nightly-2018-03-11"
 #define LEAN_SPECIAL_VERSION_DESC "@LEAN_SPECIAL_VERSION_DESC@"
-
-// When git_sha1 is not available, lean reads bin/version file and
-// assign its contents to LEAN_PACKAGE_VERSION
-#define LEAN_PACKAGE_VERSION "@LEAN_PACKAGE_VERSION@"