diff options
Diffstat (limited to 'math')
72 files changed, 1764 insertions, 568 deletions
diff --git a/math/R-cran-RcppArmadillo/Makefile b/math/R-cran-RcppArmadillo/Makefile index 645024af86ea..c1c88ee22f9a 100644 --- a/math/R-cran-RcppArmadillo/Makefile +++ b/math/R-cran-RcppArmadillo/Makefile @@ -1,5 +1,5 @@ PORTNAME= RcppArmadillo -DISTVERSION= 15.0.2-2 +DISTVERSION= 15.2.2-1 CATEGORIES= math DISTNAME= ${PORTNAME}_${DISTVERSION} diff --git a/math/R-cran-RcppArmadillo/distinfo b/math/R-cran-RcppArmadillo/distinfo index d74e8fde4887..09ba7081d1cc 100644 --- a/math/R-cran-RcppArmadillo/distinfo +++ b/math/R-cran-RcppArmadillo/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1758390802 -SHA256 (RcppArmadillo_15.0.2-2.tar.gz) = f8895e85d70ddeabb1d4ec7567f81ed6fd95f9e8715d0791afd07c8382315f4e -SIZE (RcppArmadillo_15.0.2-2.tar.gz) = 2118381 +TIMESTAMP = 1763918614 +SHA256 (RcppArmadillo_15.2.2-1.tar.gz) = 9282d5448d699403d535ab3c64b10421aa89c79f4ea291b6a585cdd5b49a54ea +SIZE (RcppArmadillo_15.2.2-1.tar.gz) = 2121993 diff --git a/math/armadillo/Makefile b/math/armadillo/Makefile index 838412842fd9..8087661da7c8 100644 --- a/math/armadillo/Makefile +++ b/math/armadillo/Makefile @@ -1,5 +1,5 @@ PORTNAME= armadillo -PORTVERSION= 15.2.1 +PORTVERSION= 15.2.2 CATEGORIES= math MASTER_SITES= SF/arma diff --git a/math/armadillo/distinfo b/math/armadillo/distinfo index 01da1d0b090e..944591ea39de 100644 --- a/math/armadillo/distinfo +++ b/math/armadillo/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1762586714 -SHA256 (armadillo-15.2.1.tar.xz) = a5b8109da3c169802f51a14d3bd1246395c24bbca55601760b0c96a3c0b2f8fa -SIZE (armadillo-15.2.1.tar.xz) = 7086824 +TIMESTAMP = 1763853184 +SHA256 (armadillo-15.2.2.tar.xz) = 8ee01cd4da55bc07b7bc7d3cba702ac6e8137d384d7e7185f3f4ae1f0c79704f +SIZE (armadillo-15.2.2.tar.xz) = 7092664 diff --git a/math/coq/Makefile b/math/coq/Makefile index 2e9d5c12c76e..8ea7c773edbb 100644 --- a/math/coq/Makefile +++ b/math/coq/Makefile @@ -7,7 +7,7 @@ DISTVERSIONPREFIX= V #DISTVERSIONSUFFIX= .0 PKGNAMESUFFIX= ${EMACS_PKGNAMESUFFIX} -MAINTAINER= hrs@FreeBSD.org +MAINTAINER= ports@FreeBSD.org COMMENT= Theorem prover based on lambda-C WWW= https://coq.inria.fr/ diff --git a/math/faiss/Makefile b/math/faiss/Makefile index e64bffca76f0..608eea9e7e2e 100644 --- a/math/faiss/Makefile +++ b/math/faiss/Makefile @@ -1,6 +1,6 @@ PORTNAME= faiss DISTVERSIONPREFIX= v -DISTVERSION= 1.12.0 +DISTVERSION= 1.13.0 CATEGORIES= math MAINTAINER= yuri@FreeBSD.org @@ -28,6 +28,9 @@ GH_ACCOUNT= facebookresearch CMAKE_ON= BUILD_SHARED_LIBS CMAKE_OFF= BUILD_TESTING FAISS_ENABLE_GPU FAISS_ENABLE_PYTHON +post-extract: # workaround for https://github.com/facebookresearch/faiss/issues/3913 + @${LN} -s ${WRKSRC} ${WRKDIR}/faiss + # tests as of 1.12.0: 100% tests passed .include <bsd.port.mk> diff --git a/math/faiss/distinfo b/math/faiss/distinfo index 993ba750a6d7..f1243da453e8 100644 --- a/math/faiss/distinfo +++ b/math/faiss/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1757855190 -SHA256 (facebookresearch-faiss-v1.12.0_GH0.tar.gz) = 561376d1a44771bf1230fabeef9c81643468009b45a585382cf38d3a7a94990a -SIZE (facebookresearch-faiss-v1.12.0_GH0.tar.gz) = 1169676 +TIMESTAMP = 1763959029 +SHA256 (facebookresearch-faiss-v1.13.0_GH0.tar.gz) = 6db002fc020fb8d02adaafd06e1b3b8fb4f9301d25d18392e27eb6e63be0361b +SIZE (facebookresearch-faiss-v1.13.0_GH0.tar.gz) = 1214369 diff --git a/math/faiss/pkg-plist b/math/faiss/pkg-plist index af4874fd8148..8bf60e859d7a 100644 --- a/math/faiss/pkg-plist +++ b/math/faiss/pkg-plist @@ -21,11 +21,13 @@ include/faiss/IndexIVFAdditiveQuantizer.h include/faiss/IndexIVFAdditiveQuantizerFastScan.h include/faiss/IndexIVFFastScan.h include/faiss/IndexIVFFlat.h +include/faiss/IndexIVFFlatPanorama.h include/faiss/IndexIVFIndependentQuantizer.h include/faiss/IndexIVFPQ.h include/faiss/IndexIVFPQFastScan.h include/faiss/IndexIVFPQR.h include/faiss/IndexIVFRaBitQ.h +include/faiss/IndexIVFRaBitQFastScan.h include/faiss/IndexIVFSpectralHash.h include/faiss/IndexLSH.h include/faiss/IndexLattice.h @@ -36,6 +38,7 @@ include/faiss/IndexPQ.h include/faiss/IndexPQFastScan.h include/faiss/IndexPreTransform.h include/faiss/IndexRaBitQ.h +include/faiss/IndexRaBitQFastScan.h include/faiss/IndexRefine.h include/faiss/IndexReplicas.h include/faiss/IndexRowwiseMinMax.h @@ -53,17 +56,20 @@ include/faiss/impl/CodePacker.h include/faiss/impl/DistanceComputer.h include/faiss/impl/FaissAssert.h include/faiss/impl/FaissException.h +include/faiss/impl/FastScanDistancePostProcessing.h include/faiss/impl/HNSW.h include/faiss/impl/IDSelector.h include/faiss/impl/LocalSearchQuantizer.h include/faiss/impl/LookupTableScaler.h include/faiss/impl/NNDescent.h include/faiss/impl/NSG.h +include/faiss/impl/PanoramaStats.h include/faiss/impl/PolysemousTraining.h include/faiss/impl/ProductAdditiveQuantizer.h include/faiss/impl/ProductQuantizer-inl.h include/faiss/impl/ProductQuantizer.h include/faiss/impl/Quantizer.h +include/faiss/impl/RaBitQUtils.h include/faiss/impl/RaBitQuantizer.h include/faiss/impl/ResidualQuantizer.h include/faiss/impl/ResultHandler.h diff --git a/math/glm/Makefile b/math/glm/Makefile index 1d05e34a5d41..9c8ad5c88364 100644 --- a/math/glm/Makefile +++ b/math/glm/Makefile @@ -1,6 +1,5 @@ PORTNAME= glm -PORTVERSION= 1.0.1 -PORTEPOCH= 1 +PORTVERSION= 1.0.2 CATEGORIES= math graphics MAINTAINER= amdmi3@FreeBSD.org diff --git a/math/glm/distinfo b/math/glm/distinfo index 67f772622f58..fd1eb28fda75 100644 --- a/math/glm/distinfo +++ b/math/glm/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1709055434 -SHA256 (g-truc-glm-1.0.1_GH0.tar.gz) = 9f3174561fd26904b23f0db5e560971cbf9b3cbda0b280f04d5c379d03bf234c -SIZE (g-truc-glm-1.0.1_GH0.tar.gz) = 4567161 +TIMESTAMP = 1760555893 +SHA256 (g-truc-glm-1.0.2_GH0.tar.gz) = 19edf2e860297efab1c74950e6076bf4dad9de483826bc95e2e0f2c758a43f65 +SIZE (g-truc-glm-1.0.2_GH0.tar.gz) = 4597309 diff --git a/math/glm/files/patch-glm_gtx_bit.hpp b/math/glm/files/patch-glm_gtx_bit.hpp deleted file mode 100644 index 395022876680..000000000000 --- a/math/glm/files/patch-glm_gtx_bit.hpp +++ /dev/null @@ -1,60 +0,0 @@ -This is needed to fix x11-wm/gamescope with glm 1.0.1 - -https://github.com/g-truc/glm/issues/1269 - ---- glm/gtx/bit.hpp.orig 2024-02-27 17:19:47 UTC -+++ glm/gtx/bit.hpp -@@ -46,7 +46,7 @@ namespace glm - /// @see gtc_round - /// @see gtx_bit - template<typename genIUType> -- GLM_DEPRECATED GLM_FUNC_DECL genIUType powerOfTwoAbove(genIUType Value); -+ GLM_FUNC_DECL genIUType powerOfTwoAbove(genIUType Value); - - /// Return the power of two number which value is just higher the input value. - /// Deprecated, use ceilPowerOfTwo from GTC_round instead -@@ -54,7 +54,7 @@ namespace glm - /// @see gtc_round - /// @see gtx_bit - template<length_t L, typename T, qualifier Q> -- GLM_DEPRECATED GLM_FUNC_DECL vec<L, T, Q> powerOfTwoAbove(vec<L, T, Q> const& value); -+ GLM_FUNC_DECL vec<L, T, Q> powerOfTwoAbove(vec<L, T, Q> const& value); - - /// Return the power of two number which value is just lower the input value. - /// Deprecated, use floorPowerOfTwo from GTC_round instead -@@ -62,7 +62,7 @@ namespace glm - /// @see gtc_round - /// @see gtx_bit - template<typename genIUType> -- GLM_DEPRECATED GLM_FUNC_DECL genIUType powerOfTwoBelow(genIUType Value); -+ GLM_FUNC_DECL genIUType powerOfTwoBelow(genIUType Value); - - /// Return the power of two number which value is just lower the input value. - /// Deprecated, use floorPowerOfTwo from GTC_round instead -@@ -70,7 +70,7 @@ namespace glm - /// @see gtc_round - /// @see gtx_bit - template<length_t L, typename T, qualifier Q> -- GLM_DEPRECATED GLM_FUNC_DECL vec<L, T, Q> powerOfTwoBelow(vec<L, T, Q> const& value); -+ GLM_FUNC_DECL vec<L, T, Q> powerOfTwoBelow(vec<L, T, Q> const& value); - - /// Return the power of two number which value is the closet to the input value. - /// Deprecated, use roundPowerOfTwo from GTC_round instead -@@ -78,7 +78,7 @@ namespace glm - /// @see gtc_round - /// @see gtx_bit - template<typename genIUType> -- GLM_DEPRECATED GLM_FUNC_DECL genIUType powerOfTwoNearest(genIUType Value); -+ GLM_FUNC_DECL genIUType powerOfTwoNearest(genIUType Value); - - /// Return the power of two number which value is the closet to the input value. - /// Deprecated, use roundPowerOfTwo from GTC_round instead -@@ -86,7 +86,7 @@ namespace glm - /// @see gtc_round - /// @see gtx_bit - template<length_t L, typename T, qualifier Q> -- GLM_DEPRECATED GLM_FUNC_DECL vec<L, T, Q> powerOfTwoNearest(vec<L, T, Q> const& value); -+ GLM_FUNC_DECL vec<L, T, Q> powerOfTwoNearest(vec<L, T, Q> const& value); - - /// @} - } //namespace glm diff --git a/math/glm/files/patch-test_core_core__func_matrix.cpp b/math/glm/files/patch-test_core_core__func_matrix.cpp deleted file mode 100644 index 080676114d84..000000000000 --- a/math/glm/files/patch-test_core_core__func_matrix.cpp +++ /dev/null @@ -1,11 +0,0 @@ ---- test/core/core_func_matrix.cpp.orig 2024-02-27 17:19:47 UTC -+++ test/core/core_func_matrix.cpp -@@ -392,7 +392,7 @@ static int test_inverse_perf(std::size_t Count, std::s - //glm::uint Ulp = 0; - //Ulp = glm::max(glm::float_distance(*Dst, *Src), Ulp); - -- std::printf("inverse<%s>(%f): %lu\n", Message, static_cast<double>(Diff), EndTime - StartTime); -+ std::printf("inverse<%s>(%f): %lu\n", Message, static_cast<double>(Diff), (unsigned long)(EndTime - StartTime)); - - return 0; - } diff --git a/math/glm/pkg-plist b/math/glm/pkg-plist index 03669b99b210..f957760e51f7 100644 --- a/math/glm/pkg-plist +++ b/math/glm/pkg-plist @@ -60,7 +60,7 @@ include/glm/detail/type_vec3.hpp include/glm/detail/type_vec3.inl include/glm/detail/type_vec4.hpp include/glm/detail/type_vec4.inl -include/glm/detail/type_vec4_simd.inl +include/glm/detail/type_vec_simd.inl include/glm/exponential.hpp include/glm/ext.hpp include/glm/ext/_matrix_vectorize.hpp @@ -310,7 +310,7 @@ include/glm/gtx/fast_square_root.hpp include/glm/gtx/fast_square_root.inl include/glm/gtx/fast_trigonometry.hpp include/glm/gtx/fast_trigonometry.inl -include/glm/gtx/float_notmalize.inl +include/glm/gtx/float_normalize.inl include/glm/gtx/functions.hpp include/glm/gtx/functions.inl include/glm/gtx/gradient_paint.hpp @@ -325,6 +325,8 @@ include/glm/gtx/intersect.hpp include/glm/gtx/intersect.inl include/glm/gtx/io.hpp include/glm/gtx/io.inl +include/glm/gtx/iteration.hpp +include/glm/gtx/iteration.inl include/glm/gtx/log_base.hpp include/glm/gtx/log_base.inl include/glm/gtx/matrix_cross_product.hpp @@ -382,6 +384,8 @@ include/glm/gtx/std_based_type.hpp include/glm/gtx/std_based_type.inl include/glm/gtx/string_cast.hpp include/glm/gtx/string_cast.inl +include/glm/gtx/structured_bindings.hpp +include/glm/gtx/structured_bindings.inl include/glm/gtx/texture.hpp include/glm/gtx/texture.inl include/glm/gtx/transform.hpp diff --git a/math/hmat-oss/Makefile b/math/hmat-oss/Makefile index 044ccdb3589b..2bd76abb45d2 100644 --- a/math/hmat-oss/Makefile +++ b/math/hmat-oss/Makefile @@ -1,6 +1,5 @@ PORTNAME= hmat-oss -DISTVERSION= 1.10.0 -PORTREVISION= 2 +DISTVERSION= 1.11.0 CATEGORIES= math MAINTAINER= yuri@FreeBSD.org @@ -34,4 +33,6 @@ do-test: ${SETENV} ${MAKE_ENV} ${MAKE_CMD} ${MAKE_ARGS} ${ALL_TARGET} && \ ${SETENV} ${MAKE_ENV} ${MAKE_CMD} ${MAKE_ARGS} test +# tests as of 1.11.0: 100% tests passed, 0 tests failed out of 4 + .include <bsd.port.mk> diff --git a/math/hmat-oss/distinfo b/math/hmat-oss/distinfo index 74b49f00d9ac..ce2331158524 100644 --- a/math/hmat-oss/distinfo +++ b/math/hmat-oss/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1720985959 -SHA256 (jeromerobert-hmat-oss-1.10.0_GH0.tar.gz) = 357969e54d4d213cbab9c0eb4ca944a160d519b0790c8300431b4acc151387e5 -SIZE (jeromerobert-hmat-oss-1.10.0_GH0.tar.gz) = 203181 +TIMESTAMP = 1763928784 +SHA256 (jeromerobert-hmat-oss-1.11.0_GH0.tar.gz) = 111f5cf45eeb70ba5e377c970af118b914029d07088dc15f1c6e81afe470e26a +SIZE (jeromerobert-hmat-oss-1.11.0_GH0.tar.gz) = 205678 diff --git a/math/hmat-oss/files/patch-CMakeLists.txt b/math/hmat-oss/files/patch-CMakeLists.txt deleted file mode 100644 index 250754940b7a..000000000000 --- a/math/hmat-oss/files/patch-CMakeLists.txt +++ /dev/null @@ -1,14 +0,0 @@ ---- CMakeLists.txt.orig 2022-10-05 15:44:52 UTC -+++ CMakeLists.txt -@@ -255,9 +255,9 @@ include(CheckCCompilerFlag) - include(CheckCXXCompilerFlag) - - function(hmat_set_compiler_flags _TARGET_NAME) -- check_cxx_compiler_flag("-Werror -Wall" HAVE_COMPILER_WARNING_FLAGS) -+ check_cxx_compiler_flag("-Wall" HAVE_COMPILER_WARNING_FLAGS) - if(HAVE_COMPILER_WARNING_FLAGS) -- target_compile_options(${_TARGET_NAME} PRIVATE -Werror -Wall) -+ target_compile_options(${_TARGET_NAME} PRIVATE -Wall) - foreach(flag -Wno-sign-compare;-Wno-undefined-var-template;-Wno-unused-parameter) - string(REPLACE "-" "_" varname ${flag}) - check_cxx_compiler_flag("${flag}" CXX${varname}) diff --git a/math/kahip/Makefile b/math/kahip/Makefile index d7f128842137..8d4ea7f28cea 100644 --- a/math/kahip/Makefile +++ b/math/kahip/Makefile @@ -1,6 +1,6 @@ PORTNAME= kahip DISTVERSIONPREFIX= v -DISTVERSION= 3.21 +DISTVERSION= 3.22 CATEGORIES= math MAINTAINER= yuri@FreeBSD.org diff --git a/math/kahip/distinfo b/math/kahip/distinfo index 2d947fbb8801..b40ff7be9803 100644 --- a/math/kahip/distinfo +++ b/math/kahip/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1762420421 -SHA256 (KaHIP-KaHIP-v3.21_GH0.tar.gz) = 0c3d53e211a9c880a8466839235f218591f2ecefce62bbf04afc8adfdb9c1e65 -SIZE (KaHIP-KaHIP-v3.21_GH0.tar.gz) = 2468901 +TIMESTAMP = 1763957535 +SHA256 (KaHIP-KaHIP-v3.22_GH0.tar.gz) = 3cbadfbf8d503351d921531413d3b66ad347a6d6e213120db87462093bb66b7c +SIZE (KaHIP-KaHIP-v3.22_GH0.tar.gz) = 2469773 diff --git a/math/lean4/Makefile b/math/lean4/Makefile index c6d417be8716..30652dafea6b 100644 --- a/math/lean4/Makefile +++ b/math/lean4/Makefile @@ -1,6 +1,6 @@ PORTNAME= lean4 DISTVERSIONPREFIX= v -DISTVERSION= 4.23.0 +DISTVERSION= 4.25.2 CATEGORIES= math lang devel # lean4 is primarily a math theorem prover, but it is also a language and a development environment MAINTAINER= yuri@FreeBSD.org @@ -32,7 +32,6 @@ CXXFLAGS+= -fPIC CMAKE_OFF= USE_MIMALLOC #MAKE_ARGS+= V=1 VERBOSE=1 -#MAKE_JOBS_UNSAFE= yes MAKE_ENV= LD_LIBRARY_PATH=${BUILD_WRKSRC}/stage0/lib/lean BINARY_ALIAS= make=${GMAKE} python=${PYTHON_CMD} @@ -48,6 +47,19 @@ pre-everything:: @${ECHO_MSG} " # mount /proc" @${ECHO_MSG} "" +post-patch: + # Add weakLeancArgs = ["-fPIC"] to all test lakefile.toml files + @${FIND} ${WRKSRC}/tests -name "lakefile.toml" | while read f; do \ + ${GREP} -q "weakLeancArgs" "$$f" || \ + ( ${PRINTF} 'weakLeancArgs = ["-fPIC"]\n\n' | cat - "$$f" > "$$f.tmp" && ${MV} "$$f.tmp" "$$f" ); \ + done + # Add weakLeancArgs to lakefile.lean files that define packages + @${FIND} ${WRKSRC}/tests -name "lakefile.lean" | while read f; do \ + if ${GREP} -q "^package .* where" "$$f" && ! ${GREP} -q "weakLeancArgs" "$$f"; then \ + ${AWK} '/^package .* where$$/ {print; print " weakLeancArgs := #[\"-fPIC\"]"; next} 1' "$$f" > "$$f.tmp" && ${MV} "$$f.tmp" "$$f"; \ + fi; \ + done + post-install: # remove empty dirs @${FIND} ${STAGEDIR}${DATADIR} -type d -empty -delete @@ -65,7 +77,6 @@ post-install: lib/lean/libleanshared_1.so \ lib/lean/libLake_shared.so -# tests as of 4.20.0: 99% tests passed, 16 tests failed out of 2594, see https://github.com/leanprover/lean4/issues/8628 -# tests as of 4.23.0: 99% tests passed, 10 tests failed out of 2870 +# tests as of 4.25.2: 100% tests passed, 0 tests failed out of 3241 .include <bsd.port.mk> diff --git a/math/lean4/distinfo b/math/lean4/distinfo index da328bb6517b..ca359438cd41 100644 --- a/math/lean4/distinfo +++ b/math/lean4/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1758525947 -SHA256 (leanprover-lean4-v4.23.0_GH0.tar.gz) = 1820cc8fc09f439c448ea39cc14f90e73058c55b12b5aa5cf4d2ca86f0c89099 -SIZE (leanprover-lean4-v4.23.0_GH0.tar.gz) = 45087678 +TIMESTAMP = 1764048066 +SHA256 (leanprover-lean4-v4.25.2_GH0.tar.gz) = 831b1d1d3833791e68de087d8f576c4703a5dd82157dd19364629f5df7fcfb2c +SIZE (leanprover-lean4-v4.25.2_GH0.tar.gz) = 50069767 diff --git a/math/lean4/files/patch-src_CMakeLists.txt b/math/lean4/files/patch-src_CMakeLists.txt index d7658e68a521..d71c117b8802 100644 --- a/math/lean4/files/patch-src_CMakeLists.txt +++ b/math/lean4/files/patch-src_CMakeLists.txt @@ -1,6 +1,6 @@ ---- src/CMakeLists.txt.orig 2025-05-07 10:26:21 UTC +--- src/CMakeLists.txt.orig 2025-11-18 02:29:21 UTC +++ src/CMakeLists.txt -@@ -472,6 +472,16 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") +@@ -473,6 +473,17 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive") string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean") @@ -14,10 +14,21 @@ + string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") + string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive") + string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean") ++ set(LEAN_EXTRA_LAKEFILE_TOML "weakLeancArgs = [\"-fPIC\"]") elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec") string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib") -@@ -801,7 +811,7 @@ endif() +@@ -586,6 +597,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu + # Lean code only needs this one include + string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/include") + ++# Include extra flags (e.g., -fPIC on FreeBSD) ++string(APPEND LEANC_OPTS " ${LEANC_EXTRA_FLAGS}") ++ + # Use CMake profile C++ flags for building Lean libraries, but do not embed in `leanc` + string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE) + string(APPEND LEANC_OPTS " ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}") +@@ -814,7 +828,7 @@ endif() file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC) endif() diff --git a/math/lean4/files/patch-src_bin_leanc.in b/math/lean4/files/patch-src_bin_leanc.in deleted file mode 100644 index 6b110ae220b3..000000000000 --- a/math/lean4/files/patch-src_bin_leanc.in +++ /dev/null @@ -1,11 +0,0 @@ ---- src/bin/leanc.in.orig 2025-05-07 10:26:21 UTC -+++ src/bin/leanc.in -@@ -7,7 +7,7 @@ done - [[ "$arg" = "-c" ]] && ldflags=() - [[ "$arg" = "-v" ]] && v=1 - done --cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_CC_FLAGS@ @LEANC_INTERNAL_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument) -+cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_CC_FLAGS@ @LEANC_INTERNAL_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument -fPIC) - cmd=$(printf '%q ' "${cmd[@]}" | sed "s!ROOT!$root!g") - [[ $v == 1 ]] && echo $cmd - eval $cmd diff --git a/math/lean4/files/patch-src_runtime_io.cpp b/math/lean4/files/patch-src_runtime_io.cpp index 2e185dfb816c..8fe17f4e138b 100644 --- a/math/lean4/files/patch-src_runtime_io.cpp +++ b/math/lean4/files/patch-src_runtime_io.cpp @@ -1,12 +1,11 @@ ---- src/runtime/io.cpp.orig 2025-05-06 09:12:17 UTC +--- src/runtime/io.cpp.orig 2025-11-18 02:29:21 UTC +++ src/runtime/io.cpp -@@ -1253,7 +1253,13 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_ar +@@ -1365,7 +1365,13 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_ar char dest[PATH_MAX]; memset(dest, 0, PATH_MAX); pid_t pid = getpid(); -- snprintf(path, PATH_MAX, "/proc/%d/exe", pid); +#if defined(__linux__) -+ snprintf(path, PATH_MAX, "/proc/%d/exe", pid); + snprintf(path, PATH_MAX, "/proc/%d/exe", pid); +#elif defined(__FreeBSD__) + snprintf(path, PATH_MAX, "/proc/%d/file", pid); +#else diff --git a/math/lean4/files/patch-src_runtime_stack__overflow.cpp b/math/lean4/files/patch-src_runtime_stack__overflow.cpp index cdd63ffde32a..e888a55cfead 100644 --- a/math/lean4/files/patch-src_runtime_stack__overflow.cpp +++ b/math/lean4/files/patch-src_runtime_stack__overflow.cpp @@ -1,11 +1,13 @@ ---- src/runtime/stack_overflow.cpp.orig 2025-05-06 09:12:17 UTC +--- src/runtime/stack_overflow.cpp.orig 2025-11-18 02:29:21 UTC +++ src/runtime/stack_overflow.cpp -@@ -21,6 +21,9 @@ Port of the corresponding Rust code (see links below). +@@ -21,6 +21,11 @@ Port of the corresponding Rust code (see links below). #include <initializer_list> #include "runtime/stack_overflow.h" ++#if defined(__FreeBSD__) +#include <pthread_np.h> +#define pthread_getattr_np pthread_attr_get_np ++#endif + namespace lean { // stack guard of the main thread diff --git a/math/lean4/files/patch-src_shell_CMakeLists.txt b/math/lean4/files/patch-src_shell_CMakeLists.txt new file mode 100644 index 000000000000..68de472208ff --- /dev/null +++ b/math/lean4/files/patch-src_shell_CMakeLists.txt @@ -0,0 +1,11 @@ +--- src/shell/CMakeLists.txt.orig 2025-11-18 02:29:21 UTC ++++ src/shell/CMakeLists.txt +@@ -57,7 +57,7 @@ endif() + endif() + + # LEANC_OPTS in CXX is necessary for macOS c++ to find its headers +-set(TEST_VARS "PATH=${LEAN_BIN}:$PATH ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'") ++set(TEST_VARS "PATH=${LEAN_BIN}:$PATH LD_LIBRARY_PATH=${CMAKE_BINARY_DIR}/lib/lean:\${LD_LIBRARY_PATH:-} ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'") + + # LEAN TESTS + file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") diff --git a/math/lean4/files/patch-stage0_src_CMakeLists.txt b/math/lean4/files/patch-stage0_src_CMakeLists.txt index 184415ffa3d9..7ec7241aa2f2 100644 --- a/math/lean4/files/patch-stage0_src_CMakeLists.txt +++ b/math/lean4/files/patch-stage0_src_CMakeLists.txt @@ -1,6 +1,6 @@ ---- stage0/src/CMakeLists.txt.orig 2025-05-06 09:12:17 UTC +--- stage0/src/CMakeLists.txt.orig 2025-11-18 02:29:21 UTC +++ stage0/src/CMakeLists.txt -@@ -472,6 +472,16 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") +@@ -473,6 +473,17 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive") string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean") @@ -14,10 +14,21 @@ + string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") + string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive") + string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean") ++ set(LEAN_EXTRA_LAKEFILE_TOML "weakLeancArgs = [\"-fPIC\"]") elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec") string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib") -@@ -798,7 +808,7 @@ endif() +@@ -586,6 +597,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu + # Lean code only needs this one include + string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/include") + ++# Include extra flags (e.g., -fPIC on FreeBSD) ++string(APPEND LEANC_OPTS " ${LEANC_EXTRA_FLAGS}") ++ + # Use CMake profile C++ flags for building Lean libraries, but do not embed in `leanc` + string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE) + string(APPEND LEANC_OPTS " ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}") +@@ -814,7 +828,7 @@ endif() file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC) endif() diff --git a/math/lean4/files/patch-stage0_src_bin_leanc.in b/math/lean4/files/patch-stage0_src_bin_leanc.in deleted file mode 100644 index a6f3f345b929..000000000000 --- a/math/lean4/files/patch-stage0_src_bin_leanc.in +++ /dev/null @@ -1,11 +0,0 @@ ---- stage0/src/bin/leanc.in.orig 2025-05-07 10:26:21 UTC -+++ stage0/src/bin/leanc.in -@@ -7,7 +7,7 @@ done - [[ "$arg" = "-c" ]] && ldflags=() - [[ "$arg" = "-v" ]] && v=1 - done --cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_CC_FLAGS@ @LEANC_INTERNAL_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument) -+cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_CC_FLAGS@ @LEANC_INTERNAL_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument -fPIC) - cmd=$(printf '%q ' "${cmd[@]}" | sed "s!ROOT!$root!g") - [[ $v == 1 ]] && echo $cmd - eval $cmd diff --git a/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp b/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp index 638daf3af176..cb4949c8e4d2 100644 --- a/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp +++ b/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp @@ -11,11 +11,3 @@ #ifdef LEAN_WINDOWS #include <windows.h> #else -@@ -20,6 +24,7 @@ Port of the corresponding Rust code (see links below). - #include <lean/lean.h> - #include <initializer_list> - #include "runtime/stack_overflow.h" -+ - - namespace lean { - // stack guard of the main thread diff --git a/math/lean4/files/patch-stage0_src_shell_CMakeLists.txt b/math/lean4/files/patch-stage0_src_shell_CMakeLists.txt new file mode 100644 index 000000000000..bd9010ce3d9b --- /dev/null +++ b/math/lean4/files/patch-stage0_src_shell_CMakeLists.txt @@ -0,0 +1,11 @@ +--- stage0/src/shell/CMakeLists.txt.orig 2025-11-18 02:29:21 UTC ++++ stage0/src/shell/CMakeLists.txt +@@ -57,7 +57,7 @@ endif() + endif() + + # LEANC_OPTS in CXX is necessary for macOS c++ to find its headers +-set(TEST_VARS "PATH=${LEAN_BIN}:$PATH ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'") ++set(TEST_VARS "PATH=${LEAN_BIN}:$PATH LD_LIBRARY_PATH=${CMAKE_BINARY_DIR}/lib/lean:\${LD_LIBRARY_PATH:-} ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'") + + # LEAN TESTS + file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") diff --git a/math/lean4/files/patch-tests_lakefile.toml b/math/lean4/files/patch-tests_lakefile.toml new file mode 100644 index 000000000000..3a01b013943d --- /dev/null +++ b/math/lean4/files/patch-tests_lakefile.toml @@ -0,0 +1,10 @@ +--- tests/lakefile.toml.orig 2025-11-17 18:29:21 UTC ++++ tests/lakefile.toml +@@ -1,5 +1,7 @@ + name = "tests" + ++weakLeancArgs = ["-fPIC"] ++ + # Allow `module` in tests when opened in the language server. + # Enabled during actual test runs in the respective test_single.sh. + moreGlobalServerArgs = ["-Dexperimental.module=true"] diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist index 20f5d941e24a..b35afb3ef8ff 100644 --- a/math/lean4/pkg-plist +++ b/math/lean4/pkg-plist @@ -377,6 +377,21 @@ lib/lean/Init/Data/ByteArray/Basic.ir lib/lean/Init/Data/ByteArray/Basic.olean lib/lean/Init/Data/ByteArray/Basic.olean.private lib/lean/Init/Data/ByteArray/Basic.olean.server +lib/lean/Init/Data/ByteArray/Bootstrap.ilean +lib/lean/Init/Data/ByteArray/Bootstrap.ir +lib/lean/Init/Data/ByteArray/Bootstrap.olean +lib/lean/Init/Data/ByteArray/Bootstrap.olean.private +lib/lean/Init/Data/ByteArray/Bootstrap.olean.server +lib/lean/Init/Data/ByteArray/Extra.ilean +lib/lean/Init/Data/ByteArray/Extra.ir +lib/lean/Init/Data/ByteArray/Extra.olean +lib/lean/Init/Data/ByteArray/Extra.olean.private +lib/lean/Init/Data/ByteArray/Extra.olean.server +lib/lean/Init/Data/ByteArray/Lemmas.ilean +lib/lean/Init/Data/ByteArray/Lemmas.ir +lib/lean/Init/Data/ByteArray/Lemmas.olean +lib/lean/Init/Data/ByteArray/Lemmas.olean.private +lib/lean/Init/Data/ByteArray/Lemmas.olean.server lib/lean/Init/Data/Cast.ilean lib/lean/Init/Data/Cast.ir lib/lean/Init/Data/Cast.olean @@ -402,6 +417,31 @@ lib/lean/Init/Data/Char/Order.ir lib/lean/Init/Data/Char/Order.olean lib/lean/Init/Data/Char/Order.olean.private lib/lean/Init/Data/Char/Order.olean.server +lib/lean/Init/Data/Dyadic.ilean +lib/lean/Init/Data/Dyadic.ir +lib/lean/Init/Data/Dyadic.olean +lib/lean/Init/Data/Dyadic.olean.private +lib/lean/Init/Data/Dyadic.olean.server +lib/lean/Init/Data/Dyadic/Basic.ilean +lib/lean/Init/Data/Dyadic/Basic.ir +lib/lean/Init/Data/Dyadic/Basic.olean +lib/lean/Init/Data/Dyadic/Basic.olean.private +lib/lean/Init/Data/Dyadic/Basic.olean.server +lib/lean/Init/Data/Dyadic/Instances.ilean +lib/lean/Init/Data/Dyadic/Instances.ir +lib/lean/Init/Data/Dyadic/Instances.olean +lib/lean/Init/Data/Dyadic/Instances.olean.private +lib/lean/Init/Data/Dyadic/Instances.olean.server +lib/lean/Init/Data/Dyadic/Inv.ilean +lib/lean/Init/Data/Dyadic/Inv.ir +lib/lean/Init/Data/Dyadic/Inv.olean +lib/lean/Init/Data/Dyadic/Inv.olean.private +lib/lean/Init/Data/Dyadic/Inv.olean.server +lib/lean/Init/Data/Dyadic/Round.ilean +lib/lean/Init/Data/Dyadic/Round.ir +lib/lean/Init/Data/Dyadic/Round.olean +lib/lean/Init/Data/Dyadic/Round.olean.private +lib/lean/Init/Data/Dyadic/Round.olean.server lib/lean/Init/Data/Fin.ilean lib/lean/Init/Data/Fin.ir lib/lean/Init/Data/Fin.olean @@ -607,6 +647,11 @@ lib/lean/Init/Data/Iterators/Combinators/FilterMap.ir lib/lean/Init/Data/Iterators/Combinators/FilterMap.olean lib/lean/Init/Data/Iterators/Combinators/FilterMap.olean.private lib/lean/Init/Data/Iterators/Combinators/FilterMap.olean.server +lib/lean/Init/Data/Iterators/Combinators/FlatMap.ilean +lib/lean/Init/Data/Iterators/Combinators/FlatMap.ir +lib/lean/Init/Data/Iterators/Combinators/FlatMap.olean +lib/lean/Init/Data/Iterators/Combinators/FlatMap.olean.private +lib/lean/Init/Data/Iterators/Combinators/FlatMap.olean.server lib/lean/Init/Data/Iterators/Combinators/Monadic.ilean lib/lean/Init/Data/Iterators/Combinators/Monadic.ir lib/lean/Init/Data/Iterators/Combinators/Monadic.olean @@ -622,6 +667,11 @@ lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.ir lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.olean lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.olean.private lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.olean.server +lib/lean/Init/Data/Iterators/Combinators/Monadic/FlatMap.ilean +lib/lean/Init/Data/Iterators/Combinators/Monadic/FlatMap.ir +lib/lean/Init/Data/Iterators/Combinators/Monadic/FlatMap.olean +lib/lean/Init/Data/Iterators/Combinators/Monadic/FlatMap.olean.private +lib/lean/Init/Data/Iterators/Combinators/Monadic/FlatMap.olean.server lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.ilean lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.ir lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.olean @@ -727,6 +777,11 @@ lib/lean/Init/Data/Iterators/Lemmas/Combinators/FilterMap.ir lib/lean/Init/Data/Iterators/Lemmas/Combinators/FilterMap.olean lib/lean/Init/Data/Iterators/Lemmas/Combinators/FilterMap.olean.private lib/lean/Init/Data/Iterators/Lemmas/Combinators/FilterMap.olean.server +lib/lean/Init/Data/Iterators/Lemmas/Combinators/FlatMap.ilean +lib/lean/Init/Data/Iterators/Lemmas/Combinators/FlatMap.ir +lib/lean/Init/Data/Iterators/Lemmas/Combinators/FlatMap.olean +lib/lean/Init/Data/Iterators/Lemmas/Combinators/FlatMap.olean.private +lib/lean/Init/Data/Iterators/Lemmas/Combinators/FlatMap.olean.server lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic.ilean lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic.ir lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic.olean @@ -742,6 +797,11 @@ lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.ir lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.olean lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.olean.private lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.olean.server +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.ilean +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.ir +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.olean +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.olean.private +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.olean.server lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.ilean lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.ir lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.olean @@ -797,6 +857,11 @@ lib/lean/Init/Data/Iterators/ToIterator.ir lib/lean/Init/Data/Iterators/ToIterator.olean lib/lean/Init/Data/Iterators/ToIterator.olean.private lib/lean/Init/Data/Iterators/ToIterator.olean.server +lib/lean/Init/Data/LawfulHashable.ilean +lib/lean/Init/Data/LawfulHashable.ir +lib/lean/Init/Data/LawfulHashable.olean +lib/lean/Init/Data/LawfulHashable.olean.private +lib/lean/Init/Data/LawfulHashable.olean.server lib/lean/Init/Data/List.ilean lib/lean/Init/Data/List.ir lib/lean/Init/Data/List.olean @@ -1042,6 +1107,11 @@ lib/lean/Init/Data/Nat/Control.ir lib/lean/Init/Data/Nat/Control.olean lib/lean/Init/Data/Nat/Control.olean.private lib/lean/Init/Data/Nat/Control.olean.server +lib/lean/Init/Data/Nat/Coprime.ilean +lib/lean/Init/Data/Nat/Coprime.ir +lib/lean/Init/Data/Nat/Coprime.olean +lib/lean/Init/Data/Nat/Coprime.olean.private +lib/lean/Init/Data/Nat/Coprime.olean.server lib/lean/Init/Data/Nat/Div.ilean lib/lean/Init/Data/Nat/Div.ir lib/lean/Init/Data/Nat/Div.olean @@ -1187,6 +1257,41 @@ lib/lean/Init/Data/Ord.ir lib/lean/Init/Data/Ord.olean lib/lean/Init/Data/Ord.olean.private lib/lean/Init/Data/Ord.olean.server +lib/lean/Init/Data/Ord/Array.ilean +lib/lean/Init/Data/Ord/Array.ir +lib/lean/Init/Data/Ord/Array.olean +lib/lean/Init/Data/Ord/Array.olean.private +lib/lean/Init/Data/Ord/Array.olean.server +lib/lean/Init/Data/Ord/Basic.ilean +lib/lean/Init/Data/Ord/Basic.ir +lib/lean/Init/Data/Ord/Basic.olean +lib/lean/Init/Data/Ord/Basic.olean.private +lib/lean/Init/Data/Ord/Basic.olean.server +lib/lean/Init/Data/Ord/BitVec.ilean +lib/lean/Init/Data/Ord/BitVec.ir +lib/lean/Init/Data/Ord/BitVec.olean +lib/lean/Init/Data/Ord/BitVec.olean.private +lib/lean/Init/Data/Ord/BitVec.olean.server +lib/lean/Init/Data/Ord/SInt.ilean +lib/lean/Init/Data/Ord/SInt.ir +lib/lean/Init/Data/Ord/SInt.olean +lib/lean/Init/Data/Ord/SInt.olean.private +lib/lean/Init/Data/Ord/SInt.olean.server +lib/lean/Init/Data/Ord/String.ilean +lib/lean/Init/Data/Ord/String.ir +lib/lean/Init/Data/Ord/String.olean +lib/lean/Init/Data/Ord/String.olean.private +lib/lean/Init/Data/Ord/String.olean.server +lib/lean/Init/Data/Ord/UInt.ilean +lib/lean/Init/Data/Ord/UInt.ir +lib/lean/Init/Data/Ord/UInt.olean +lib/lean/Init/Data/Ord/UInt.olean.private +lib/lean/Init/Data/Ord/UInt.olean.server +lib/lean/Init/Data/Ord/Vector.ilean +lib/lean/Init/Data/Ord/Vector.ir +lib/lean/Init/Data/Ord/Vector.olean +lib/lean/Init/Data/Ord/Vector.olean.private +lib/lean/Init/Data/Ord/Vector.olean.server lib/lean/Init/Data/Order.ilean lib/lean/Init/Data/Order.ir lib/lean/Init/Data/Order.olean @@ -1197,16 +1302,41 @@ lib/lean/Init/Data/Order/Classes.ir lib/lean/Init/Data/Order/Classes.olean lib/lean/Init/Data/Order/Classes.olean.private lib/lean/Init/Data/Order/Classes.olean.server +lib/lean/Init/Data/Order/ClassesExtra.ilean +lib/lean/Init/Data/Order/ClassesExtra.ir +lib/lean/Init/Data/Order/ClassesExtra.olean +lib/lean/Init/Data/Order/ClassesExtra.olean.private +lib/lean/Init/Data/Order/ClassesExtra.olean.server lib/lean/Init/Data/Order/Factories.ilean lib/lean/Init/Data/Order/Factories.ir lib/lean/Init/Data/Order/Factories.olean lib/lean/Init/Data/Order/Factories.olean.private lib/lean/Init/Data/Order/Factories.olean.server +lib/lean/Init/Data/Order/FactoriesExtra.ilean +lib/lean/Init/Data/Order/FactoriesExtra.ir +lib/lean/Init/Data/Order/FactoriesExtra.olean +lib/lean/Init/Data/Order/FactoriesExtra.olean.private +lib/lean/Init/Data/Order/FactoriesExtra.olean.server lib/lean/Init/Data/Order/Lemmas.ilean lib/lean/Init/Data/Order/Lemmas.ir lib/lean/Init/Data/Order/Lemmas.olean lib/lean/Init/Data/Order/Lemmas.olean.private lib/lean/Init/Data/Order/Lemmas.olean.server +lib/lean/Init/Data/Order/LemmasExtra.ilean +lib/lean/Init/Data/Order/LemmasExtra.ir +lib/lean/Init/Data/Order/LemmasExtra.olean +lib/lean/Init/Data/Order/LemmasExtra.olean.private +lib/lean/Init/Data/Order/LemmasExtra.olean.server +lib/lean/Init/Data/Order/Ord.ilean +lib/lean/Init/Data/Order/Ord.ir +lib/lean/Init/Data/Order/Ord.olean +lib/lean/Init/Data/Order/Ord.olean.private +lib/lean/Init/Data/Order/Ord.olean.server +lib/lean/Init/Data/Order/PackageFactories.ilean +lib/lean/Init/Data/Order/PackageFactories.ir +lib/lean/Init/Data/Order/PackageFactories.olean +lib/lean/Init/Data/Order/PackageFactories.olean.private +lib/lean/Init/Data/Order/PackageFactories.olean.server lib/lean/Init/Data/PLift.ilean lib/lean/Init/Data/PLift.ir lib/lean/Init/Data/PLift.olean @@ -1257,6 +1387,31 @@ lib/lean/Init/Data/Range/Polymorphic/Basic.ir lib/lean/Init/Data/Range/Polymorphic/Basic.olean lib/lean/Init/Data/Range/Polymorphic/Basic.olean.private lib/lean/Init/Data/Range/Polymorphic/Basic.olean.server +lib/lean/Init/Data/Range/Polymorphic/BitVec.ilean +lib/lean/Init/Data/Range/Polymorphic/BitVec.ir +lib/lean/Init/Data/Range/Polymorphic/BitVec.olean +lib/lean/Init/Data/Range/Polymorphic/BitVec.olean.private +lib/lean/Init/Data/Range/Polymorphic/BitVec.olean.server +lib/lean/Init/Data/Range/Polymorphic/GetElemTactic.ilean +lib/lean/Init/Data/Range/Polymorphic/GetElemTactic.ir +lib/lean/Init/Data/Range/Polymorphic/GetElemTactic.olean +lib/lean/Init/Data/Range/Polymorphic/GetElemTactic.olean.private +lib/lean/Init/Data/Range/Polymorphic/GetElemTactic.olean.server +lib/lean/Init/Data/Range/Polymorphic/Instances.ilean +lib/lean/Init/Data/Range/Polymorphic/Instances.ir +lib/lean/Init/Data/Range/Polymorphic/Instances.olean +lib/lean/Init/Data/Range/Polymorphic/Instances.olean.private +lib/lean/Init/Data/Range/Polymorphic/Instances.olean.server +lib/lean/Init/Data/Range/Polymorphic/Int.ilean +lib/lean/Init/Data/Range/Polymorphic/Int.ir +lib/lean/Init/Data/Range/Polymorphic/Int.olean +lib/lean/Init/Data/Range/Polymorphic/Int.olean.private +lib/lean/Init/Data/Range/Polymorphic/Int.olean.server +lib/lean/Init/Data/Range/Polymorphic/Internal/SignedBitVec.ilean +lib/lean/Init/Data/Range/Polymorphic/Internal/SignedBitVec.ir +lib/lean/Init/Data/Range/Polymorphic/Internal/SignedBitVec.olean +lib/lean/Init/Data/Range/Polymorphic/Internal/SignedBitVec.olean.private +lib/lean/Init/Data/Range/Polymorphic/Internal/SignedBitVec.olean.server lib/lean/Init/Data/Range/Polymorphic/Iterators.ilean lib/lean/Init/Data/Range/Polymorphic/Iterators.ir lib/lean/Init/Data/Range/Polymorphic/Iterators.olean @@ -1287,16 +1442,41 @@ lib/lean/Init/Data/Range/Polymorphic/RangeIterator.ir lib/lean/Init/Data/Range/Polymorphic/RangeIterator.olean lib/lean/Init/Data/Range/Polymorphic/RangeIterator.olean.private lib/lean/Init/Data/Range/Polymorphic/RangeIterator.olean.server +lib/lean/Init/Data/Range/Polymorphic/SInt.ilean +lib/lean/Init/Data/Range/Polymorphic/SInt.ir +lib/lean/Init/Data/Range/Polymorphic/SInt.olean +lib/lean/Init/Data/Range/Polymorphic/SInt.olean.private +lib/lean/Init/Data/Range/Polymorphic/SInt.olean.server lib/lean/Init/Data/Range/Polymorphic/Stream.ilean lib/lean/Init/Data/Range/Polymorphic/Stream.ir lib/lean/Init/Data/Range/Polymorphic/Stream.olean lib/lean/Init/Data/Range/Polymorphic/Stream.olean.private lib/lean/Init/Data/Range/Polymorphic/Stream.olean.server +lib/lean/Init/Data/Range/Polymorphic/UInt.ilean +lib/lean/Init/Data/Range/Polymorphic/UInt.ir +lib/lean/Init/Data/Range/Polymorphic/UInt.olean +lib/lean/Init/Data/Range/Polymorphic/UInt.olean.private +lib/lean/Init/Data/Range/Polymorphic/UInt.olean.server lib/lean/Init/Data/Range/Polymorphic/UpwardEnumerable.ilean lib/lean/Init/Data/Range/Polymorphic/UpwardEnumerable.ir lib/lean/Init/Data/Range/Polymorphic/UpwardEnumerable.olean lib/lean/Init/Data/Range/Polymorphic/UpwardEnumerable.olean.private lib/lean/Init/Data/Range/Polymorphic/UpwardEnumerable.olean.server +lib/lean/Init/Data/Rat.ilean +lib/lean/Init/Data/Rat.ir +lib/lean/Init/Data/Rat.olean +lib/lean/Init/Data/Rat.olean.private +lib/lean/Init/Data/Rat.olean.server +lib/lean/Init/Data/Rat/Basic.ilean +lib/lean/Init/Data/Rat/Basic.ir +lib/lean/Init/Data/Rat/Basic.olean +lib/lean/Init/Data/Rat/Basic.olean.private +lib/lean/Init/Data/Rat/Basic.olean.server +lib/lean/Init/Data/Rat/Lemmas.ilean +lib/lean/Init/Data/Rat/Lemmas.ir +lib/lean/Init/Data/Rat/Lemmas.olean +lib/lean/Init/Data/Rat/Lemmas.olean.private +lib/lean/Init/Data/Rat/Lemmas.olean.server lib/lean/Init/Data/Repr.ilean lib/lean/Init/Data/Repr.ir lib/lean/Init/Data/Repr.olean @@ -1392,6 +1572,16 @@ lib/lean/Init/Data/String/Basic.ir lib/lean/Init/Data/String/Basic.olean lib/lean/Init/Data/String/Basic.olean.private lib/lean/Init/Data/String/Basic.olean.server +lib/lean/Init/Data/String/Bootstrap.ilean +lib/lean/Init/Data/String/Bootstrap.ir +lib/lean/Init/Data/String/Bootstrap.olean +lib/lean/Init/Data/String/Bootstrap.olean.private +lib/lean/Init/Data/String/Bootstrap.olean.server +lib/lean/Init/Data/String/Decode.ilean +lib/lean/Init/Data/String/Decode.ir +lib/lean/Init/Data/String/Decode.olean +lib/lean/Init/Data/String/Decode.olean.private +lib/lean/Init/Data/String/Decode.olean.server lib/lean/Init/Data/String/Extra.ilean lib/lean/Init/Data/String/Extra.ir lib/lean/Init/Data/String/Extra.olean @@ -1402,6 +1592,46 @@ lib/lean/Init/Data/String/Lemmas.ir lib/lean/Init/Data/String/Lemmas.olean lib/lean/Init/Data/String/Lemmas.olean.private lib/lean/Init/Data/String/Lemmas.olean.server +lib/lean/Init/Data/String/Pattern.ilean +lib/lean/Init/Data/String/Pattern.ir +lib/lean/Init/Data/String/Pattern.olean +lib/lean/Init/Data/String/Pattern.olean.private +lib/lean/Init/Data/String/Pattern.olean.server +lib/lean/Init/Data/String/Pattern/Basic.ilean +lib/lean/Init/Data/String/Pattern/Basic.ir +lib/lean/Init/Data/String/Pattern/Basic.olean +lib/lean/Init/Data/String/Pattern/Basic.olean.private +lib/lean/Init/Data/String/Pattern/Basic.olean.server +lib/lean/Init/Data/String/Pattern/Char.ilean +lib/lean/Init/Data/String/Pattern/Char.ir +lib/lean/Init/Data/String/Pattern/Char.olean +lib/lean/Init/Data/String/Pattern/Char.olean.private +lib/lean/Init/Data/String/Pattern/Char.olean.server +lib/lean/Init/Data/String/Pattern/Pred.ilean +lib/lean/Init/Data/String/Pattern/Pred.ir +lib/lean/Init/Data/String/Pattern/Pred.olean +lib/lean/Init/Data/String/Pattern/Pred.olean.private +lib/lean/Init/Data/String/Pattern/Pred.olean.server +lib/lean/Init/Data/String/Pattern/String.ilean +lib/lean/Init/Data/String/Pattern/String.ir +lib/lean/Init/Data/String/Pattern/String.olean +lib/lean/Init/Data/String/Pattern/String.olean.private +lib/lean/Init/Data/String/Pattern/String.olean.server +lib/lean/Init/Data/String/Repr.ilean +lib/lean/Init/Data/String/Repr.ir +lib/lean/Init/Data/String/Repr.olean +lib/lean/Init/Data/String/Repr.olean.private +lib/lean/Init/Data/String/Repr.olean.server +lib/lean/Init/Data/String/Slice.ilean +lib/lean/Init/Data/String/Slice.ir +lib/lean/Init/Data/String/Slice.olean +lib/lean/Init/Data/String/Slice.olean.private +lib/lean/Init/Data/String/Slice.olean.server +lib/lean/Init/Data/String/Stream.ilean +lib/lean/Init/Data/String/Stream.ir +lib/lean/Init/Data/String/Stream.olean +lib/lean/Init/Data/String/Stream.olean.private +lib/lean/Init/Data/String/Stream.olean.server lib/lean/Init/Data/Subtype.ilean lib/lean/Init/Data/Subtype.ir lib/lean/Init/Data/Subtype.olean @@ -1452,6 +1682,11 @@ lib/lean/Init/Data/ToString/Macro.ir lib/lean/Init/Data/ToString/Macro.olean lib/lean/Init/Data/ToString/Macro.olean.private lib/lean/Init/Data/ToString/Macro.olean.server +lib/lean/Init/Data/ToString/Name.ilean +lib/lean/Init/Data/ToString/Name.ir +lib/lean/Init/Data/ToString/Name.olean +lib/lean/Init/Data/ToString/Name.olean.private +lib/lean/Init/Data/ToString/Name.olean.server lib/lean/Init/Data/UInt.ilean lib/lean/Init/Data/UInt.ir lib/lean/Init/Data/UInt.olean @@ -1577,6 +1812,11 @@ lib/lean/Init/Data/Vector/Range.ir lib/lean/Init/Data/Vector/Range.olean lib/lean/Init/Data/Vector/Range.olean.private lib/lean/Init/Data/Vector/Range.olean.server +lib/lean/Init/Data/Vector/Stream.ilean +lib/lean/Init/Data/Vector/Stream.ir +lib/lean/Init/Data/Vector/Stream.olean +lib/lean/Init/Data/Vector/Stream.olean.private +lib/lean/Init/Data/Vector/Stream.olean.server lib/lean/Init/Data/Vector/Zip.ilean lib/lean/Init/Data/Vector/Zip.ir lib/lean/Init/Data/Vector/Zip.olean @@ -1607,6 +1847,11 @@ lib/lean/Init/Grind.ir lib/lean/Init/Grind.olean lib/lean/Init/Grind.olean.private lib/lean/Init/Grind.olean.server +lib/lean/Init/Grind/AC.ilean +lib/lean/Init/Grind/AC.ir +lib/lean/Init/Grind/AC.olean +lib/lean/Init/Grind/AC.olean.private +lib/lean/Init/Grind/AC.olean.server lib/lean/Init/Grind/Attr.ilean lib/lean/Init/Grind/Attr.ir lib/lean/Init/Grind/Attr.olean @@ -1622,6 +1867,16 @@ lib/lean/Init/Grind/Ext.ir lib/lean/Init/Grind/Ext.olean lib/lean/Init/Grind/Ext.olean.private lib/lean/Init/Grind/Ext.olean.server +lib/lean/Init/Grind/Injective.ilean +lib/lean/Init/Grind/Injective.ir +lib/lean/Init/Grind/Injective.olean +lib/lean/Init/Grind/Injective.olean.private +lib/lean/Init/Grind/Injective.olean.server +lib/lean/Init/Grind/Interactive.ilean +lib/lean/Init/Grind/Interactive.ir +lib/lean/Init/Grind/Interactive.olean +lib/lean/Init/Grind/Interactive.olean.private +lib/lean/Init/Grind/Interactive.olean.server lib/lean/Init/Grind/Lemmas.ilean lib/lean/Init/Grind/Lemmas.ir lib/lean/Init/Grind/Lemmas.olean @@ -1642,6 +1897,16 @@ lib/lean/Init/Grind/Module/Envelope.ir lib/lean/Init/Grind/Module/Envelope.olean lib/lean/Init/Grind/Module/Envelope.olean.private lib/lean/Init/Grind/Module/Envelope.olean.server +lib/lean/Init/Grind/Module/NatModuleNorm.ilean +lib/lean/Init/Grind/Module/NatModuleNorm.ir +lib/lean/Init/Grind/Module/NatModuleNorm.olean +lib/lean/Init/Grind/Module/NatModuleNorm.olean.private +lib/lean/Init/Grind/Module/NatModuleNorm.olean.server +lib/lean/Init/Grind/Module/OfNatModule.ilean +lib/lean/Init/Grind/Module/OfNatModule.ir +lib/lean/Init/Grind/Module/OfNatModule.olean +lib/lean/Init/Grind/Module/OfNatModule.olean.private +lib/lean/Init/Grind/Module/OfNatModule.olean.server lib/lean/Init/Grind/Norm.ilean lib/lean/Init/Grind/Norm.ir lib/lean/Init/Grind/Norm.olean @@ -1652,6 +1917,11 @@ lib/lean/Init/Grind/Offset.ir lib/lean/Init/Grind/Offset.olean lib/lean/Init/Grind/Offset.olean.private lib/lean/Init/Grind/Offset.olean.server +lib/lean/Init/Grind/Order.ilean +lib/lean/Init/Grind/Order.ir +lib/lean/Init/Grind/Order.olean +lib/lean/Init/Grind/Order.olean.private +lib/lean/Init/Grind/Order.olean.server lib/lean/Init/Grind/Ordered.ilean lib/lean/Init/Grind/Ordered.ir lib/lean/Init/Grind/Ordered.olean @@ -1682,6 +1952,11 @@ lib/lean/Init/Grind/Ordered/Order.ir lib/lean/Init/Grind/Ordered/Order.olean lib/lean/Init/Grind/Ordered/Order.olean.private lib/lean/Init/Grind/Ordered/Order.olean.server +lib/lean/Init/Grind/Ordered/Rat.ilean +lib/lean/Init/Grind/Ordered/Rat.ir +lib/lean/Init/Grind/Ordered/Rat.olean +lib/lean/Init/Grind/Ordered/Rat.olean.private +lib/lean/Init/Grind/Ordered/Rat.olean.server lib/lean/Init/Grind/Ordered/Ring.ilean lib/lean/Init/Grind/Ordered/Ring.ir lib/lean/Init/Grind/Ordered/Ring.olean @@ -1707,6 +1982,16 @@ lib/lean/Init/Grind/Ring/Basic.ir lib/lean/Init/Grind/Ring/Basic.olean lib/lean/Init/Grind/Ring/Basic.olean.private lib/lean/Init/Grind/Ring/Basic.olean.server +lib/lean/Init/Grind/Ring/CommSemiringAdapter.ilean +lib/lean/Init/Grind/Ring/CommSemiringAdapter.ir +lib/lean/Init/Grind/Ring/CommSemiringAdapter.olean +lib/lean/Init/Grind/Ring/CommSemiringAdapter.olean.private +lib/lean/Init/Grind/Ring/CommSemiringAdapter.olean.server +lib/lean/Init/Grind/Ring/CommSolver.ilean +lib/lean/Init/Grind/Ring/CommSolver.ir +lib/lean/Init/Grind/Ring/CommSolver.olean +lib/lean/Init/Grind/Ring/CommSolver.olean.private +lib/lean/Init/Grind/Ring/CommSolver.olean.server lib/lean/Init/Grind/Ring/Envelope.ilean lib/lean/Init/Grind/Ring/Envelope.ir lib/lean/Init/Grind/Ring/Envelope.olean @@ -1717,16 +2002,6 @@ lib/lean/Init/Grind/Ring/Field.ir lib/lean/Init/Grind/Ring/Field.olean lib/lean/Init/Grind/Ring/Field.olean.private lib/lean/Init/Grind/Ring/Field.olean.server -lib/lean/Init/Grind/Ring/OfSemiring.ilean -lib/lean/Init/Grind/Ring/OfSemiring.ir -lib/lean/Init/Grind/Ring/OfSemiring.olean -lib/lean/Init/Grind/Ring/OfSemiring.olean.private -lib/lean/Init/Grind/Ring/OfSemiring.olean.server -lib/lean/Init/Grind/Ring/Poly.ilean -lib/lean/Init/Grind/Ring/Poly.ir -lib/lean/Init/Grind/Ring/Poly.olean -lib/lean/Init/Grind/Ring/Poly.olean.private -lib/lean/Init/Grind/Ring/Poly.olean.server lib/lean/Init/Grind/Ring/ToInt.ilean lib/lean/Init/Grind/Ring/ToInt.ir lib/lean/Init/Grind/Ring/ToInt.olean @@ -1787,6 +2062,11 @@ lib/lean/Init/GrindInstances/Ring/Nat.ir lib/lean/Init/GrindInstances/Ring/Nat.olean lib/lean/Init/GrindInstances/Ring/Nat.olean.private lib/lean/Init/GrindInstances/Ring/Nat.olean.server +lib/lean/Init/GrindInstances/Ring/Rat.ilean +lib/lean/Init/GrindInstances/Ring/Rat.ir +lib/lean/Init/GrindInstances/Ring/Rat.olean +lib/lean/Init/GrindInstances/Ring/Rat.olean.private +lib/lean/Init/GrindInstances/Ring/Rat.olean.server lib/lean/Init/GrindInstances/Ring/SInt.ilean lib/lean/Init/GrindInstances/Ring/SInt.ir lib/lean/Init/GrindInstances/Ring/SInt.olean @@ -1837,6 +2117,11 @@ lib/lean/Init/Internal/Order/Tactic.ir lib/lean/Init/Internal/Order/Tactic.olean lib/lean/Init/Internal/Order/Tactic.olean.private lib/lean/Init/Internal/Order/Tactic.olean.server +lib/lean/Init/LawfulBEqTactics.ilean +lib/lean/Init/LawfulBEqTactics.ir +lib/lean/Init/LawfulBEqTactics.olean +lib/lean/Init/LawfulBEqTactics.olean.private +lib/lean/Init/LawfulBEqTactics.olean.server lib/lean/Init/MacroTrace.ilean lib/lean/Init/MacroTrace.ir lib/lean/Init/MacroTrace.olean @@ -1847,11 +2132,21 @@ lib/lean/Init/Meta.ir lib/lean/Init/Meta.olean lib/lean/Init/Meta.olean.private lib/lean/Init/Meta.olean.server +lib/lean/Init/Meta/Defs.ilean +lib/lean/Init/Meta/Defs.ir +lib/lean/Init/Meta/Defs.olean +lib/lean/Init/Meta/Defs.olean.private +lib/lean/Init/Meta/Defs.olean.server lib/lean/Init/MetaTypes.ilean lib/lean/Init/MetaTypes.ir lib/lean/Init/MetaTypes.olean lib/lean/Init/MetaTypes.olean.private lib/lean/Init/MetaTypes.olean.server +lib/lean/Init/MethodSpecsSimp.ilean +lib/lean/Init/MethodSpecsSimp.ir +lib/lean/Init/MethodSpecsSimp.olean +lib/lean/Init/MethodSpecsSimp.olean.private +lib/lean/Init/MethodSpecsSimp.olean.server lib/lean/Init/Notation.ilean lib/lean/Init/Notation.ir lib/lean/Init/Notation.olean @@ -2023,307 +2318,785 @@ lib/lean/Init/While.olean lib/lean/Init/While.olean.private lib/lean/Init/While.olean.server lib/lean/Lake.ilean +lib/lean/Lake.ir lib/lean/Lake.olean +lib/lean/Lake.olean.private +lib/lean/Lake.olean.server lib/lean/Lake/Build.ilean +lib/lean/Lake/Build.ir lib/lean/Lake/Build.olean +lib/lean/Lake/Build.olean.private +lib/lean/Lake/Build.olean.server lib/lean/Lake/Build/Actions.ilean +lib/lean/Lake/Build/Actions.ir lib/lean/Lake/Build/Actions.olean +lib/lean/Lake/Build/Actions.olean.private +lib/lean/Lake/Build/Actions.olean.server lib/lean/Lake/Build/Common.ilean +lib/lean/Lake/Build/Common.ir lib/lean/Lake/Build/Common.olean +lib/lean/Lake/Build/Common.olean.private +lib/lean/Lake/Build/Common.olean.server lib/lean/Lake/Build/Context.ilean +lib/lean/Lake/Build/Context.ir lib/lean/Lake/Build/Context.olean +lib/lean/Lake/Build/Context.olean.private +lib/lean/Lake/Build/Context.olean.server lib/lean/Lake/Build/Data.ilean +lib/lean/Lake/Build/Data.ir lib/lean/Lake/Build/Data.olean +lib/lean/Lake/Build/Data.olean.private +lib/lean/Lake/Build/Data.olean.server lib/lean/Lake/Build/Executable.ilean +lib/lean/Lake/Build/Executable.ir lib/lean/Lake/Build/Executable.olean +lib/lean/Lake/Build/Executable.olean.private +lib/lean/Lake/Build/Executable.olean.server lib/lean/Lake/Build/ExternLib.ilean +lib/lean/Lake/Build/ExternLib.ir lib/lean/Lake/Build/ExternLib.olean +lib/lean/Lake/Build/ExternLib.olean.private +lib/lean/Lake/Build/ExternLib.olean.server lib/lean/Lake/Build/Facets.ilean +lib/lean/Lake/Build/Facets.ir lib/lean/Lake/Build/Facets.olean +lib/lean/Lake/Build/Facets.olean.private +lib/lean/Lake/Build/Facets.olean.server lib/lean/Lake/Build/Fetch.ilean +lib/lean/Lake/Build/Fetch.ir lib/lean/Lake/Build/Fetch.olean +lib/lean/Lake/Build/Fetch.olean.private +lib/lean/Lake/Build/Fetch.olean.server lib/lean/Lake/Build/Index.ilean +lib/lean/Lake/Build/Index.ir lib/lean/Lake/Build/Index.olean +lib/lean/Lake/Build/Index.olean.private +lib/lean/Lake/Build/Index.olean.server lib/lean/Lake/Build/Info.ilean +lib/lean/Lake/Build/Info.ir lib/lean/Lake/Build/Info.olean +lib/lean/Lake/Build/Info.olean.private +lib/lean/Lake/Build/Info.olean.server +lib/lean/Lake/Build/Infos.ilean +lib/lean/Lake/Build/Infos.ir +lib/lean/Lake/Build/Infos.olean +lib/lean/Lake/Build/Infos.olean.private +lib/lean/Lake/Build/Infos.olean.server lib/lean/Lake/Build/InitFacets.ilean +lib/lean/Lake/Build/InitFacets.ir lib/lean/Lake/Build/InitFacets.olean +lib/lean/Lake/Build/InitFacets.olean.private +lib/lean/Lake/Build/InitFacets.olean.server lib/lean/Lake/Build/InputFile.ilean +lib/lean/Lake/Build/InputFile.ir lib/lean/Lake/Build/InputFile.olean +lib/lean/Lake/Build/InputFile.olean.private +lib/lean/Lake/Build/InputFile.olean.server lib/lean/Lake/Build/Job.ilean +lib/lean/Lake/Build/Job.ir lib/lean/Lake/Build/Job.olean +lib/lean/Lake/Build/Job.olean.private +lib/lean/Lake/Build/Job.olean.server lib/lean/Lake/Build/Job/Basic.ilean +lib/lean/Lake/Build/Job/Basic.ir lib/lean/Lake/Build/Job/Basic.olean +lib/lean/Lake/Build/Job/Basic.olean.private +lib/lean/Lake/Build/Job/Basic.olean.server lib/lean/Lake/Build/Job/Monad.ilean +lib/lean/Lake/Build/Job/Monad.ir lib/lean/Lake/Build/Job/Monad.olean +lib/lean/Lake/Build/Job/Monad.olean.private +lib/lean/Lake/Build/Job/Monad.olean.server lib/lean/Lake/Build/Job/Register.ilean +lib/lean/Lake/Build/Job/Register.ir lib/lean/Lake/Build/Job/Register.olean +lib/lean/Lake/Build/Job/Register.olean.private +lib/lean/Lake/Build/Job/Register.olean.server lib/lean/Lake/Build/Key.ilean +lib/lean/Lake/Build/Key.ir lib/lean/Lake/Build/Key.olean +lib/lean/Lake/Build/Key.olean.private +lib/lean/Lake/Build/Key.olean.server lib/lean/Lake/Build/Library.ilean +lib/lean/Lake/Build/Library.ir lib/lean/Lake/Build/Library.olean +lib/lean/Lake/Build/Library.olean.private +lib/lean/Lake/Build/Library.olean.server lib/lean/Lake/Build/Module.ilean +lib/lean/Lake/Build/Module.ir lib/lean/Lake/Build/Module.olean +lib/lean/Lake/Build/Module.olean.private +lib/lean/Lake/Build/Module.olean.server lib/lean/Lake/Build/ModuleArtifacts.ilean +lib/lean/Lake/Build/ModuleArtifacts.ir lib/lean/Lake/Build/ModuleArtifacts.olean +lib/lean/Lake/Build/ModuleArtifacts.olean.private +lib/lean/Lake/Build/ModuleArtifacts.olean.server lib/lean/Lake/Build/Package.ilean +lib/lean/Lake/Build/Package.ir lib/lean/Lake/Build/Package.olean +lib/lean/Lake/Build/Package.olean.private +lib/lean/Lake/Build/Package.olean.server lib/lean/Lake/Build/Run.ilean +lib/lean/Lake/Build/Run.ir lib/lean/Lake/Build/Run.olean +lib/lean/Lake/Build/Run.olean.private +lib/lean/Lake/Build/Run.olean.server lib/lean/Lake/Build/Store.ilean +lib/lean/Lake/Build/Store.ir lib/lean/Lake/Build/Store.olean +lib/lean/Lake/Build/Store.olean.private +lib/lean/Lake/Build/Store.olean.server lib/lean/Lake/Build/Target.ilean +lib/lean/Lake/Build/Target.ir lib/lean/Lake/Build/Target.olean +lib/lean/Lake/Build/Target.olean.private +lib/lean/Lake/Build/Target.olean.server lib/lean/Lake/Build/Target/Basic.ilean +lib/lean/Lake/Build/Target/Basic.ir lib/lean/Lake/Build/Target/Basic.olean +lib/lean/Lake/Build/Target/Basic.olean.private +lib/lean/Lake/Build/Target/Basic.olean.server lib/lean/Lake/Build/Target/Fetch.ilean +lib/lean/Lake/Build/Target/Fetch.ir lib/lean/Lake/Build/Target/Fetch.olean +lib/lean/Lake/Build/Target/Fetch.olean.private +lib/lean/Lake/Build/Target/Fetch.olean.server lib/lean/Lake/Build/Targets.ilean +lib/lean/Lake/Build/Targets.ir lib/lean/Lake/Build/Targets.olean +lib/lean/Lake/Build/Targets.olean.private +lib/lean/Lake/Build/Targets.olean.server lib/lean/Lake/Build/Topological.ilean +lib/lean/Lake/Build/Topological.ir lib/lean/Lake/Build/Topological.olean +lib/lean/Lake/Build/Topological.olean.private +lib/lean/Lake/Build/Topological.olean.server lib/lean/Lake/Build/Trace.ilean +lib/lean/Lake/Build/Trace.ir lib/lean/Lake/Build/Trace.olean +lib/lean/Lake/Build/Trace.olean.private +lib/lean/Lake/Build/Trace.olean.server lib/lean/Lake/CLI.ilean +lib/lean/Lake/CLI.ir lib/lean/Lake/CLI.olean +lib/lean/Lake/CLI.olean.private +lib/lean/Lake/CLI.olean.server lib/lean/Lake/CLI/Actions.ilean +lib/lean/Lake/CLI/Actions.ir lib/lean/Lake/CLI/Actions.olean +lib/lean/Lake/CLI/Actions.olean.private +lib/lean/Lake/CLI/Actions.olean.server lib/lean/Lake/CLI/Build.ilean +lib/lean/Lake/CLI/Build.ir lib/lean/Lake/CLI/Build.olean +lib/lean/Lake/CLI/Build.olean.private +lib/lean/Lake/CLI/Build.olean.server lib/lean/Lake/CLI/Error.ilean +lib/lean/Lake/CLI/Error.ir lib/lean/Lake/CLI/Error.olean +lib/lean/Lake/CLI/Error.olean.private +lib/lean/Lake/CLI/Error.olean.server lib/lean/Lake/CLI/Help.ilean +lib/lean/Lake/CLI/Help.ir lib/lean/Lake/CLI/Help.olean +lib/lean/Lake/CLI/Help.olean.private +lib/lean/Lake/CLI/Help.olean.server lib/lean/Lake/CLI/Init.ilean +lib/lean/Lake/CLI/Init.ir lib/lean/Lake/CLI/Init.olean +lib/lean/Lake/CLI/Init.olean.private +lib/lean/Lake/CLI/Init.olean.server lib/lean/Lake/CLI/Main.ilean +lib/lean/Lake/CLI/Main.ir lib/lean/Lake/CLI/Main.olean +lib/lean/Lake/CLI/Main.olean.private +lib/lean/Lake/CLI/Main.olean.server lib/lean/Lake/CLI/Serve.ilean +lib/lean/Lake/CLI/Serve.ir lib/lean/Lake/CLI/Serve.olean +lib/lean/Lake/CLI/Serve.olean.private +lib/lean/Lake/CLI/Serve.olean.server lib/lean/Lake/CLI/Translate.ilean +lib/lean/Lake/CLI/Translate.ir lib/lean/Lake/CLI/Translate.olean +lib/lean/Lake/CLI/Translate.olean.private +lib/lean/Lake/CLI/Translate.olean.server lib/lean/Lake/CLI/Translate/Lean.ilean +lib/lean/Lake/CLI/Translate/Lean.ir lib/lean/Lake/CLI/Translate/Lean.olean +lib/lean/Lake/CLI/Translate/Lean.olean.private +lib/lean/Lake/CLI/Translate/Lean.olean.server lib/lean/Lake/CLI/Translate/Toml.ilean +lib/lean/Lake/CLI/Translate/Toml.ir lib/lean/Lake/CLI/Translate/Toml.olean +lib/lean/Lake/CLI/Translate/Toml.olean.private +lib/lean/Lake/CLI/Translate/Toml.olean.server lib/lean/Lake/Config.ilean +lib/lean/Lake/Config.ir lib/lean/Lake/Config.olean +lib/lean/Lake/Config.olean.private +lib/lean/Lake/Config.olean.server lib/lean/Lake/Config/Artifact.ilean +lib/lean/Lake/Config/Artifact.ir lib/lean/Lake/Config/Artifact.olean +lib/lean/Lake/Config/Artifact.olean.private +lib/lean/Lake/Config/Artifact.olean.server lib/lean/Lake/Config/Cache.ilean +lib/lean/Lake/Config/Cache.ir lib/lean/Lake/Config/Cache.olean +lib/lean/Lake/Config/Cache.olean.private +lib/lean/Lake/Config/Cache.olean.server lib/lean/Lake/Config/ConfigDecl.ilean +lib/lean/Lake/Config/ConfigDecl.ir lib/lean/Lake/Config/ConfigDecl.olean +lib/lean/Lake/Config/ConfigDecl.olean.private +lib/lean/Lake/Config/ConfigDecl.olean.server lib/lean/Lake/Config/ConfigTarget.ilean +lib/lean/Lake/Config/ConfigTarget.ir lib/lean/Lake/Config/ConfigTarget.olean +lib/lean/Lake/Config/ConfigTarget.olean.private +lib/lean/Lake/Config/ConfigTarget.olean.server lib/lean/Lake/Config/Context.ilean +lib/lean/Lake/Config/Context.ir lib/lean/Lake/Config/Context.olean +lib/lean/Lake/Config/Context.olean.private +lib/lean/Lake/Config/Context.olean.server lib/lean/Lake/Config/Defaults.ilean +lib/lean/Lake/Config/Defaults.ir lib/lean/Lake/Config/Defaults.olean +lib/lean/Lake/Config/Defaults.olean.private +lib/lean/Lake/Config/Defaults.olean.server lib/lean/Lake/Config/Dependency.ilean +lib/lean/Lake/Config/Dependency.ir lib/lean/Lake/Config/Dependency.olean +lib/lean/Lake/Config/Dependency.olean.private +lib/lean/Lake/Config/Dependency.olean.server lib/lean/Lake/Config/Dynlib.ilean +lib/lean/Lake/Config/Dynlib.ir lib/lean/Lake/Config/Dynlib.olean +lib/lean/Lake/Config/Dynlib.olean.private +lib/lean/Lake/Config/Dynlib.olean.server lib/lean/Lake/Config/Env.ilean +lib/lean/Lake/Config/Env.ir lib/lean/Lake/Config/Env.olean +lib/lean/Lake/Config/Env.olean.private +lib/lean/Lake/Config/Env.olean.server lib/lean/Lake/Config/ExternLib.ilean +lib/lean/Lake/Config/ExternLib.ir lib/lean/Lake/Config/ExternLib.olean +lib/lean/Lake/Config/ExternLib.olean.private +lib/lean/Lake/Config/ExternLib.olean.server lib/lean/Lake/Config/ExternLibConfig.ilean +lib/lean/Lake/Config/ExternLibConfig.ir lib/lean/Lake/Config/ExternLibConfig.olean +lib/lean/Lake/Config/ExternLibConfig.olean.private +lib/lean/Lake/Config/ExternLibConfig.olean.server lib/lean/Lake/Config/FacetConfig.ilean +lib/lean/Lake/Config/FacetConfig.ir lib/lean/Lake/Config/FacetConfig.olean +lib/lean/Lake/Config/FacetConfig.olean.private +lib/lean/Lake/Config/FacetConfig.olean.server lib/lean/Lake/Config/Glob.ilean +lib/lean/Lake/Config/Glob.ir lib/lean/Lake/Config/Glob.olean +lib/lean/Lake/Config/Glob.olean.private +lib/lean/Lake/Config/Glob.olean.server lib/lean/Lake/Config/InputFile.ilean +lib/lean/Lake/Config/InputFile.ir lib/lean/Lake/Config/InputFile.olean +lib/lean/Lake/Config/InputFile.olean.private +lib/lean/Lake/Config/InputFile.olean.server lib/lean/Lake/Config/InputFileConfig.ilean +lib/lean/Lake/Config/InputFileConfig.ir lib/lean/Lake/Config/InputFileConfig.olean +lib/lean/Lake/Config/InputFileConfig.olean.private +lib/lean/Lake/Config/InputFileConfig.olean.server lib/lean/Lake/Config/InstallPath.ilean +lib/lean/Lake/Config/InstallPath.ir lib/lean/Lake/Config/InstallPath.olean +lib/lean/Lake/Config/InstallPath.olean.private +lib/lean/Lake/Config/InstallPath.olean.server lib/lean/Lake/Config/Kinds.ilean +lib/lean/Lake/Config/Kinds.ir lib/lean/Lake/Config/Kinds.olean +lib/lean/Lake/Config/Kinds.olean.private +lib/lean/Lake/Config/Kinds.olean.server lib/lean/Lake/Config/Lang.ilean +lib/lean/Lake/Config/Lang.ir lib/lean/Lake/Config/Lang.olean +lib/lean/Lake/Config/Lang.olean.private +lib/lean/Lake/Config/Lang.olean.server lib/lean/Lake/Config/LeanConfig.ilean +lib/lean/Lake/Config/LeanConfig.ir lib/lean/Lake/Config/LeanConfig.olean +lib/lean/Lake/Config/LeanConfig.olean.private +lib/lean/Lake/Config/LeanConfig.olean.server lib/lean/Lake/Config/LeanExe.ilean +lib/lean/Lake/Config/LeanExe.ir lib/lean/Lake/Config/LeanExe.olean +lib/lean/Lake/Config/LeanExe.olean.private +lib/lean/Lake/Config/LeanExe.olean.server lib/lean/Lake/Config/LeanExeConfig.ilean +lib/lean/Lake/Config/LeanExeConfig.ir lib/lean/Lake/Config/LeanExeConfig.olean +lib/lean/Lake/Config/LeanExeConfig.olean.private +lib/lean/Lake/Config/LeanExeConfig.olean.server lib/lean/Lake/Config/LeanLib.ilean +lib/lean/Lake/Config/LeanLib.ir lib/lean/Lake/Config/LeanLib.olean +lib/lean/Lake/Config/LeanLib.olean.private +lib/lean/Lake/Config/LeanLib.olean.server lib/lean/Lake/Config/LeanLibConfig.ilean +lib/lean/Lake/Config/LeanLibConfig.ir lib/lean/Lake/Config/LeanLibConfig.olean +lib/lean/Lake/Config/LeanLibConfig.olean.private +lib/lean/Lake/Config/LeanLibConfig.olean.server lib/lean/Lake/Config/Meta.ilean +lib/lean/Lake/Config/Meta.ir lib/lean/Lake/Config/Meta.olean +lib/lean/Lake/Config/Meta.olean.private +lib/lean/Lake/Config/Meta.olean.server +lib/lean/Lake/Config/MetaClasses.ilean +lib/lean/Lake/Config/MetaClasses.ir +lib/lean/Lake/Config/MetaClasses.olean +lib/lean/Lake/Config/MetaClasses.olean.private +lib/lean/Lake/Config/MetaClasses.olean.server lib/lean/Lake/Config/Module.ilean +lib/lean/Lake/Config/Module.ir lib/lean/Lake/Config/Module.olean +lib/lean/Lake/Config/Module.olean.private +lib/lean/Lake/Config/Module.olean.server lib/lean/Lake/Config/Monad.ilean +lib/lean/Lake/Config/Monad.ir lib/lean/Lake/Config/Monad.olean +lib/lean/Lake/Config/Monad.olean.private +lib/lean/Lake/Config/Monad.olean.server lib/lean/Lake/Config/Opaque.ilean +lib/lean/Lake/Config/Opaque.ir lib/lean/Lake/Config/Opaque.olean +lib/lean/Lake/Config/Opaque.olean.private +lib/lean/Lake/Config/Opaque.olean.server lib/lean/Lake/Config/OutFormat.ilean +lib/lean/Lake/Config/OutFormat.ir lib/lean/Lake/Config/OutFormat.olean +lib/lean/Lake/Config/OutFormat.olean.private +lib/lean/Lake/Config/OutFormat.olean.server lib/lean/Lake/Config/Package.ilean +lib/lean/Lake/Config/Package.ir lib/lean/Lake/Config/Package.olean +lib/lean/Lake/Config/Package.olean.private +lib/lean/Lake/Config/Package.olean.server +lib/lean/Lake/Config/PackageConfig.ilean +lib/lean/Lake/Config/PackageConfig.ir +lib/lean/Lake/Config/PackageConfig.olean +lib/lean/Lake/Config/PackageConfig.olean.private +lib/lean/Lake/Config/PackageConfig.olean.server lib/lean/Lake/Config/Pattern.ilean +lib/lean/Lake/Config/Pattern.ir lib/lean/Lake/Config/Pattern.olean +lib/lean/Lake/Config/Pattern.olean.private +lib/lean/Lake/Config/Pattern.olean.server lib/lean/Lake/Config/Script.ilean +lib/lean/Lake/Config/Script.ir lib/lean/Lake/Config/Script.olean +lib/lean/Lake/Config/Script.olean.private +lib/lean/Lake/Config/Script.olean.server lib/lean/Lake/Config/TargetConfig.ilean +lib/lean/Lake/Config/TargetConfig.ir lib/lean/Lake/Config/TargetConfig.olean +lib/lean/Lake/Config/TargetConfig.olean.private +lib/lean/Lake/Config/TargetConfig.olean.server lib/lean/Lake/Config/Workspace.ilean +lib/lean/Lake/Config/Workspace.ir lib/lean/Lake/Config/Workspace.olean +lib/lean/Lake/Config/Workspace.olean.private +lib/lean/Lake/Config/Workspace.olean.server lib/lean/Lake/Config/WorkspaceConfig.ilean +lib/lean/Lake/Config/WorkspaceConfig.ir lib/lean/Lake/Config/WorkspaceConfig.olean +lib/lean/Lake/Config/WorkspaceConfig.olean.private +lib/lean/Lake/Config/WorkspaceConfig.olean.server lib/lean/Lake/DSL.ilean +lib/lean/Lake/DSL.ir lib/lean/Lake/DSL.olean +lib/lean/Lake/DSL.olean.private +lib/lean/Lake/DSL.olean.server lib/lean/Lake/DSL/Attributes.ilean +lib/lean/Lake/DSL/Attributes.ir lib/lean/Lake/DSL/Attributes.olean +lib/lean/Lake/DSL/Attributes.olean.private +lib/lean/Lake/DSL/Attributes.olean.server lib/lean/Lake/DSL/AttributesCore.ilean +lib/lean/Lake/DSL/AttributesCore.ir lib/lean/Lake/DSL/AttributesCore.olean +lib/lean/Lake/DSL/AttributesCore.olean.private +lib/lean/Lake/DSL/AttributesCore.olean.server lib/lean/Lake/DSL/Config.ilean +lib/lean/Lake/DSL/Config.ir lib/lean/Lake/DSL/Config.olean +lib/lean/Lake/DSL/Config.olean.private +lib/lean/Lake/DSL/Config.olean.server lib/lean/Lake/DSL/DeclUtil.ilean +lib/lean/Lake/DSL/DeclUtil.ir lib/lean/Lake/DSL/DeclUtil.olean +lib/lean/Lake/DSL/DeclUtil.olean.private +lib/lean/Lake/DSL/DeclUtil.olean.server lib/lean/Lake/DSL/Extensions.ilean +lib/lean/Lake/DSL/Extensions.ir lib/lean/Lake/DSL/Extensions.olean +lib/lean/Lake/DSL/Extensions.olean.private +lib/lean/Lake/DSL/Extensions.olean.server lib/lean/Lake/DSL/Key.ilean +lib/lean/Lake/DSL/Key.ir lib/lean/Lake/DSL/Key.olean +lib/lean/Lake/DSL/Key.olean.private +lib/lean/Lake/DSL/Key.olean.server lib/lean/Lake/DSL/Meta.ilean +lib/lean/Lake/DSL/Meta.ir lib/lean/Lake/DSL/Meta.olean +lib/lean/Lake/DSL/Meta.olean.private +lib/lean/Lake/DSL/Meta.olean.server lib/lean/Lake/DSL/Package.ilean +lib/lean/Lake/DSL/Package.ir lib/lean/Lake/DSL/Package.olean +lib/lean/Lake/DSL/Package.olean.private +lib/lean/Lake/DSL/Package.olean.server lib/lean/Lake/DSL/Require.ilean +lib/lean/Lake/DSL/Require.ir lib/lean/Lake/DSL/Require.olean +lib/lean/Lake/DSL/Require.olean.private +lib/lean/Lake/DSL/Require.olean.server lib/lean/Lake/DSL/Script.ilean +lib/lean/Lake/DSL/Script.ir lib/lean/Lake/DSL/Script.olean +lib/lean/Lake/DSL/Script.olean.private +lib/lean/Lake/DSL/Script.olean.server lib/lean/Lake/DSL/Syntax.ilean +lib/lean/Lake/DSL/Syntax.ir lib/lean/Lake/DSL/Syntax.olean +lib/lean/Lake/DSL/Syntax.olean.private +lib/lean/Lake/DSL/Syntax.olean.server lib/lean/Lake/DSL/Targets.ilean +lib/lean/Lake/DSL/Targets.ir lib/lean/Lake/DSL/Targets.olean +lib/lean/Lake/DSL/Targets.olean.private +lib/lean/Lake/DSL/Targets.olean.server lib/lean/Lake/DSL/VerLit.ilean +lib/lean/Lake/DSL/VerLit.ir lib/lean/Lake/DSL/VerLit.olean +lib/lean/Lake/DSL/VerLit.olean.private +lib/lean/Lake/DSL/VerLit.olean.server lib/lean/Lake/Load.ilean +lib/lean/Lake/Load.ir lib/lean/Lake/Load.olean +lib/lean/Lake/Load.olean.private +lib/lean/Lake/Load.olean.server lib/lean/Lake/Load/Config.ilean +lib/lean/Lake/Load/Config.ir lib/lean/Lake/Load/Config.olean +lib/lean/Lake/Load/Config.olean.private +lib/lean/Lake/Load/Config.olean.server lib/lean/Lake/Load/Lean.ilean +lib/lean/Lake/Load/Lean.ir lib/lean/Lake/Load/Lean.olean +lib/lean/Lake/Load/Lean.olean.private +lib/lean/Lake/Load/Lean.olean.server lib/lean/Lake/Load/Lean/Elab.ilean +lib/lean/Lake/Load/Lean/Elab.ir lib/lean/Lake/Load/Lean/Elab.olean +lib/lean/Lake/Load/Lean/Elab.olean.private +lib/lean/Lake/Load/Lean/Elab.olean.server lib/lean/Lake/Load/Lean/Eval.ilean +lib/lean/Lake/Load/Lean/Eval.ir lib/lean/Lake/Load/Lean/Eval.olean +lib/lean/Lake/Load/Lean/Eval.olean.private +lib/lean/Lake/Load/Lean/Eval.olean.server lib/lean/Lake/Load/Manifest.ilean +lib/lean/Lake/Load/Manifest.ir lib/lean/Lake/Load/Manifest.olean +lib/lean/Lake/Load/Manifest.olean.private +lib/lean/Lake/Load/Manifest.olean.server lib/lean/Lake/Load/Materialize.ilean +lib/lean/Lake/Load/Materialize.ir lib/lean/Lake/Load/Materialize.olean +lib/lean/Lake/Load/Materialize.olean.private +lib/lean/Lake/Load/Materialize.olean.server lib/lean/Lake/Load/Package.ilean +lib/lean/Lake/Load/Package.ir lib/lean/Lake/Load/Package.olean +lib/lean/Lake/Load/Package.olean.private +lib/lean/Lake/Load/Package.olean.server lib/lean/Lake/Load/Resolve.ilean +lib/lean/Lake/Load/Resolve.ir lib/lean/Lake/Load/Resolve.olean +lib/lean/Lake/Load/Resolve.olean.private +lib/lean/Lake/Load/Resolve.olean.server lib/lean/Lake/Load/Toml.ilean +lib/lean/Lake/Load/Toml.ir lib/lean/Lake/Load/Toml.olean +lib/lean/Lake/Load/Toml.olean.private +lib/lean/Lake/Load/Toml.olean.server lib/lean/Lake/Load/Workspace.ilean +lib/lean/Lake/Load/Workspace.ir lib/lean/Lake/Load/Workspace.olean +lib/lean/Lake/Load/Workspace.olean.private +lib/lean/Lake/Load/Workspace.olean.server lib/lean/Lake/Reservoir.ilean +lib/lean/Lake/Reservoir.ir lib/lean/Lake/Reservoir.olean +lib/lean/Lake/Reservoir.olean.private +lib/lean/Lake/Reservoir.olean.server lib/lean/Lake/Toml.ilean +lib/lean/Lake/Toml.ir lib/lean/Lake/Toml.olean +lib/lean/Lake/Toml.olean.private +lib/lean/Lake/Toml.olean.server lib/lean/Lake/Toml/Data.ilean +lib/lean/Lake/Toml/Data.ir lib/lean/Lake/Toml/Data.olean +lib/lean/Lake/Toml/Data.olean.private +lib/lean/Lake/Toml/Data.olean.server lib/lean/Lake/Toml/Data/DateTime.ilean +lib/lean/Lake/Toml/Data/DateTime.ir lib/lean/Lake/Toml/Data/DateTime.olean +lib/lean/Lake/Toml/Data/DateTime.olean.private +lib/lean/Lake/Toml/Data/DateTime.olean.server lib/lean/Lake/Toml/Data/Dict.ilean +lib/lean/Lake/Toml/Data/Dict.ir lib/lean/Lake/Toml/Data/Dict.olean +lib/lean/Lake/Toml/Data/Dict.olean.private +lib/lean/Lake/Toml/Data/Dict.olean.server lib/lean/Lake/Toml/Data/Value.ilean +lib/lean/Lake/Toml/Data/Value.ir lib/lean/Lake/Toml/Data/Value.olean +lib/lean/Lake/Toml/Data/Value.olean.private +lib/lean/Lake/Toml/Data/Value.olean.server lib/lean/Lake/Toml/Decode.ilean +lib/lean/Lake/Toml/Decode.ir lib/lean/Lake/Toml/Decode.olean +lib/lean/Lake/Toml/Decode.olean.private +lib/lean/Lake/Toml/Decode.olean.server lib/lean/Lake/Toml/Elab.ilean +lib/lean/Lake/Toml/Elab.ir lib/lean/Lake/Toml/Elab.olean +lib/lean/Lake/Toml/Elab.olean.private +lib/lean/Lake/Toml/Elab.olean.server lib/lean/Lake/Toml/Elab/Expression.ilean +lib/lean/Lake/Toml/Elab/Expression.ir lib/lean/Lake/Toml/Elab/Expression.olean +lib/lean/Lake/Toml/Elab/Expression.olean.private +lib/lean/Lake/Toml/Elab/Expression.olean.server lib/lean/Lake/Toml/Elab/Value.ilean +lib/lean/Lake/Toml/Elab/Value.ir lib/lean/Lake/Toml/Elab/Value.olean +lib/lean/Lake/Toml/Elab/Value.olean.private +lib/lean/Lake/Toml/Elab/Value.olean.server lib/lean/Lake/Toml/Encode.ilean +lib/lean/Lake/Toml/Encode.ir lib/lean/Lake/Toml/Encode.olean +lib/lean/Lake/Toml/Encode.olean.private +lib/lean/Lake/Toml/Encode.olean.server lib/lean/Lake/Toml/Grammar.ilean +lib/lean/Lake/Toml/Grammar.ir lib/lean/Lake/Toml/Grammar.olean +lib/lean/Lake/Toml/Grammar.olean.private +lib/lean/Lake/Toml/Grammar.olean.server lib/lean/Lake/Toml/Load.ilean +lib/lean/Lake/Toml/Load.ir lib/lean/Lake/Toml/Load.olean +lib/lean/Lake/Toml/Load.olean.private +lib/lean/Lake/Toml/Load.olean.server lib/lean/Lake/Toml/ParserUtil.ilean +lib/lean/Lake/Toml/ParserUtil.ir lib/lean/Lake/Toml/ParserUtil.olean +lib/lean/Lake/Toml/ParserUtil.olean.private +lib/lean/Lake/Toml/ParserUtil.olean.server +lib/lean/Lake/Util.ilean +lib/lean/Lake/Util.ir +lib/lean/Lake/Util.olean +lib/lean/Lake/Util.olean.private +lib/lean/Lake/Util.olean.server lib/lean/Lake/Util/Binder.ilean +lib/lean/Lake/Util/Binder.ir lib/lean/Lake/Util/Binder.olean +lib/lean/Lake/Util/Binder.olean.private +lib/lean/Lake/Util/Binder.olean.server lib/lean/Lake/Util/Casing.ilean +lib/lean/Lake/Util/Casing.ir lib/lean/Lake/Util/Casing.olean +lib/lean/Lake/Util/Casing.olean.private +lib/lean/Lake/Util/Casing.olean.server lib/lean/Lake/Util/Cli.ilean +lib/lean/Lake/Util/Cli.ir lib/lean/Lake/Util/Cli.olean +lib/lean/Lake/Util/Cli.olean.private +lib/lean/Lake/Util/Cli.olean.server lib/lean/Lake/Util/Cycle.ilean +lib/lean/Lake/Util/Cycle.ir lib/lean/Lake/Util/Cycle.olean +lib/lean/Lake/Util/Cycle.olean.private +lib/lean/Lake/Util/Cycle.olean.server lib/lean/Lake/Util/Date.ilean +lib/lean/Lake/Util/Date.ir lib/lean/Lake/Util/Date.olean +lib/lean/Lake/Util/Date.olean.private +lib/lean/Lake/Util/Date.olean.server lib/lean/Lake/Util/EStateT.ilean +lib/lean/Lake/Util/EStateT.ir lib/lean/Lake/Util/EStateT.olean +lib/lean/Lake/Util/EStateT.olean.private +lib/lean/Lake/Util/EStateT.olean.server lib/lean/Lake/Util/EquipT.ilean +lib/lean/Lake/Util/EquipT.ir lib/lean/Lake/Util/EquipT.olean +lib/lean/Lake/Util/EquipT.olean.private +lib/lean/Lake/Util/EquipT.olean.server lib/lean/Lake/Util/Error.ilean +lib/lean/Lake/Util/Error.ir lib/lean/Lake/Util/Error.olean +lib/lean/Lake/Util/Error.olean.private +lib/lean/Lake/Util/Error.olean.server lib/lean/Lake/Util/Exit.ilean +lib/lean/Lake/Util/Exit.ir lib/lean/Lake/Util/Exit.olean +lib/lean/Lake/Util/Exit.olean.private +lib/lean/Lake/Util/Exit.olean.server lib/lean/Lake/Util/Family.ilean +lib/lean/Lake/Util/Family.ir lib/lean/Lake/Util/Family.olean +lib/lean/Lake/Util/Family.olean.private +lib/lean/Lake/Util/Family.olean.server lib/lean/Lake/Util/FilePath.ilean +lib/lean/Lake/Util/FilePath.ir lib/lean/Lake/Util/FilePath.olean +lib/lean/Lake/Util/FilePath.olean.private +lib/lean/Lake/Util/FilePath.olean.server lib/lean/Lake/Util/Git.ilean +lib/lean/Lake/Util/Git.ir lib/lean/Lake/Util/Git.olean +lib/lean/Lake/Util/Git.olean.private +lib/lean/Lake/Util/Git.olean.server lib/lean/Lake/Util/IO.ilean +lib/lean/Lake/Util/IO.ir lib/lean/Lake/Util/IO.olean +lib/lean/Lake/Util/IO.olean.private +lib/lean/Lake/Util/IO.olean.server lib/lean/Lake/Util/JsonObject.ilean +lib/lean/Lake/Util/JsonObject.ir lib/lean/Lake/Util/JsonObject.olean +lib/lean/Lake/Util/JsonObject.olean.private +lib/lean/Lake/Util/JsonObject.olean.server lib/lean/Lake/Util/Lift.ilean +lib/lean/Lake/Util/Lift.ir lib/lean/Lake/Util/Lift.olean -lib/lean/Lake/Util/List.ilean -lib/lean/Lake/Util/List.olean +lib/lean/Lake/Util/Lift.olean.private +lib/lean/Lake/Util/Lift.olean.server lib/lean/Lake/Util/Lock.ilean +lib/lean/Lake/Util/Lock.ir lib/lean/Lake/Util/Lock.olean +lib/lean/Lake/Util/Lock.olean.private +lib/lean/Lake/Util/Lock.olean.server lib/lean/Lake/Util/Log.ilean +lib/lean/Lake/Util/Log.ir lib/lean/Lake/Util/Log.olean +lib/lean/Lake/Util/Log.olean.private +lib/lean/Lake/Util/Log.olean.server lib/lean/Lake/Util/MainM.ilean +lib/lean/Lake/Util/MainM.ir lib/lean/Lake/Util/MainM.olean +lib/lean/Lake/Util/MainM.olean.private +lib/lean/Lake/Util/MainM.olean.server lib/lean/Lake/Util/Message.ilean +lib/lean/Lake/Util/Message.ir lib/lean/Lake/Util/Message.olean +lib/lean/Lake/Util/Message.olean.private +lib/lean/Lake/Util/Message.olean.server lib/lean/Lake/Util/Name.ilean +lib/lean/Lake/Util/Name.ir lib/lean/Lake/Util/Name.olean +lib/lean/Lake/Util/Name.olean.private +lib/lean/Lake/Util/Name.olean.server lib/lean/Lake/Util/NativeLib.ilean +lib/lean/Lake/Util/NativeLib.ir lib/lean/Lake/Util/NativeLib.olean +lib/lean/Lake/Util/NativeLib.olean.private +lib/lean/Lake/Util/NativeLib.olean.server lib/lean/Lake/Util/Opaque.ilean +lib/lean/Lake/Util/Opaque.ir lib/lean/Lake/Util/Opaque.olean +lib/lean/Lake/Util/Opaque.olean.private +lib/lean/Lake/Util/Opaque.olean.server lib/lean/Lake/Util/OpaqueType.ilean +lib/lean/Lake/Util/OpaqueType.ir lib/lean/Lake/Util/OpaqueType.olean +lib/lean/Lake/Util/OpaqueType.olean.private +lib/lean/Lake/Util/OpaqueType.olean.server lib/lean/Lake/Util/OrdHashSet.ilean +lib/lean/Lake/Util/OrdHashSet.ir lib/lean/Lake/Util/OrdHashSet.olean +lib/lean/Lake/Util/OrdHashSet.olean.private +lib/lean/Lake/Util/OrdHashSet.olean.server lib/lean/Lake/Util/OrderedTagAttribute.ilean +lib/lean/Lake/Util/OrderedTagAttribute.ir lib/lean/Lake/Util/OrderedTagAttribute.olean +lib/lean/Lake/Util/OrderedTagAttribute.olean.private +lib/lean/Lake/Util/OrderedTagAttribute.olean.server lib/lean/Lake/Util/Proc.ilean +lib/lean/Lake/Util/Proc.ir lib/lean/Lake/Util/Proc.olean +lib/lean/Lake/Util/Proc.olean.private +lib/lean/Lake/Util/Proc.olean.server lib/lean/Lake/Util/RBArray.ilean +lib/lean/Lake/Util/RBArray.ir lib/lean/Lake/Util/RBArray.olean +lib/lean/Lake/Util/RBArray.olean.private +lib/lean/Lake/Util/RBArray.olean.server +lib/lean/Lake/Util/Reservoir.ilean +lib/lean/Lake/Util/Reservoir.ir +lib/lean/Lake/Util/Reservoir.olean +lib/lean/Lake/Util/Reservoir.olean.private +lib/lean/Lake/Util/Reservoir.olean.server lib/lean/Lake/Util/Store.ilean +lib/lean/Lake/Util/Store.ir lib/lean/Lake/Util/Store.olean +lib/lean/Lake/Util/Store.olean.private +lib/lean/Lake/Util/Store.olean.server lib/lean/Lake/Util/StoreInsts.ilean +lib/lean/Lake/Util/StoreInsts.ir lib/lean/Lake/Util/StoreInsts.olean -lib/lean/Lake/Util/Sugar.ilean -lib/lean/Lake/Util/Sugar.olean +lib/lean/Lake/Util/StoreInsts.olean.private +lib/lean/Lake/Util/StoreInsts.olean.server +lib/lean/Lake/Util/String.ilean +lib/lean/Lake/Util/String.ir +lib/lean/Lake/Util/String.olean +lib/lean/Lake/Util/String.olean.private +lib/lean/Lake/Util/String.olean.server lib/lean/Lake/Util/Task.ilean +lib/lean/Lake/Util/Task.ir lib/lean/Lake/Util/Task.olean +lib/lean/Lake/Util/Task.olean.private +lib/lean/Lake/Util/Task.olean.server +lib/lean/Lake/Util/Url.ilean +lib/lean/Lake/Util/Url.ir +lib/lean/Lake/Util/Url.olean +lib/lean/Lake/Util/Url.olean.private +lib/lean/Lake/Util/Url.olean.server lib/lean/Lake/Util/Version.ilean +lib/lean/Lake/Util/Version.ir lib/lean/Lake/Util/Version.olean +lib/lean/Lake/Util/Version.olean.private +lib/lean/Lake/Util/Version.olean.server lib/lean/Lake/Version.ilean +lib/lean/Lake/Version.ir lib/lean/Lake/Version.olean +lib/lean/Lake/Version.olean.private +lib/lean/Lake/Version.olean.server lib/lean/LakeMain.ilean +lib/lean/LakeMain.ir lib/lean/LakeMain.olean +lib/lean/LakeMain.olean.private +lib/lean/LakeMain.olean.server lib/lean/Lean.ilean lib/lean/Lean.ir lib/lean/Lean.olean @@ -2934,6 +3707,11 @@ lib/lean/Lean/Data/DeclarationRange.ir lib/lean/Lean/Data/DeclarationRange.olean lib/lean/Lean/Data/DeclarationRange.olean.private lib/lean/Lean/Data/DeclarationRange.olean.server +lib/lean/Lean/Data/EditDistance.ilean +lib/lean/Lean/Data/EditDistance.ir +lib/lean/Lean/Data/EditDistance.olean +lib/lean/Lean/Data/EditDistance.olean.private +lib/lean/Lean/Data/EditDistance.olean.server lib/lean/Lean/Data/Format.ilean lib/lean/Lean/Data/Format.ir lib/lean/Lean/Data/Format.olean @@ -3234,11 +4012,36 @@ lib/lean/Lean/DocString/Extension.ir lib/lean/Lean/DocString/Extension.olean lib/lean/Lean/DocString/Extension.olean.private lib/lean/Lean/DocString/Extension.olean.server +lib/lean/Lean/DocString/Formatter.ilean +lib/lean/Lean/DocString/Formatter.ir +lib/lean/Lean/DocString/Formatter.olean +lib/lean/Lean/DocString/Formatter.olean.private +lib/lean/Lean/DocString/Formatter.olean.server lib/lean/Lean/DocString/Links.ilean lib/lean/Lean/DocString/Links.ir lib/lean/Lean/DocString/Links.olean lib/lean/Lean/DocString/Links.olean.private lib/lean/Lean/DocString/Links.olean.server +lib/lean/Lean/DocString/Markdown.ilean +lib/lean/Lean/DocString/Markdown.ir +lib/lean/Lean/DocString/Markdown.olean +lib/lean/Lean/DocString/Markdown.olean.private +lib/lean/Lean/DocString/Markdown.olean.server +lib/lean/Lean/DocString/Parser.ilean +lib/lean/Lean/DocString/Parser.ir +lib/lean/Lean/DocString/Parser.olean +lib/lean/Lean/DocString/Parser.olean.private +lib/lean/Lean/DocString/Parser.olean.server +lib/lean/Lean/DocString/Syntax.ilean +lib/lean/Lean/DocString/Syntax.ir +lib/lean/Lean/DocString/Syntax.olean +lib/lean/Lean/DocString/Syntax.olean.private +lib/lean/Lean/DocString/Syntax.olean.server +lib/lean/Lean/DocString/Types.ilean +lib/lean/Lean/DocString/Types.ir +lib/lean/Lean/DocString/Types.olean +lib/lean/Lean/DocString/Types.olean.private +lib/lean/Lean/DocString/Types.olean.server lib/lean/Lean/Elab.ilean lib/lean/Lean/Elab.ir lib/lean/Lean/Elab.olean @@ -3314,11 +4117,21 @@ lib/lean/Lean/Elab/CheckTactic.ir lib/lean/Lean/Elab/CheckTactic.olean lib/lean/Lean/Elab/CheckTactic.olean.private lib/lean/Lean/Elab/CheckTactic.olean.server +lib/lean/Lean/Elab/Coinductive.ilean +lib/lean/Lean/Elab/Coinductive.ir +lib/lean/Lean/Elab/Coinductive.olean +lib/lean/Lean/Elab/Coinductive.olean.private +lib/lean/Lean/Elab/Coinductive.olean.server lib/lean/Lean/Elab/Command.ilean lib/lean/Lean/Elab/Command.ir lib/lean/Lean/Elab/Command.olean lib/lean/Lean/Elab/Command.olean.private lib/lean/Lean/Elab/Command.olean.server +lib/lean/Lean/Elab/Command/Scope.ilean +lib/lean/Lean/Elab/Command/Scope.ir +lib/lean/Lean/Elab/Command/Scope.olean +lib/lean/Lean/Elab/Command/Scope.olean.private +lib/lean/Lean/Elab/Command/Scope.olean.server lib/lean/Lean/Elab/ComputedFields.ilean lib/lean/Lean/Elab/ComputedFields.ir lib/lean/Lean/Elab/ComputedFields.olean @@ -3394,6 +4207,11 @@ lib/lean/Lean/Elab/Deriving/Inhabited.ir lib/lean/Lean/Elab/Deriving/Inhabited.olean lib/lean/Lean/Elab/Deriving/Inhabited.olean.private lib/lean/Lean/Elab/Deriving/Inhabited.olean.server +lib/lean/Lean/Elab/Deriving/LawfulBEq.ilean +lib/lean/Lean/Elab/Deriving/LawfulBEq.ir +lib/lean/Lean/Elab/Deriving/LawfulBEq.olean +lib/lean/Lean/Elab/Deriving/LawfulBEq.olean.private +lib/lean/Lean/Elab/Deriving/LawfulBEq.olean.server lib/lean/Lean/Elab/Deriving/Nonempty.ilean lib/lean/Lean/Elab/Deriving/Nonempty.ir lib/lean/Lean/Elab/Deriving/Nonempty.olean @@ -3404,6 +4222,11 @@ lib/lean/Lean/Elab/Deriving/Ord.ir lib/lean/Lean/Elab/Deriving/Ord.olean lib/lean/Lean/Elab/Deriving/Ord.olean.private lib/lean/Lean/Elab/Deriving/Ord.olean.server +lib/lean/Lean/Elab/Deriving/ReflBEq.ilean +lib/lean/Lean/Elab/Deriving/ReflBEq.ir +lib/lean/Lean/Elab/Deriving/ReflBEq.olean +lib/lean/Lean/Elab/Deriving/ReflBEq.olean.private +lib/lean/Lean/Elab/Deriving/ReflBEq.olean.server lib/lean/Lean/Elab/Deriving/Repr.ilean lib/lean/Lean/Elab/Deriving/Repr.ir lib/lean/Lean/Elab/Deriving/Repr.olean @@ -3434,6 +4257,36 @@ lib/lean/Lean/Elab/Do.ir lib/lean/Lean/Elab/Do.olean lib/lean/Lean/Elab/Do.olean.private lib/lean/Lean/Elab/Do.olean.server +lib/lean/Lean/Elab/DocString.ilean +lib/lean/Lean/Elab/DocString.ir +lib/lean/Lean/Elab/DocString.olean +lib/lean/Lean/Elab/DocString.olean.private +lib/lean/Lean/Elab/DocString.olean.server +lib/lean/Lean/Elab/DocString/Builtin.ilean +lib/lean/Lean/Elab/DocString/Builtin.ir +lib/lean/Lean/Elab/DocString/Builtin.olean +lib/lean/Lean/Elab/DocString/Builtin.olean.private +lib/lean/Lean/Elab/DocString/Builtin.olean.server +lib/lean/Lean/Elab/DocString/Builtin/Keywords.ilean +lib/lean/Lean/Elab/DocString/Builtin/Keywords.ir +lib/lean/Lean/Elab/DocString/Builtin/Keywords.olean +lib/lean/Lean/Elab/DocString/Builtin/Keywords.olean.private +lib/lean/Lean/Elab/DocString/Builtin/Keywords.olean.server +lib/lean/Lean/Elab/DocString/Builtin/Parsing.ilean +lib/lean/Lean/Elab/DocString/Builtin/Parsing.ir +lib/lean/Lean/Elab/DocString/Builtin/Parsing.olean +lib/lean/Lean/Elab/DocString/Builtin/Parsing.olean.private +lib/lean/Lean/Elab/DocString/Builtin/Parsing.olean.server +lib/lean/Lean/Elab/DocString/Builtin/Postponed.ilean +lib/lean/Lean/Elab/DocString/Builtin/Postponed.ir +lib/lean/Lean/Elab/DocString/Builtin/Postponed.olean +lib/lean/Lean/Elab/DocString/Builtin/Postponed.olean.private +lib/lean/Lean/Elab/DocString/Builtin/Postponed.olean.server +lib/lean/Lean/Elab/DocString/Builtin/Scopes.ilean +lib/lean/Lean/Elab/DocString/Builtin/Scopes.ir +lib/lean/Lean/Elab/DocString/Builtin/Scopes.olean +lib/lean/Lean/Elab/DocString/Builtin/Scopes.olean.private +lib/lean/Lean/Elab/DocString/Builtin/Scopes.olean.server lib/lean/Lean/Elab/ElabRules.ilean lib/lean/Lean/Elab/ElabRules.ir lib/lean/Lean/Elab/ElabRules.olean @@ -3609,6 +4462,11 @@ lib/lean/Lean/Elab/PreDefinition/Eqns.ir lib/lean/Lean/Elab/PreDefinition/Eqns.olean lib/lean/Lean/Elab/PreDefinition/Eqns.olean.private lib/lean/Lean/Elab/PreDefinition/Eqns.olean.server +lib/lean/Lean/Elab/PreDefinition/EqnsUtils.ilean +lib/lean/Lean/Elab/PreDefinition/EqnsUtils.ir +lib/lean/Lean/Elab/PreDefinition/EqnsUtils.olean +lib/lean/Lean/Elab/PreDefinition/EqnsUtils.olean.private +lib/lean/Lean/Elab/PreDefinition/EqnsUtils.olean.server lib/lean/Lean/Elab/PreDefinition/FixedParams.ilean lib/lean/Lean/Elab/PreDefinition/FixedParams.ir lib/lean/Lean/Elab/PreDefinition/FixedParams.olean @@ -3629,11 +4487,6 @@ lib/lean/Lean/Elab/PreDefinition/Mutual.ir lib/lean/Lean/Elab/PreDefinition/Mutual.olean lib/lean/Lean/Elab/PreDefinition/Mutual.olean.private lib/lean/Lean/Elab/PreDefinition/Mutual.olean.server -lib/lean/Lean/Elab/PreDefinition/Nonrec/Eqns.ilean -lib/lean/Lean/Elab/PreDefinition/Nonrec/Eqns.ir -lib/lean/Lean/Elab/PreDefinition/Nonrec/Eqns.olean -lib/lean/Lean/Elab/PreDefinition/Nonrec/Eqns.olean.private -lib/lean/Lean/Elab/PreDefinition/Nonrec/Eqns.olean.server lib/lean/Lean/Elab/PreDefinition/PartialFixpoint.ilean lib/lean/Lean/Elab/PreDefinition/PartialFixpoint.ir lib/lean/Lean/Elab/PreDefinition/PartialFixpoint.olean @@ -4234,6 +5087,11 @@ lib/lean/Lean/Elab/Tactic/Do/VCGen/Split.ir lib/lean/Lean/Elab/Tactic/Do/VCGen/Split.olean lib/lean/Lean/Elab/Tactic/Do/VCGen/Split.olean.private lib/lean/Lean/Elab/Tactic/Do/VCGen/Split.olean.server +lib/lean/Lean/Elab/Tactic/Do/VCGen/SuggestInvariant.ilean +lib/lean/Lean/Elab/Tactic/Do/VCGen/SuggestInvariant.ir +lib/lean/Lean/Elab/Tactic/Do/VCGen/SuggestInvariant.olean +lib/lean/Lean/Elab/Tactic/Do/VCGen/SuggestInvariant.olean.private +lib/lean/Lean/Elab/Tactic/Do/VCGen/SuggestInvariant.olean.server lib/lean/Lean/Elab/Tactic/Doc.ilean lib/lean/Lean/Elab/Tactic/Doc.ir lib/lean/Lean/Elab/Tactic/Doc.olean @@ -4269,6 +5127,41 @@ lib/lean/Lean/Elab/Tactic/Grind.ir lib/lean/Lean/Elab/Tactic/Grind.olean lib/lean/Lean/Elab/Tactic/Grind.olean.private lib/lean/Lean/Elab/Tactic/Grind.olean.server +lib/lean/Lean/Elab/Tactic/Grind/Basic.ilean +lib/lean/Lean/Elab/Tactic/Grind/Basic.ir +lib/lean/Lean/Elab/Tactic/Grind/Basic.olean +lib/lean/Lean/Elab/Tactic/Grind/Basic.olean.private +lib/lean/Lean/Elab/Tactic/Grind/Basic.olean.server +lib/lean/Lean/Elab/Tactic/Grind/BuiltinTactic.ilean +lib/lean/Lean/Elab/Tactic/Grind/BuiltinTactic.ir +lib/lean/Lean/Elab/Tactic/Grind/BuiltinTactic.olean +lib/lean/Lean/Elab/Tactic/Grind/BuiltinTactic.olean.private +lib/lean/Lean/Elab/Tactic/Grind/BuiltinTactic.olean.server +lib/lean/Lean/Elab/Tactic/Grind/Filter.ilean +lib/lean/Lean/Elab/Tactic/Grind/Filter.ir +lib/lean/Lean/Elab/Tactic/Grind/Filter.olean +lib/lean/Lean/Elab/Tactic/Grind/Filter.olean.private +lib/lean/Lean/Elab/Tactic/Grind/Filter.olean.server +lib/lean/Lean/Elab/Tactic/Grind/Have.ilean +lib/lean/Lean/Elab/Tactic/Grind/Have.ir +lib/lean/Lean/Elab/Tactic/Grind/Have.olean +lib/lean/Lean/Elab/Tactic/Grind/Have.olean.private +lib/lean/Lean/Elab/Tactic/Grind/Have.olean.server +lib/lean/Lean/Elab/Tactic/Grind/Main.ilean +lib/lean/Lean/Elab/Tactic/Grind/Main.ir +lib/lean/Lean/Elab/Tactic/Grind/Main.olean +lib/lean/Lean/Elab/Tactic/Grind/Main.olean.private +lib/lean/Lean/Elab/Tactic/Grind/Main.olean.server +lib/lean/Lean/Elab/Tactic/Grind/ShowState.ilean +lib/lean/Lean/Elab/Tactic/Grind/ShowState.ir +lib/lean/Lean/Elab/Tactic/Grind/ShowState.olean +lib/lean/Lean/Elab/Tactic/Grind/ShowState.olean.private +lib/lean/Lean/Elab/Tactic/Grind/ShowState.olean.server +lib/lean/Lean/Elab/Tactic/Grind/Trace.ilean +lib/lean/Lean/Elab/Tactic/Grind/Trace.ir +lib/lean/Lean/Elab/Tactic/Grind/Trace.olean +lib/lean/Lean/Elab/Tactic/Grind/Trace.olean.private +lib/lean/Lean/Elab/Tactic/Grind/Trace.olean.server lib/lean/Lean/Elab/Tactic/Guard.ilean lib/lean/Lean/Elab/Tactic/Guard.ir lib/lean/Lean/Elab/Tactic/Guard.olean @@ -4349,6 +5242,11 @@ lib/lean/Lean/Elab/Tactic/RCases.ir lib/lean/Lean/Elab/Tactic/RCases.olean lib/lean/Lean/Elab/Tactic/RCases.olean.private lib/lean/Lean/Elab/Tactic/RCases.olean.server +lib/lean/Lean/Elab/Tactic/RenameInaccessibles.ilean +lib/lean/Lean/Elab/Tactic/RenameInaccessibles.ir +lib/lean/Lean/Elab/Tactic/RenameInaccessibles.olean +lib/lean/Lean/Elab/Tactic/RenameInaccessibles.olean.private +lib/lean/Lean/Elab/Tactic/RenameInaccessibles.olean.server lib/lean/Lean/Elab/Tactic/Repeat.ilean lib/lean/Lean/Elab/Tactic/Repeat.ir lib/lean/Lean/Elab/Tactic/Repeat.olean @@ -4439,6 +5337,11 @@ lib/lean/Lean/Elab/Term.ir lib/lean/Lean/Elab/Term.olean lib/lean/Lean/Elab/Term.olean.private lib/lean/Lean/Elab/Term.olean.server +lib/lean/Lean/Elab/Term/TermElabM.ilean +lib/lean/Lean/Elab/Term/TermElabM.ir +lib/lean/Lean/Elab/Term/TermElabM.olean +lib/lean/Lean/Elab/Term/TermElabM.olean.private +lib/lean/Lean/Elab/Term/TermElabM.olean.server lib/lean/Lean/Elab/Time.ilean lib/lean/Lean/Elab/Time.ir lib/lean/Lean/Elab/Time.olean @@ -4539,6 +5442,11 @@ lib/lean/Lean/Expr.ir lib/lean/Lean/Expr.olean lib/lean/Lean/Expr.olean.private lib/lean/Lean/Expr.olean.server +lib/lean/Lean/ExtraModUses.ilean +lib/lean/Lean/ExtraModUses.ir +lib/lean/Lean/ExtraModUses.olean +lib/lean/Lean/ExtraModUses.olean.private +lib/lean/Lean/ExtraModUses.olean.server lib/lean/Lean/HeadIndex.ilean lib/lean/Lean/HeadIndex.ir lib/lean/Lean/HeadIndex.olean @@ -4619,6 +5527,11 @@ lib/lean/Lean/Linter/Deprecated.ir lib/lean/Lean/Linter/Deprecated.olean lib/lean/Lean/Linter/Deprecated.olean.private lib/lean/Lean/Linter/Deprecated.olean.server +lib/lean/Lean/Linter/DocsOnAlt.ilean +lib/lean/Lean/Linter/DocsOnAlt.ir +lib/lean/Lean/Linter/DocsOnAlt.olean +lib/lean/Lean/Linter/DocsOnAlt.olean.private +lib/lean/Lean/Linter/DocsOnAlt.olean.server lib/lean/Lean/Linter/List.ilean lib/lean/Lean/Linter/List.ir lib/lean/Lean/Linter/List.olean @@ -4784,16 +5697,26 @@ lib/lean/Lean/Meta/Constructions/CasesOn.ir lib/lean/Lean/Meta/Constructions/CasesOn.olean lib/lean/Lean/Meta/Constructions/CasesOn.olean.private lib/lean/Lean/Meta/Constructions/CasesOn.olean.server +lib/lean/Lean/Meta/Constructions/CasesOnSameCtor.ilean +lib/lean/Lean/Meta/Constructions/CasesOnSameCtor.ir +lib/lean/Lean/Meta/Constructions/CasesOnSameCtor.olean +lib/lean/Lean/Meta/Constructions/CasesOnSameCtor.olean.private +lib/lean/Lean/Meta/Constructions/CasesOnSameCtor.olean.server +lib/lean/Lean/Meta/Constructions/CtorElim.ilean +lib/lean/Lean/Meta/Constructions/CtorElim.ir +lib/lean/Lean/Meta/Constructions/CtorElim.olean +lib/lean/Lean/Meta/Constructions/CtorElim.olean.private +lib/lean/Lean/Meta/Constructions/CtorElim.olean.server +lib/lean/Lean/Meta/Constructions/CtorIdx.ilean +lib/lean/Lean/Meta/Constructions/CtorIdx.ir +lib/lean/Lean/Meta/Constructions/CtorIdx.olean +lib/lean/Lean/Meta/Constructions/CtorIdx.olean.private +lib/lean/Lean/Meta/Constructions/CtorIdx.olean.server lib/lean/Lean/Meta/Constructions/NoConfusion.ilean lib/lean/Lean/Meta/Constructions/NoConfusion.ir lib/lean/Lean/Meta/Constructions/NoConfusion.olean lib/lean/Lean/Meta/Constructions/NoConfusion.olean.private lib/lean/Lean/Meta/Constructions/NoConfusion.olean.server -lib/lean/Lean/Meta/Constructions/NoConfusionLinear.ilean -lib/lean/Lean/Meta/Constructions/NoConfusionLinear.ir -lib/lean/Lean/Meta/Constructions/NoConfusionLinear.olean -lib/lean/Lean/Meta/Constructions/NoConfusionLinear.olean.private -lib/lean/Lean/Meta/Constructions/NoConfusionLinear.olean.server lib/lean/Lean/Meta/Constructions/RecOn.ilean lib/lean/Lean/Meta/Constructions/RecOn.ir lib/lean/Lean/Meta/Constructions/RecOn.olean @@ -5024,11 +5947,26 @@ lib/lean/Lean/Meta/MatchUtil.ir lib/lean/Lean/Meta/MatchUtil.olean lib/lean/Lean/Meta/MatchUtil.olean.private lib/lean/Lean/Meta/MatchUtil.olean.server +lib/lean/Lean/Meta/MethodSpecs.ilean +lib/lean/Lean/Meta/MethodSpecs.ir +lib/lean/Lean/Meta/MethodSpecs.olean +lib/lean/Lean/Meta/MethodSpecs.olean.private +lib/lean/Lean/Meta/MethodSpecs.olean.server +lib/lean/Lean/Meta/MkIffOfInductiveProp.ilean +lib/lean/Lean/Meta/MkIffOfInductiveProp.ir +lib/lean/Lean/Meta/MkIffOfInductiveProp.olean +lib/lean/Lean/Meta/MkIffOfInductiveProp.olean.private +lib/lean/Lean/Meta/MkIffOfInductiveProp.olean.server lib/lean/Lean/Meta/NatInstTesters.ilean lib/lean/Lean/Meta/NatInstTesters.ir lib/lean/Lean/Meta/NatInstTesters.olean lib/lean/Lean/Meta/NatInstTesters.olean.private lib/lean/Lean/Meta/NatInstTesters.olean.server +lib/lean/Lean/Meta/NatTable.ilean +lib/lean/Lean/Meta/NatTable.ir +lib/lean/Lean/Meta/NatTable.olean +lib/lean/Lean/Meta/NatTable.olean.private +lib/lean/Lean/Meta/NatTable.olean.server lib/lean/Lean/Meta/Offset.ilean lib/lean/Lean/Meta/Offset.ir lib/lean/Lean/Meta/Offset.olean @@ -5064,6 +6002,11 @@ lib/lean/Lean/Meta/ReduceEval.ir lib/lean/Lean/Meta/ReduceEval.olean lib/lean/Lean/Meta/ReduceEval.olean.private lib/lean/Lean/Meta/ReduceEval.olean.server +lib/lean/Lean/Meta/SameCtorUtils.ilean +lib/lean/Lean/Meta/SameCtorUtils.ir +lib/lean/Lean/Meta/SameCtorUtils.olean +lib/lean/Lean/Meta/SameCtorUtils.olean.private +lib/lean/Lean/Meta/SameCtorUtils.olean.server lib/lean/Lean/Meta/SizeOf.ilean lib/lean/Lean/Meta/SizeOf.ir lib/lean/Lean/Meta/SizeOf.olean @@ -5209,11 +6152,91 @@ lib/lean/Lean/Meta/Tactic/Grind.ir lib/lean/Lean/Meta/Tactic/Grind.olean lib/lean/Lean/Meta/Tactic/Grind.olean.private lib/lean/Lean/Meta/Tactic/Grind.olean.server +lib/lean/Lean/Meta/Tactic/Grind/AC.ilean +lib/lean/Lean/Meta/Tactic/Grind/AC.ir +lib/lean/Lean/Meta/Tactic/Grind/AC.olean +lib/lean/Lean/Meta/Tactic/Grind/AC.olean.private +lib/lean/Lean/Meta/Tactic/Grind/AC.olean.server +lib/lean/Lean/Meta/Tactic/Grind/AC/Action.ilean +lib/lean/Lean/Meta/Tactic/Grind/AC/Action.ir +lib/lean/Lean/Meta/Tactic/Grind/AC/Action.olean +lib/lean/Lean/Meta/Tactic/Grind/AC/Action.olean.private +lib/lean/Lean/Meta/Tactic/Grind/AC/Action.olean.server +lib/lean/Lean/Meta/Tactic/Grind/AC/DenoteExpr.ilean +lib/lean/Lean/Meta/Tactic/Grind/AC/DenoteExpr.ir +lib/lean/Lean/Meta/Tactic/Grind/AC/DenoteExpr.olean +lib/lean/Lean/Meta/Tactic/Grind/AC/DenoteExpr.olean.private +lib/lean/Lean/Meta/Tactic/Grind/AC/DenoteExpr.olean.server +lib/lean/Lean/Meta/Tactic/Grind/AC/Eq.ilean +lib/lean/Lean/Meta/Tactic/Grind/AC/Eq.ir +lib/lean/Lean/Meta/Tactic/Grind/AC/Eq.olean +lib/lean/Lean/Meta/Tactic/Grind/AC/Eq.olean.private +lib/lean/Lean/Meta/Tactic/Grind/AC/Eq.olean.server +lib/lean/Lean/Meta/Tactic/Grind/AC/Internalize.ilean +lib/lean/Lean/Meta/Tactic/Grind/AC/Internalize.ir +lib/lean/Lean/Meta/Tactic/Grind/AC/Internalize.olean +lib/lean/Lean/Meta/Tactic/Grind/AC/Internalize.olean.private +lib/lean/Lean/Meta/Tactic/Grind/AC/Internalize.olean.server +lib/lean/Lean/Meta/Tactic/Grind/AC/Inv.ilean +lib/lean/Lean/Meta/Tactic/Grind/AC/Inv.ir +lib/lean/Lean/Meta/Tactic/Grind/AC/Inv.olean +lib/lean/Lean/Meta/Tactic/Grind/AC/Inv.olean.private +lib/lean/Lean/Meta/Tactic/Grind/AC/Inv.olean.server +lib/lean/Lean/Meta/Tactic/Grind/AC/PP.ilean +lib/lean/Lean/Meta/Tactic/Grind/AC/PP.ir +lib/lean/Lean/Meta/Tactic/Grind/AC/PP.olean +lib/lean/Lean/Meta/Tactic/Grind/AC/PP.olean.private +lib/lean/Lean/Meta/Tactic/Grind/AC/PP.olean.server +lib/lean/Lean/Meta/Tactic/Grind/AC/Proof.ilean +lib/lean/Lean/Meta/Tactic/Grind/AC/Proof.ir +lib/lean/Lean/Meta/Tactic/Grind/AC/Proof.olean +lib/lean/Lean/Meta/Tactic/Grind/AC/Proof.olean.private +lib/lean/Lean/Meta/Tactic/Grind/AC/Proof.olean.server +lib/lean/Lean/Meta/Tactic/Grind/AC/Seq.ilean +lib/lean/Lean/Meta/Tactic/Grind/AC/Seq.ir +lib/lean/Lean/Meta/Tactic/Grind/AC/Seq.olean +lib/lean/Lean/Meta/Tactic/Grind/AC/Seq.olean.private +lib/lean/Lean/Meta/Tactic/Grind/AC/Seq.olean.server +lib/lean/Lean/Meta/Tactic/Grind/AC/ToExpr.ilean +lib/lean/Lean/Meta/Tactic/Grind/AC/ToExpr.ir +lib/lean/Lean/Meta/Tactic/Grind/AC/ToExpr.olean +lib/lean/Lean/Meta/Tactic/Grind/AC/ToExpr.olean.private +lib/lean/Lean/Meta/Tactic/Grind/AC/ToExpr.olean.server +lib/lean/Lean/Meta/Tactic/Grind/AC/Types.ilean +lib/lean/Lean/Meta/Tactic/Grind/AC/Types.ir +lib/lean/Lean/Meta/Tactic/Grind/AC/Types.olean +lib/lean/Lean/Meta/Tactic/Grind/AC/Types.olean.private +lib/lean/Lean/Meta/Tactic/Grind/AC/Types.olean.server +lib/lean/Lean/Meta/Tactic/Grind/AC/Util.ilean +lib/lean/Lean/Meta/Tactic/Grind/AC/Util.ir +lib/lean/Lean/Meta/Tactic/Grind/AC/Util.olean +lib/lean/Lean/Meta/Tactic/Grind/AC/Util.olean.private +lib/lean/Lean/Meta/Tactic/Grind/AC/Util.olean.server +lib/lean/Lean/Meta/Tactic/Grind/AC/Var.ilean +lib/lean/Lean/Meta/Tactic/Grind/AC/Var.ir +lib/lean/Lean/Meta/Tactic/Grind/AC/Var.olean +lib/lean/Lean/Meta/Tactic/Grind/AC/Var.olean.private +lib/lean/Lean/Meta/Tactic/Grind/AC/Var.olean.server +lib/lean/Lean/Meta/Tactic/Grind/AC/VarRename.ilean +lib/lean/Lean/Meta/Tactic/Grind/AC/VarRename.ir +lib/lean/Lean/Meta/Tactic/Grind/AC/VarRename.olean +lib/lean/Lean/Meta/Tactic/Grind/AC/VarRename.olean.private +lib/lean/Lean/Meta/Tactic/Grind/AC/VarRename.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Action.ilean +lib/lean/Lean/Meta/Tactic/Grind/Action.ir +lib/lean/Lean/Meta/Tactic/Grind/Action.olean +lib/lean/Lean/Meta/Tactic/Grind/Action.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Action.olean.server lib/lean/Lean/Meta/Tactic/Grind/AlphaShareCommon.ilean lib/lean/Lean/Meta/Tactic/Grind/AlphaShareCommon.ir lib/lean/Lean/Meta/Tactic/Grind/AlphaShareCommon.olean lib/lean/Lean/Meta/Tactic/Grind/AlphaShareCommon.olean.private lib/lean/Lean/Meta/Tactic/Grind/AlphaShareCommon.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Anchor.ilean +lib/lean/Lean/Meta/Tactic/Grind/Anchor.ir +lib/lean/Lean/Meta/Tactic/Grind/Anchor.olean +lib/lean/Lean/Meta/Tactic/Grind/Anchor.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Anchor.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith.ir lib/lean/Lean/Meta/Tactic/Grind/Arith.olean @@ -5224,6 +6247,11 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Action.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Action.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Action.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Action.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Action.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.olean @@ -5234,6 +6262,11 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Functions.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Functions.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Functions.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Functions.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Functions.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.olean @@ -5244,6 +6277,31 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadCanon.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadCanon.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadCanon.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadCanon.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadCanon.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadRing.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadRing.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadRing.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadRing.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadRing.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadSemiring.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadSemiring.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadSemiring.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadSemiring.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadSemiring.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommRingM.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommRingM.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommRingM.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommRingM.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommRingM.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommSemiringM.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommSemiringM.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommSemiringM.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommSemiringM.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommSemiringM.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/PP.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/PP.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/PP.olean @@ -5269,11 +6327,21 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/ToExpr.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/ToExpr.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/ToExpr.olean @@ -5284,21 +6352,21 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.olean.server -lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.ilean -lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.ir -lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.olean -lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.olean.private -lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.olean.server -lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Var.ilean -lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Var.ir -lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Var.olean -lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Var.olean.private -lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Var.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/VarRename.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/VarRename.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/VarRename.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/VarRename.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/VarRename.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Action.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Action.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Action.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Action.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Action.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.olean @@ -5389,6 +6457,11 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/VarRename.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/VarRename.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/VarRename.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/VarRename.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/VarRename.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/EvalNum.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/EvalNum.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/EvalNum.olean @@ -5399,21 +6472,16 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/Insts.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Insts.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/Insts.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/Insts.olean.server -lib/lean/Lean/Meta/Tactic/Grind/Arith/Internalize.ilean -lib/lean/Lean/Meta/Tactic/Grind/Arith/Internalize.ir -lib/lean/Lean/Meta/Tactic/Grind/Arith/Internalize.olean -lib/lean/Lean/Meta/Tactic/Grind/Arith/Internalize.olean.private -lib/lean/Lean/Meta/Tactic/Grind/Arith/Internalize.olean.server -lib/lean/Lean/Meta/Tactic/Grind/Arith/Inv.ilean -lib/lean/Lean/Meta/Tactic/Grind/Arith/Inv.ir -lib/lean/Lean/Meta/Tactic/Grind/Arith/Inv.olean -lib/lean/Lean/Meta/Tactic/Grind/Arith/Inv.olean.private -lib/lean/Lean/Meta/Tactic/Grind/Arith/Inv.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Action.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Action.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Action.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Action.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Action.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.olean @@ -5434,6 +6502,11 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Inv.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Inv.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Inv.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Inv.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/LinearM.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/LinearM.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/LinearM.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/LinearM.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/LinearM.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/MBTC.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/MBTC.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/MBTC.olean @@ -5444,6 +6517,11 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Model.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Model.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Model.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Model.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/OfNatModule.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/OfNatModule.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/OfNatModule.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/OfNatModule.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/OfNatModule.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/PP.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/PP.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/PP.olean @@ -5499,6 +6577,11 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Var.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Var.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Var.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Var.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/VarRename.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/VarRename.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/VarRename.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/VarRename.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/VarRename.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/Main.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/Main.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Main.olean @@ -5544,11 +6627,6 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.olean.server -lib/lean/Lean/Meta/Tactic/Grind/Arith/ProofUtil.ilean -lib/lean/Lean/Meta/Tactic/Grind/Arith/ProofUtil.ir -lib/lean/Lean/Meta/Tactic/Grind/Arith/ProofUtil.olean -lib/lean/Lean/Meta/Tactic/Grind/Arith/ProofUtil.olean.private -lib/lean/Lean/Meta/Tactic/Grind/Arith/ProofUtil.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/Simproc.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/Simproc.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Simproc.olean @@ -5589,6 +6667,16 @@ lib/lean/Lean/Meta/Tactic/Grind/CasesMatch.ir lib/lean/Lean/Meta/Tactic/Grind/CasesMatch.olean lib/lean/Lean/Meta/Tactic/Grind/CasesMatch.olean.private lib/lean/Lean/Meta/Tactic/Grind/CasesMatch.olean.server +lib/lean/Lean/Meta/Tactic/Grind/CastLike.ilean +lib/lean/Lean/Meta/Tactic/Grind/CastLike.ir +lib/lean/Lean/Meta/Tactic/Grind/CastLike.olean +lib/lean/Lean/Meta/Tactic/Grind/CastLike.olean.private +lib/lean/Lean/Meta/Tactic/Grind/CastLike.olean.server +lib/lean/Lean/Meta/Tactic/Grind/CheckResult.ilean +lib/lean/Lean/Meta/Tactic/Grind/CheckResult.ir +lib/lean/Lean/Meta/Tactic/Grind/CheckResult.olean +lib/lean/Lean/Meta/Tactic/Grind/CheckResult.olean.private +lib/lean/Lean/Meta/Tactic/Grind/CheckResult.olean.server lib/lean/Lean/Meta/Tactic/Grind/Core.ilean lib/lean/Lean/Meta/Tactic/Grind/Core.ir lib/lean/Lean/Meta/Tactic/Grind/Core.olean @@ -5609,11 +6697,21 @@ lib/lean/Lean/Meta/Tactic/Grind/EMatch.ir lib/lean/Lean/Meta/Tactic/Grind/EMatch.olean lib/lean/Lean/Meta/Tactic/Grind/EMatch.olean.private lib/lean/Lean/Meta/Tactic/Grind/EMatch.olean.server +lib/lean/Lean/Meta/Tactic/Grind/EMatchAction.ilean +lib/lean/Lean/Meta/Tactic/Grind/EMatchAction.ir +lib/lean/Lean/Meta/Tactic/Grind/EMatchAction.olean +lib/lean/Lean/Meta/Tactic/Grind/EMatchAction.olean.private +lib/lean/Lean/Meta/Tactic/Grind/EMatchAction.olean.server lib/lean/Lean/Meta/Tactic/Grind/EMatchTheorem.ilean lib/lean/Lean/Meta/Tactic/Grind/EMatchTheorem.ir lib/lean/Lean/Meta/Tactic/Grind/EMatchTheorem.olean lib/lean/Lean/Meta/Tactic/Grind/EMatchTheorem.olean.private lib/lean/Lean/Meta/Tactic/Grind/EMatchTheorem.olean.server +lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremParam.ilean +lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremParam.ir +lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremParam.olean +lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremParam.olean.private +lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremParam.olean.server lib/lean/Lean/Meta/Tactic/Grind/EqResolution.ilean lib/lean/Lean/Meta/Tactic/Grind/EqResolution.ir lib/lean/Lean/Meta/Tactic/Grind/EqResolution.olean @@ -5644,6 +6742,11 @@ lib/lean/Lean/Meta/Tactic/Grind/Injection.ir lib/lean/Lean/Meta/Tactic/Grind/Injection.olean lib/lean/Lean/Meta/Tactic/Grind/Injection.olean.private lib/lean/Lean/Meta/Tactic/Grind/Injection.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Injective.ilean +lib/lean/Lean/Meta/Tactic/Grind/Injective.ir +lib/lean/Lean/Meta/Tactic/Grind/Injective.olean +lib/lean/Lean/Meta/Tactic/Grind/Injective.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Injective.olean.server lib/lean/Lean/Meta/Tactic/Grind/Internalize.ilean lib/lean/Lean/Meta/Tactic/Grind/Internalize.ir lib/lean/Lean/Meta/Tactic/Grind/Internalize.olean @@ -5694,6 +6797,51 @@ lib/lean/Lean/Meta/Tactic/Grind/MatchDiscrOnly.ir lib/lean/Lean/Meta/Tactic/Grind/MatchDiscrOnly.olean lib/lean/Lean/Meta/Tactic/Grind/MatchDiscrOnly.olean.private lib/lean/Lean/Meta/Tactic/Grind/MatchDiscrOnly.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Order.ilean +lib/lean/Lean/Meta/Tactic/Grind/Order.ir +lib/lean/Lean/Meta/Tactic/Grind/Order.olean +lib/lean/Lean/Meta/Tactic/Grind/Order.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Order.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Order/Assert.ilean +lib/lean/Lean/Meta/Tactic/Grind/Order/Assert.ir +lib/lean/Lean/Meta/Tactic/Grind/Order/Assert.olean +lib/lean/Lean/Meta/Tactic/Grind/Order/Assert.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Order/Assert.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Order/Internalize.ilean +lib/lean/Lean/Meta/Tactic/Grind/Order/Internalize.ir +lib/lean/Lean/Meta/Tactic/Grind/Order/Internalize.olean +lib/lean/Lean/Meta/Tactic/Grind/Order/Internalize.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Order/Internalize.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Order/OrderM.ilean +lib/lean/Lean/Meta/Tactic/Grind/Order/OrderM.ir +lib/lean/Lean/Meta/Tactic/Grind/Order/OrderM.olean +lib/lean/Lean/Meta/Tactic/Grind/Order/OrderM.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Order/OrderM.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Order/Proof.ilean +lib/lean/Lean/Meta/Tactic/Grind/Order/Proof.ir +lib/lean/Lean/Meta/Tactic/Grind/Order/Proof.olean +lib/lean/Lean/Meta/Tactic/Grind/Order/Proof.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Order/Proof.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Order/StructId.ilean +lib/lean/Lean/Meta/Tactic/Grind/Order/StructId.ir +lib/lean/Lean/Meta/Tactic/Grind/Order/StructId.olean +lib/lean/Lean/Meta/Tactic/Grind/Order/StructId.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Order/StructId.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Order/Types.ilean +lib/lean/Lean/Meta/Tactic/Grind/Order/Types.ir +lib/lean/Lean/Meta/Tactic/Grind/Order/Types.olean +lib/lean/Lean/Meta/Tactic/Grind/Order/Types.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Order/Types.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Order/Util.ilean +lib/lean/Lean/Meta/Tactic/Grind/Order/Util.ir +lib/lean/Lean/Meta/Tactic/Grind/Order/Util.olean +lib/lean/Lean/Meta/Tactic/Grind/Order/Util.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Order/Util.olean.server +lib/lean/Lean/Meta/Tactic/Grind/OrderInsts.ilean +lib/lean/Lean/Meta/Tactic/Grind/OrderInsts.ir +lib/lean/Lean/Meta/Tactic/Grind/OrderInsts.olean +lib/lean/Lean/Meta/Tactic/Grind/OrderInsts.olean.private +lib/lean/Lean/Meta/Tactic/Grind/OrderInsts.olean.server lib/lean/Lean/Meta/Tactic/Grind/PP.ilean lib/lean/Lean/Meta/Tactic/Grind/PP.ir lib/lean/Lean/Meta/Tactic/Grind/PP.olean @@ -5714,11 +6862,21 @@ lib/lean/Lean/Meta/Tactic/Grind/Proof.ir lib/lean/Lean/Meta/Tactic/Grind/Proof.olean lib/lean/Lean/Meta/Tactic/Grind/Proof.olean.private lib/lean/Lean/Meta/Tactic/Grind/Proof.olean.server +lib/lean/Lean/Meta/Tactic/Grind/ProofUtil.ilean +lib/lean/Lean/Meta/Tactic/Grind/ProofUtil.ir +lib/lean/Lean/Meta/Tactic/Grind/ProofUtil.olean +lib/lean/Lean/Meta/Tactic/Grind/ProofUtil.olean.private +lib/lean/Lean/Meta/Tactic/Grind/ProofUtil.olean.server lib/lean/Lean/Meta/Tactic/Grind/Propagate.ilean lib/lean/Lean/Meta/Tactic/Grind/Propagate.ir lib/lean/Lean/Meta/Tactic/Grind/Propagate.olean lib/lean/Lean/Meta/Tactic/Grind/Propagate.olean.private lib/lean/Lean/Meta/Tactic/Grind/Propagate.olean.server +lib/lean/Lean/Meta/Tactic/Grind/PropagateInj.ilean +lib/lean/Lean/Meta/Tactic/Grind/PropagateInj.ir +lib/lean/Lean/Meta/Tactic/Grind/PropagateInj.olean +lib/lean/Lean/Meta/Tactic/Grind/PropagateInj.olean.private +lib/lean/Lean/Meta/Tactic/Grind/PropagateInj.olean.server lib/lean/Lean/Meta/Tactic/Grind/PropagatorAttr.ilean lib/lean/Lean/Meta/Tactic/Grind/PropagatorAttr.ir lib/lean/Lean/Meta/Tactic/Grind/PropagatorAttr.olean @@ -5769,6 +6927,11 @@ lib/lean/Lean/Meta/Tactic/Grind/SynthInstance.ir lib/lean/Lean/Meta/Tactic/Grind/SynthInstance.olean lib/lean/Lean/Meta/Tactic/Grind/SynthInstance.olean.private lib/lean/Lean/Meta/Tactic/Grind/SynthInstance.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Theorems.ilean +lib/lean/Lean/Meta/Tactic/Grind/Theorems.ir +lib/lean/Lean/Meta/Tactic/Grind/Theorems.olean +lib/lean/Lean/Meta/Tactic/Grind/Theorems.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Theorems.olean.server lib/lean/Lean/Meta/Tactic/Grind/Types.ilean lib/lean/Lean/Meta/Tactic/Grind/Types.ir lib/lean/Lean/Meta/Tactic/Grind/Types.olean @@ -5779,6 +6942,11 @@ lib/lean/Lean/Meta/Tactic/Grind/Util.ir lib/lean/Lean/Meta/Tactic/Grind/Util.olean lib/lean/Lean/Meta/Tactic/Grind/Util.olean.private lib/lean/Lean/Meta/Tactic/Grind/Util.olean.server +lib/lean/Lean/Meta/Tactic/Grind/VarRename.ilean +lib/lean/Lean/Meta/Tactic/Grind/VarRename.ir +lib/lean/Lean/Meta/Tactic/Grind/VarRename.olean +lib/lean/Lean/Meta/Tactic/Grind/VarRename.olean.private +lib/lean/Lean/Meta/Tactic/Grind/VarRename.olean.server lib/lean/Lean/Meta/Tactic/IndependentOf.ilean lib/lean/Lean/Meta/Tactic/IndependentOf.ir lib/lean/Lean/Meta/Tactic/IndependentOf.olean @@ -5929,6 +7097,11 @@ lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.ir lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.olean.private lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.olean.server +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/CtorIdx.ilean +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/CtorIdx.ir +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/CtorIdx.olean +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/CtorIdx.olean.private +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/CtorIdx.olean.server lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.ilean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.ir lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.olean @@ -5944,6 +7117,11 @@ lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.ir lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.olean.private lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.olean.server +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/MethodSpecs.ilean +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/MethodSpecs.ir +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/MethodSpecs.olean +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/MethodSpecs.olean.private +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/MethodSpecs.olean.server lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.ilean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.ir lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.olean @@ -6189,6 +7367,11 @@ lib/lean/Lean/Parser/Term.ir lib/lean/Lean/Parser/Term.olean lib/lean/Lean/Parser/Term.olean.private lib/lean/Lean/Parser/Term.olean.server +lib/lean/Lean/Parser/Term/Basic.ilean +lib/lean/Lean/Parser/Term/Basic.ir +lib/lean/Lean/Parser/Term/Basic.olean +lib/lean/Lean/Parser/Term/Basic.olean.private +lib/lean/Lean/Parser/Term/Basic.olean.server lib/lean/Lean/Parser/Term/Doc.ilean lib/lean/Lean/Parser/Term/Doc.ir lib/lean/Lean/Parser/Term/Doc.olean @@ -6214,6 +7397,16 @@ lib/lean/Lean/PremiseSelection.ir lib/lean/Lean/PremiseSelection.olean lib/lean/Lean/PremiseSelection.olean.private lib/lean/Lean/PremiseSelection.olean.server +lib/lean/Lean/PremiseSelection/Basic.ilean +lib/lean/Lean/PremiseSelection/Basic.ir +lib/lean/Lean/PremiseSelection/Basic.olean +lib/lean/Lean/PremiseSelection/Basic.olean.private +lib/lean/Lean/PremiseSelection/Basic.olean.server +lib/lean/Lean/PremiseSelection/MePo.ilean +lib/lean/Lean/PremiseSelection/MePo.ir +lib/lean/Lean/PremiseSelection/MePo.olean +lib/lean/Lean/PremiseSelection/MePo.olean.private +lib/lean/Lean/PremiseSelection/MePo.olean.server lib/lean/Lean/PrettyPrinter.ilean lib/lean/Lean/PrettyPrinter.ir lib/lean/Lean/PrettyPrinter.olean @@ -6364,11 +7557,11 @@ lib/lean/Lean/Server/Completion/CompletionInfoSelection.ir lib/lean/Lean/Server/Completion/CompletionInfoSelection.olean lib/lean/Lean/Server/Completion/CompletionInfoSelection.olean.private lib/lean/Lean/Server/Completion/CompletionInfoSelection.olean.server -lib/lean/Lean/Server/Completion/CompletionItemData.ilean -lib/lean/Lean/Server/Completion/CompletionItemData.ir -lib/lean/Lean/Server/Completion/CompletionItemData.olean -lib/lean/Lean/Server/Completion/CompletionItemData.olean.private -lib/lean/Lean/Server/Completion/CompletionItemData.olean.server +lib/lean/Lean/Server/Completion/CompletionItemCompression.ilean +lib/lean/Lean/Server/Completion/CompletionItemCompression.ir +lib/lean/Lean/Server/Completion/CompletionItemCompression.olean +lib/lean/Lean/Server/Completion/CompletionItemCompression.olean.private +lib/lean/Lean/Server/Completion/CompletionItemCompression.olean.server lib/lean/Lean/Server/Completion/CompletionResolution.ilean lib/lean/Lean/Server/Completion/CompletionResolution.ir lib/lean/Lean/Server/Completion/CompletionResolution.olean @@ -6509,6 +7702,11 @@ lib/lean/Lean/Server/Test/Cancel.ir lib/lean/Lean/Server/Test/Cancel.olean lib/lean/Lean/Server/Test/Cancel.olean.private lib/lean/Lean/Server/Test/Cancel.olean.server +lib/lean/Lean/Server/Test/Refs.ilean +lib/lean/Lean/Server/Test/Refs.ir +lib/lean/Lean/Server/Test/Refs.olean +lib/lean/Lean/Server/Test/Refs.olean.private +lib/lean/Lean/Server/Test/Refs.olean.server lib/lean/Lean/Server/Test/Runner.ilean lib/lean/Lean/Server/Test/Runner.ir lib/lean/Lean/Server/Test/Runner.olean @@ -6729,6 +7927,11 @@ lib/lean/Lean/Util/ReplaceLevel.ir lib/lean/Lean/Util/ReplaceLevel.olean lib/lean/Lean/Util/ReplaceLevel.olean.private lib/lean/Lean/Util/ReplaceLevel.olean.server +lib/lean/Lean/Util/Reprove.ilean +lib/lean/Lean/Util/Reprove.ir +lib/lean/Lean/Util/Reprove.olean +lib/lean/Lean/Util/Reprove.olean.private +lib/lean/Lean/Util/Reprove.olean.server lib/lean/Lean/Util/SCC.ilean lib/lean/Lean/Util/SCC.ir lib/lean/Lean/Util/SCC.olean @@ -6739,11 +7942,6 @@ lib/lean/Lean/Util/SafeExponentiation.ir lib/lean/Lean/Util/SafeExponentiation.olean lib/lean/Lean/Util/SafeExponentiation.olean.private lib/lean/Lean/Util/SafeExponentiation.olean.server -lib/lean/Lean/Util/SearchPath.ilean -lib/lean/Lean/Util/SearchPath.ir -lib/lean/Lean/Util/SearchPath.olean -lib/lean/Lean/Util/SearchPath.olean.private -lib/lean/Lean/Util/SearchPath.olean.server lib/lean/Lean/Util/ShareCommon.ilean lib/lean/Lean/Util/ShareCommon.ir lib/lean/Lean/Util/ShareCommon.olean @@ -6779,6 +7977,11 @@ lib/lean/Lean/Widget/Basic.ir lib/lean/Lean/Widget/Basic.olean lib/lean/Lean/Widget/Basic.olean.private lib/lean/Lean/Widget/Basic.olean.server +lib/lean/Lean/Widget/Commands.ilean +lib/lean/Lean/Widget/Commands.ir +lib/lean/Lean/Widget/Commands.olean +lib/lean/Lean/Widget/Commands.olean.private +lib/lean/Lean/Widget/Commands.olean.server lib/lean/Lean/Widget/Diff.ilean lib/lean/Lean/Widget/Diff.ir lib/lean/Lean/Widget/Diff.olean @@ -6817,52 +8020,20 @@ lib/lean/Lean/Widget/UserWidget.olean.server lib/lean/Leanc.ilean lib/lean/Leanc.olean lib/lean/Std.ilean +lib/lean/Std.ir lib/lean/Std.olean -lib/lean/Std/Classes.ilean -lib/lean/Std/Classes.ir -lib/lean/Std/Classes.olean -lib/lean/Std/Classes.olean.private -lib/lean/Std/Classes.olean.server -lib/lean/Std/Classes/Ord.ilean -lib/lean/Std/Classes/Ord.ir -lib/lean/Std/Classes/Ord.olean -lib/lean/Std/Classes/Ord.olean.private -lib/lean/Std/Classes/Ord.olean.server -lib/lean/Std/Classes/Ord/Basic.ilean -lib/lean/Std/Classes/Ord/Basic.ir -lib/lean/Std/Classes/Ord/Basic.olean -lib/lean/Std/Classes/Ord/Basic.olean.private -lib/lean/Std/Classes/Ord/Basic.olean.server -lib/lean/Std/Classes/Ord/BitVec.ilean -lib/lean/Std/Classes/Ord/BitVec.ir -lib/lean/Std/Classes/Ord/BitVec.olean -lib/lean/Std/Classes/Ord/BitVec.olean.private -lib/lean/Std/Classes/Ord/BitVec.olean.server -lib/lean/Std/Classes/Ord/SInt.ilean -lib/lean/Std/Classes/Ord/SInt.ir -lib/lean/Std/Classes/Ord/SInt.olean -lib/lean/Std/Classes/Ord/SInt.olean.private -lib/lean/Std/Classes/Ord/SInt.olean.server -lib/lean/Std/Classes/Ord/String.ilean -lib/lean/Std/Classes/Ord/String.ir -lib/lean/Std/Classes/Ord/String.olean -lib/lean/Std/Classes/Ord/String.olean.private -lib/lean/Std/Classes/Ord/String.olean.server -lib/lean/Std/Classes/Ord/UInt.ilean -lib/lean/Std/Classes/Ord/UInt.ir -lib/lean/Std/Classes/Ord/UInt.olean -lib/lean/Std/Classes/Ord/UInt.olean.private -lib/lean/Std/Classes/Ord/UInt.olean.server -lib/lean/Std/Classes/Ord/Vector.ilean -lib/lean/Std/Classes/Ord/Vector.ir -lib/lean/Std/Classes/Ord/Vector.olean -lib/lean/Std/Classes/Ord/Vector.olean.private -lib/lean/Std/Classes/Ord/Vector.olean.server +lib/lean/Std.olean.private +lib/lean/Std.olean.server lib/lean/Std/Data.ilean lib/lean/Std/Data.ir lib/lean/Std/Data.olean lib/lean/Std/Data.olean.private lib/lean/Std/Data.olean.server +lib/lean/Std/Data/ByteSlice.ilean +lib/lean/Std/Data/ByteSlice.ir +lib/lean/Std/Data/ByteSlice.olean +lib/lean/Std/Data/ByteSlice.olean.private +lib/lean/Std/Data/ByteSlice.olean.server lib/lean/Std/Data/DHashMap.ilean lib/lean/Std/Data/DHashMap.ir lib/lean/Std/Data/DHashMap.olean @@ -6883,6 +8054,11 @@ lib/lean/Std/Data/DHashMap/Internal/AssocList/Basic.ir lib/lean/Std/Data/DHashMap/Internal/AssocList/Basic.olean lib/lean/Std/Data/DHashMap/Internal/AssocList/Basic.olean.private lib/lean/Std/Data/DHashMap/Internal/AssocList/Basic.olean.server +lib/lean/Std/Data/DHashMap/Internal/AssocList/Iterator.ilean +lib/lean/Std/Data/DHashMap/Internal/AssocList/Iterator.ir +lib/lean/Std/Data/DHashMap/Internal/AssocList/Iterator.olean +lib/lean/Std/Data/DHashMap/Internal/AssocList/Iterator.olean.private +lib/lean/Std/Data/DHashMap/Internal/AssocList/Iterator.olean.server lib/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.ilean lib/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.ir lib/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.olean @@ -6923,6 +8099,16 @@ lib/lean/Std/Data/DHashMap/Internal/WF.ir lib/lean/Std/Data/DHashMap/Internal/WF.olean lib/lean/Std/Data/DHashMap/Internal/WF.olean.private lib/lean/Std/Data/DHashMap/Internal/WF.olean.server +lib/lean/Std/Data/DHashMap/Iterator.ilean +lib/lean/Std/Data/DHashMap/Iterator.ir +lib/lean/Std/Data/DHashMap/Iterator.olean +lib/lean/Std/Data/DHashMap/Iterator.olean.private +lib/lean/Std/Data/DHashMap/Iterator.olean.server +lib/lean/Std/Data/DHashMap/IteratorLemmas.ilean +lib/lean/Std/Data/DHashMap/IteratorLemmas.ir +lib/lean/Std/Data/DHashMap/IteratorLemmas.olean +lib/lean/Std/Data/DHashMap/IteratorLemmas.olean.private +lib/lean/Std/Data/DHashMap/IteratorLemmas.olean.server lib/lean/Std/Data/DHashMap/Lemmas.ilean lib/lean/Std/Data/DHashMap/Lemmas.ir lib/lean/Std/Data/DHashMap/Lemmas.olean @@ -7148,6 +8334,16 @@ lib/lean/Std/Data/HashMap/Basic.ir lib/lean/Std/Data/HashMap/Basic.olean lib/lean/Std/Data/HashMap/Basic.olean.private lib/lean/Std/Data/HashMap/Basic.olean.server +lib/lean/Std/Data/HashMap/Iterator.ilean +lib/lean/Std/Data/HashMap/Iterator.ir +lib/lean/Std/Data/HashMap/Iterator.olean +lib/lean/Std/Data/HashMap/Iterator.olean.private +lib/lean/Std/Data/HashMap/Iterator.olean.server +lib/lean/Std/Data/HashMap/IteratorLemmas.ilean +lib/lean/Std/Data/HashMap/IteratorLemmas.ir +lib/lean/Std/Data/HashMap/IteratorLemmas.olean +lib/lean/Std/Data/HashMap/IteratorLemmas.olean.private +lib/lean/Std/Data/HashMap/IteratorLemmas.olean.server lib/lean/Std/Data/HashMap/Lemmas.ilean lib/lean/Std/Data/HashMap/Lemmas.ir lib/lean/Std/Data/HashMap/Lemmas.olean @@ -7173,6 +8369,16 @@ lib/lean/Std/Data/HashSet/Basic.ir lib/lean/Std/Data/HashSet/Basic.olean lib/lean/Std/Data/HashSet/Basic.olean.private lib/lean/Std/Data/HashSet/Basic.olean.server +lib/lean/Std/Data/HashSet/Iterator.ilean +lib/lean/Std/Data/HashSet/Iterator.ir +lib/lean/Std/Data/HashSet/Iterator.olean +lib/lean/Std/Data/HashSet/Iterator.olean.private +lib/lean/Std/Data/HashSet/Iterator.olean.server +lib/lean/Std/Data/HashSet/IteratorLemmas.ilean +lib/lean/Std/Data/HashSet/IteratorLemmas.ir +lib/lean/Std/Data/HashSet/IteratorLemmas.olean +lib/lean/Std/Data/HashSet/IteratorLemmas.olean.private +lib/lean/Std/Data/HashSet/IteratorLemmas.olean.server lib/lean/Std/Data/HashSet/Lemmas.ilean lib/lean/Std/Data/HashSet/Lemmas.ir lib/lean/Std/Data/HashSet/Lemmas.olean @@ -7633,6 +8839,11 @@ lib/lean/Std/Do/SPred/Notation.ir lib/lean/Std/Do/SPred/Notation.olean lib/lean/Std/Do/SPred/Notation.olean.private lib/lean/Std/Do/SPred/Notation.olean.server +lib/lean/Std/Do/SPred/Notation/Basic.ilean +lib/lean/Std/Do/SPred/Notation/Basic.ir +lib/lean/Std/Do/SPred/Notation/Basic.olean +lib/lean/Std/Do/SPred/Notation/Basic.olean.private +lib/lean/Std/Do/SPred/Notation/Basic.olean.server lib/lean/Std/Do/SPred/SPred.ilean lib/lean/Std/Do/SPred/SPred.ir lib/lean/Std/Do/SPred/SPred.olean @@ -7703,6 +8914,11 @@ lib/lean/Std/Internal/Async/DNS.ir lib/lean/Std/Internal/Async/DNS.olean lib/lean/Std/Internal/Async/DNS.olean.private lib/lean/Std/Internal/Async/DNS.olean.server +lib/lean/Std/Internal/Async/IO.ilean +lib/lean/Std/Internal/Async/IO.ir +lib/lean/Std/Internal/Async/IO.olean +lib/lean/Std/Internal/Async/IO.olean.private +lib/lean/Std/Internal/Async/IO.olean.server lib/lean/Std/Internal/Async/Process.ilean lib/lean/Std/Internal/Async/Process.ir lib/lean/Std/Internal/Async/Process.olean @@ -7713,6 +8929,11 @@ lib/lean/Std/Internal/Async/Select.ir lib/lean/Std/Internal/Async/Select.olean lib/lean/Std/Internal/Async/Select.olean.private lib/lean/Std/Internal/Async/Select.olean.server +lib/lean/Std/Internal/Async/Signal.ilean +lib/lean/Std/Internal/Async/Signal.ir +lib/lean/Std/Internal/Async/Signal.olean +lib/lean/Std/Internal/Async/Signal.olean.private +lib/lean/Std/Internal/Async/Signal.olean.server lib/lean/Std/Internal/Async/System.ilean lib/lean/Std/Internal/Async/System.ir lib/lean/Std/Internal/Async/System.olean @@ -7753,11 +8974,6 @@ lib/lean/Std/Internal/Parsec/String.ir lib/lean/Std/Internal/Parsec/String.olean lib/lean/Std/Internal/Parsec/String.olean.private lib/lean/Std/Internal/Parsec/String.olean.server -lib/lean/Std/Internal/Rat.ilean -lib/lean/Std/Internal/Rat.ir -lib/lean/Std/Internal/Rat.olean -lib/lean/Std/Internal/Rat.olean.private -lib/lean/Std/Internal/Rat.olean.server lib/lean/Std/Internal/UV.ilean lib/lean/Std/Internal/UV.ir lib/lean/Std/Internal/UV.olean @@ -7773,6 +8989,11 @@ lib/lean/Std/Internal/UV/Loop.ir lib/lean/Std/Internal/UV/Loop.olean lib/lean/Std/Internal/UV/Loop.olean.private lib/lean/Std/Internal/UV/Loop.olean.server +lib/lean/Std/Internal/UV/Signal.ilean +lib/lean/Std/Internal/UV/Signal.ir +lib/lean/Std/Internal/UV/Signal.olean +lib/lean/Std/Internal/UV/Signal.olean.private +lib/lean/Std/Internal/UV/Signal.olean.server lib/lean/Std/Internal/UV/System.ilean lib/lean/Std/Internal/UV/System.ir lib/lean/Std/Internal/UV/System.olean @@ -7943,6 +9164,16 @@ lib/lean/Std/Sync/Basic.ir lib/lean/Std/Sync/Basic.olean lib/lean/Std/Sync/Basic.olean.private lib/lean/Std/Sync/Basic.olean.server +lib/lean/Std/Sync/Broadcast.ilean +lib/lean/Std/Sync/Broadcast.ir +lib/lean/Std/Sync/Broadcast.olean +lib/lean/Std/Sync/Broadcast.olean.private +lib/lean/Std/Sync/Broadcast.olean.server +lib/lean/Std/Sync/CancellationToken.ilean +lib/lean/Std/Sync/CancellationToken.ir +lib/lean/Std/Sync/CancellationToken.olean +lib/lean/Std/Sync/CancellationToken.olean.private +lib/lean/Std/Sync/CancellationToken.olean.server lib/lean/Std/Sync/Channel.ilean lib/lean/Std/Sync/Channel.ir lib/lean/Std/Sync/Channel.olean @@ -7953,6 +9184,11 @@ lib/lean/Std/Sync/Mutex.ir lib/lean/Std/Sync/Mutex.olean lib/lean/Std/Sync/Mutex.olean.private lib/lean/Std/Sync/Mutex.olean.server +lib/lean/Std/Sync/Notify.ilean +lib/lean/Std/Sync/Notify.ir +lib/lean/Std/Sync/Notify.olean +lib/lean/Std/Sync/Notify.olean.private +lib/lean/Std/Sync/Notify.olean.server lib/lean/Std/Sync/RecursiveMutex.ilean lib/lean/Std/Sync/RecursiveMutex.ir lib/lean/Std/Sync/RecursiveMutex.olean @@ -7963,6 +9199,11 @@ lib/lean/Std/Sync/SharedMutex.ir lib/lean/Std/Sync/SharedMutex.olean lib/lean/Std/Sync/SharedMutex.olean.private lib/lean/Std/Sync/SharedMutex.olean.server +lib/lean/Std/Sync/StreamMap.ilean +lib/lean/Std/Sync/StreamMap.ir +lib/lean/Std/Sync/StreamMap.olean +lib/lean/Std/Sync/StreamMap.olean.private +lib/lean/Std/Sync/StreamMap.olean.server lib/lean/Std/Tactic.ilean lib/lean/Std/Tactic.ir lib/lean/Std/Tactic.olean @@ -8665,6 +9906,7 @@ lib/lean/libleanmanifest.a lib/lean/libleanrt.a lib/lean/libleanshared.so lib/lean/libleanshared_1.so +lib/lean/libleanshared_2.so share/lean/lean.mk %%DATADIR%%/src/lean/Init.lean %%DATADIR%%/src/lean/Init/BinderNameHint.lean @@ -8740,11 +9982,19 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Bool.lean %%DATADIR%%/src/lean/Init/Data/ByteArray.lean %%DATADIR%%/src/lean/Init/Data/ByteArray/Basic.lean +%%DATADIR%%/src/lean/Init/Data/ByteArray/Bootstrap.lean +%%DATADIR%%/src/lean/Init/Data/ByteArray/Extra.lean +%%DATADIR%%/src/lean/Init/Data/ByteArray/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Cast.lean %%DATADIR%%/src/lean/Init/Data/Char.lean %%DATADIR%%/src/lean/Init/Data/Char/Basic.lean %%DATADIR%%/src/lean/Init/Data/Char/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Char/Order.lean +%%DATADIR%%/src/lean/Init/Data/Dyadic.lean +%%DATADIR%%/src/lean/Init/Data/Dyadic/Basic.lean +%%DATADIR%%/src/lean/Init/Data/Dyadic/Instances.lean +%%DATADIR%%/src/lean/Init/Data/Dyadic/Inv.lean +%%DATADIR%%/src/lean/Init/Data/Dyadic/Round.lean %%DATADIR%%/src/lean/Init/Data/Fin.lean %%DATADIR%%/src/lean/Init/Data/Fin/Basic.lean %%DATADIR%%/src/lean/Init/Data/Fin/Bitwise.lean @@ -8786,9 +10036,11 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Iterators/Combinators.lean %%DATADIR%%/src/lean/Init/Data/Iterators/Combinators/Attach.lean %%DATADIR%%/src/lean/Init/Data/Iterators/Combinators/FilterMap.lean +%%DATADIR%%/src/lean/Init/Data/Iterators/Combinators/FlatMap.lean %%DATADIR%%/src/lean/Init/Data/Iterators/Combinators/Monadic.lean %%DATADIR%%/src/lean/Init/Data/Iterators/Combinators/Monadic/Attach.lean %%DATADIR%%/src/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean +%%DATADIR%%/src/lean/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean %%DATADIR%%/src/lean/Init/Data/Iterators/Combinators/Monadic/ULift.lean %%DATADIR%%/src/lean/Init/Data/Iterators/Combinators/ULift.lean %%DATADIR%%/src/lean/Init/Data/Iterators/Consumers.lean @@ -8810,9 +10062,11 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Iterators/Lemmas/Combinators.lean %%DATADIR%%/src/lean/Init/Data/Iterators/Lemmas/Combinators/Attach.lean %%DATADIR%%/src/lean/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean +%%DATADIR%%/src/lean/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean %%DATADIR%%/src/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean %%DATADIR%%/src/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean %%DATADIR%%/src/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean +%%DATADIR%%/src/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.lean %%DATADIR%%/src/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean %%DATADIR%%/src/lean/Init/Data/Iterators/Lemmas/Combinators/ULift.lean %%DATADIR%%/src/lean/Init/Data/Iterators/Lemmas/Consumers.lean @@ -8824,6 +10078,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Iterators/Lemmas/Monadic/Basic.lean %%DATADIR%%/src/lean/Init/Data/Iterators/PostconditionMonad.lean %%DATADIR%%/src/lean/Init/Data/Iterators/ToIterator.lean +%%DATADIR%%/src/lean/Init/Data/LawfulHashable.lean %%DATADIR%%/src/lean/Init/Data/List.lean %%DATADIR%%/src/lean/Init/Data/List/Attach.lean %%DATADIR%%/src/lean/Init/Data/List/Basic.lean @@ -8873,6 +10128,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Nat/Compare.lean %%DATADIR%%/src/lean/Init/Data/Nat/Control.lean +%%DATADIR%%/src/lean/Init/Data/Nat/Coprime.lean %%DATADIR%%/src/lean/Init/Data/Nat/Div.lean %%DATADIR%%/src/lean/Init/Data/Nat/Div/Basic.lean %%DATADIR%%/src/lean/Init/Data/Nat/Div/Lemmas.lean @@ -8902,10 +10158,22 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Option/List.lean %%DATADIR%%/src/lean/Init/Data/Option/Monadic.lean %%DATADIR%%/src/lean/Init/Data/Ord.lean +%%DATADIR%%/src/lean/Init/Data/Ord/Array.lean +%%DATADIR%%/src/lean/Init/Data/Ord/Basic.lean +%%DATADIR%%/src/lean/Init/Data/Ord/BitVec.lean +%%DATADIR%%/src/lean/Init/Data/Ord/SInt.lean +%%DATADIR%%/src/lean/Init/Data/Ord/String.lean +%%DATADIR%%/src/lean/Init/Data/Ord/UInt.lean +%%DATADIR%%/src/lean/Init/Data/Ord/Vector.lean %%DATADIR%%/src/lean/Init/Data/Order.lean %%DATADIR%%/src/lean/Init/Data/Order/Classes.lean +%%DATADIR%%/src/lean/Init/Data/Order/ClassesExtra.lean %%DATADIR%%/src/lean/Init/Data/Order/Factories.lean +%%DATADIR%%/src/lean/Init/Data/Order/FactoriesExtra.lean %%DATADIR%%/src/lean/Init/Data/Order/Lemmas.lean +%%DATADIR%%/src/lean/Init/Data/Order/LemmasExtra.lean +%%DATADIR%%/src/lean/Init/Data/Order/Ord.lean +%%DATADIR%%/src/lean/Init/Data/Order/PackageFactories.lean %%DATADIR%%/src/lean/Init/Data/PLift.lean %%DATADIR%%/src/lean/Init/Data/Prod.lean %%DATADIR%%/src/lean/Init/Data/Queue.lean @@ -8916,14 +10184,24 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Range/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Range/Polymorphic.lean %%DATADIR%%/src/lean/Init/Data/Range/Polymorphic/Basic.lean +%%DATADIR%%/src/lean/Init/Data/Range/Polymorphic/BitVec.lean +%%DATADIR%%/src/lean/Init/Data/Range/Polymorphic/GetElemTactic.lean +%%DATADIR%%/src/lean/Init/Data/Range/Polymorphic/Instances.lean +%%DATADIR%%/src/lean/Init/Data/Range/Polymorphic/Int.lean +%%DATADIR%%/src/lean/Init/Data/Range/Polymorphic/Internal/SignedBitVec.lean %%DATADIR%%/src/lean/Init/Data/Range/Polymorphic/Iterators.lean %%DATADIR%%/src/lean/Init/Data/Range/Polymorphic/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Range/Polymorphic/Nat.lean %%DATADIR%%/src/lean/Init/Data/Range/Polymorphic/NatLemmas.lean %%DATADIR%%/src/lean/Init/Data/Range/Polymorphic/PRange.lean %%DATADIR%%/src/lean/Init/Data/Range/Polymorphic/RangeIterator.lean +%%DATADIR%%/src/lean/Init/Data/Range/Polymorphic/SInt.lean %%DATADIR%%/src/lean/Init/Data/Range/Polymorphic/Stream.lean +%%DATADIR%%/src/lean/Init/Data/Range/Polymorphic/UInt.lean %%DATADIR%%/src/lean/Init/Data/Range/Polymorphic/UpwardEnumerable.lean +%%DATADIR%%/src/lean/Init/Data/Rat.lean +%%DATADIR%%/src/lean/Init/Data/Rat/Basic.lean +%%DATADIR%%/src/lean/Init/Data/Rat/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Repr.lean %%DATADIR%%/src/lean/Init/Data/SInt.lean %%DATADIR%%/src/lean/Init/Data/SInt/Basic.lean @@ -8943,8 +10221,18 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Stream.lean %%DATADIR%%/src/lean/Init/Data/String.lean %%DATADIR%%/src/lean/Init/Data/String/Basic.lean +%%DATADIR%%/src/lean/Init/Data/String/Bootstrap.lean +%%DATADIR%%/src/lean/Init/Data/String/Decode.lean %%DATADIR%%/src/lean/Init/Data/String/Extra.lean %%DATADIR%%/src/lean/Init/Data/String/Lemmas.lean +%%DATADIR%%/src/lean/Init/Data/String/Pattern.lean +%%DATADIR%%/src/lean/Init/Data/String/Pattern/Basic.lean +%%DATADIR%%/src/lean/Init/Data/String/Pattern/Char.lean +%%DATADIR%%/src/lean/Init/Data/String/Pattern/Pred.lean +%%DATADIR%%/src/lean/Init/Data/String/Pattern/String.lean +%%DATADIR%%/src/lean/Init/Data/String/Repr.lean +%%DATADIR%%/src/lean/Init/Data/String/Slice.lean +%%DATADIR%%/src/lean/Init/Data/String/Stream.lean %%DATADIR%%/src/lean/Init/Data/Subtype.lean %%DATADIR%%/src/lean/Init/Data/Subtype/Basic.lean %%DATADIR%%/src/lean/Init/Data/Subtype/Order.lean @@ -8955,6 +10243,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/ToString.lean %%DATADIR%%/src/lean/Init/Data/ToString/Basic.lean %%DATADIR%%/src/lean/Init/Data/ToString/Macro.lean +%%DATADIR%%/src/lean/Init/Data/ToString/Name.lean %%DATADIR%%/src/lean/Init/Data/UInt.lean %%DATADIR%%/src/lean/Init/Data/UInt/Basic.lean %%DATADIR%%/src/lean/Init/Data/UInt/BasicAux.lean @@ -8980,36 +10269,44 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Vector/OfFn.lean %%DATADIR%%/src/lean/Init/Data/Vector/Perm.lean %%DATADIR%%/src/lean/Init/Data/Vector/Range.lean +%%DATADIR%%/src/lean/Init/Data/Vector/Stream.lean %%DATADIR%%/src/lean/Init/Data/Vector/Zip.lean %%DATADIR%%/src/lean/Init/Data/Zero.lean %%DATADIR%%/src/lean/Init/Dynamic.lean %%DATADIR%%/src/lean/Init/Ext.lean %%DATADIR%%/src/lean/Init/GetElem.lean %%DATADIR%%/src/lean/Init/Grind.lean +%%DATADIR%%/src/lean/Init/Grind/AC.lean %%DATADIR%%/src/lean/Init/Grind/Attr.lean %%DATADIR%%/src/lean/Init/Grind/Cases.lean %%DATADIR%%/src/lean/Init/Grind/Ext.lean +%%DATADIR%%/src/lean/Init/Grind/Injective.lean +%%DATADIR%%/src/lean/Init/Grind/Interactive.lean %%DATADIR%%/src/lean/Init/Grind/Lemmas.lean %%DATADIR%%/src/lean/Init/Grind/Module.lean %%DATADIR%%/src/lean/Init/Grind/Module/Basic.lean %%DATADIR%%/src/lean/Init/Grind/Module/Envelope.lean +%%DATADIR%%/src/lean/Init/Grind/Module/NatModuleNorm.lean +%%DATADIR%%/src/lean/Init/Grind/Module/OfNatModule.lean %%DATADIR%%/src/lean/Init/Grind/Norm.lean %%DATADIR%%/src/lean/Init/Grind/Offset.lean +%%DATADIR%%/src/lean/Init/Grind/Order.lean %%DATADIR%%/src/lean/Init/Grind/Ordered.lean %%DATADIR%%/src/lean/Init/Grind/Ordered/Field.lean %%DATADIR%%/src/lean/Init/Grind/Ordered/Int.lean %%DATADIR%%/src/lean/Init/Grind/Ordered/Linarith.lean %%DATADIR%%/src/lean/Init/Grind/Ordered/Module.lean %%DATADIR%%/src/lean/Init/Grind/Ordered/Order.lean +%%DATADIR%%/src/lean/Init/Grind/Ordered/Rat.lean %%DATADIR%%/src/lean/Init/Grind/Ordered/Ring.lean %%DATADIR%%/src/lean/Init/Grind/PP.lean %%DATADIR%%/src/lean/Init/Grind/Propagator.lean %%DATADIR%%/src/lean/Init/Grind/Ring.lean %%DATADIR%%/src/lean/Init/Grind/Ring/Basic.lean +%%DATADIR%%/src/lean/Init/Grind/Ring/CommSemiringAdapter.lean +%%DATADIR%%/src/lean/Init/Grind/Ring/CommSolver.lean %%DATADIR%%/src/lean/Init/Grind/Ring/Envelope.lean %%DATADIR%%/src/lean/Init/Grind/Ring/Field.lean -%%DATADIR%%/src/lean/Init/Grind/Ring/OfSemiring.lean -%%DATADIR%%/src/lean/Init/Grind/Ring/Poly.lean %%DATADIR%%/src/lean/Init/Grind/Ring/ToInt.lean %%DATADIR%%/src/lean/Init/Grind/Tactics.lean %%DATADIR%%/src/lean/Init/Grind/ToInt.lean @@ -9022,6 +10319,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/GrindInstances/Ring/Fin.lean %%DATADIR%%/src/lean/Init/GrindInstances/Ring/Int.lean %%DATADIR%%/src/lean/Init/GrindInstances/Ring/Nat.lean +%%DATADIR%%/src/lean/Init/GrindInstances/Ring/Rat.lean %%DATADIR%%/src/lean/Init/GrindInstances/Ring/SInt.lean %%DATADIR%%/src/lean/Init/GrindInstances/Ring/UInt.lean %%DATADIR%%/src/lean/Init/GrindInstances/ToInt.lean @@ -9032,9 +10330,12 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Internal/Order/Basic.lean %%DATADIR%%/src/lean/Init/Internal/Order/Lemmas.lean %%DATADIR%%/src/lean/Init/Internal/Order/Tactic.lean +%%DATADIR%%/src/lean/Init/LawfulBEqTactics.lean %%DATADIR%%/src/lean/Init/MacroTrace.lean %%DATADIR%%/src/lean/Init/Meta.lean +%%DATADIR%%/src/lean/Init/Meta/Defs.lean %%DATADIR%%/src/lean/Init/MetaTypes.lean +%%DATADIR%%/src/lean/Init/MethodSpecsSimp.lean %%DATADIR%%/src/lean/Init/Notation.lean %%DATADIR%%/src/lean/Init/NotationExtra.lean %%DATADIR%%/src/lean/Init/Omega.lean @@ -9191,6 +10492,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Data/Array.lean %%DATADIR%%/src/lean/Lean/Data/AssocList.lean %%DATADIR%%/src/lean/Lean/Data/DeclarationRange.lean +%%DATADIR%%/src/lean/Lean/Data/EditDistance.lean %%DATADIR%%/src/lean/Lean/Data/Format.lean %%DATADIR%%/src/lean/Lean/Data/FuzzyMatching.lean %%DATADIR%%/src/lean/Lean/Data/Json.lean @@ -9251,7 +10553,12 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/DocString.lean %%DATADIR%%/src/lean/Lean/DocString/Add.lean %%DATADIR%%/src/lean/Lean/DocString/Extension.lean +%%DATADIR%%/src/lean/Lean/DocString/Formatter.lean %%DATADIR%%/src/lean/Lean/DocString/Links.lean +%%DATADIR%%/src/lean/Lean/DocString/Markdown.lean +%%DATADIR%%/src/lean/Lean/DocString/Parser.lean +%%DATADIR%%/src/lean/Lean/DocString/Syntax.lean +%%DATADIR%%/src/lean/Lean/DocString/Types.lean %%DATADIR%%/src/lean/Lean/Elab.lean %%DATADIR%%/src/lean/Lean/Elab/App.lean %%DATADIR%%/src/lean/Lean/Elab/Arg.lean @@ -9267,7 +10574,9 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/BuiltinTerm.lean %%DATADIR%%/src/lean/Lean/Elab/Calc.lean %%DATADIR%%/src/lean/Lean/Elab/CheckTactic.lean +%%DATADIR%%/src/lean/Lean/Elab/Coinductive.lean %%DATADIR%%/src/lean/Lean/Elab/Command.lean +%%DATADIR%%/src/lean/Lean/Elab/Command/Scope.lean %%DATADIR%%/src/lean/Lean/Elab/ComputedFields.lean %%DATADIR%%/src/lean/Lean/Elab/Config.lean %%DATADIR%%/src/lean/Lean/Elab/DeclModifiers.lean @@ -9283,14 +10592,22 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/Deriving/FromToJson.lean %%DATADIR%%/src/lean/Lean/Elab/Deriving/Hashable.lean %%DATADIR%%/src/lean/Lean/Elab/Deriving/Inhabited.lean +%%DATADIR%%/src/lean/Lean/Elab/Deriving/LawfulBEq.lean %%DATADIR%%/src/lean/Lean/Elab/Deriving/Nonempty.lean %%DATADIR%%/src/lean/Lean/Elab/Deriving/Ord.lean +%%DATADIR%%/src/lean/Lean/Elab/Deriving/ReflBEq.lean %%DATADIR%%/src/lean/Lean/Elab/Deriving/Repr.lean %%DATADIR%%/src/lean/Lean/Elab/Deriving/SizeOf.lean %%DATADIR%%/src/lean/Lean/Elab/Deriving/ToExpr.lean %%DATADIR%%/src/lean/Lean/Elab/Deriving/TypeName.lean %%DATADIR%%/src/lean/Lean/Elab/Deriving/Util.lean %%DATADIR%%/src/lean/Lean/Elab/Do.lean +%%DATADIR%%/src/lean/Lean/Elab/DocString.lean +%%DATADIR%%/src/lean/Lean/Elab/DocString/Builtin.lean +%%DATADIR%%/src/lean/Lean/Elab/DocString/Builtin/Keywords.lean +%%DATADIR%%/src/lean/Lean/Elab/DocString/Builtin/Parsing.lean +%%DATADIR%%/src/lean/Lean/Elab/DocString/Builtin/Postponed.lean +%%DATADIR%%/src/lean/Lean/Elab/DocString/Builtin/Scopes.lean %%DATADIR%%/src/lean/Lean/Elab/ElabRules.lean %%DATADIR%%/src/lean/Lean/Elab/ErrorExplanation.lean %%DATADIR%%/src/lean/Lean/Elab/Eval.lean @@ -9326,11 +10643,11 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Basic.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/EqUnfold.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Eqns.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/EqnsUtils.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/FixedParams.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Main.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/MkInhabitant.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Mutual.lean -%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Nonrec/Eqns.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/PartialFixpoint.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean @@ -9451,6 +10768,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/Tactic/Do/VCGen.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Do/VCGen/Basic.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Do/VCGen/Split.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/Do/VCGen/SuggestInvariant.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Doc.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/ElabTerm.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/ExposeNames.lean @@ -9458,6 +10776,13 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/Tactic/FalseOrByContra.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Generalize.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Grind.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/Grind/Basic.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/Grind/BuiltinTactic.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/Grind/Filter.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/Grind/Have.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/Grind/Main.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/Grind/ShowState.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/Grind/Trace.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Guard.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Induction.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Injection.lean @@ -9474,6 +10799,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/Tactic/Omega/MinNatAbs.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Omega/OmegaM.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/RCases.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/RenameInaccessibles.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Repeat.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Rewrite.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Rewrites.lean @@ -9492,6 +10818,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/Tactic/Try.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Unfold.lean %%DATADIR%%/src/lean/Lean/Elab/Term.lean +%%DATADIR%%/src/lean/Lean/Elab/Term/TermElabM.lean %%DATADIR%%/src/lean/Lean/Elab/Time.lean %%DATADIR%%/src/lean/Lean/Elab/Util.lean %%DATADIR%%/src/lean/Lean/Elab/WhereFinally.lean @@ -9513,6 +10840,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/ErrorExplanations/UnknownIdentifier.lean %%DATADIR%%/src/lean/Lean/Exception.lean %%DATADIR%%/src/lean/Lean/Expr.lean +%%DATADIR%%/src/lean/Lean/ExtraModUses.lean %%DATADIR%%/src/lean/Lean/HeadIndex.lean %%DATADIR%%/src/lean/Lean/Hygiene.lean %%DATADIR%%/src/lean/Lean/ImportingFlag.lean @@ -9529,6 +10857,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Linter/Builtin.lean %%DATADIR%%/src/lean/Lean/Linter/ConstructorAsVariable.lean %%DATADIR%%/src/lean/Lean/Linter/Deprecated.lean +%%DATADIR%%/src/lean/Lean/Linter/DocsOnAlt.lean %%DATADIR%%/src/lean/Lean/Linter/List.lean %%DATADIR%%/src/lean/Lean/Linter/MissingDocs.lean %%DATADIR%%/src/lean/Lean/Linter/Omit.lean @@ -9562,8 +10891,10 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Constructions.lean %%DATADIR%%/src/lean/Lean/Meta/Constructions/BRecOn.lean %%DATADIR%%/src/lean/Lean/Meta/Constructions/CasesOn.lean +%%DATADIR%%/src/lean/Lean/Meta/Constructions/CasesOnSameCtor.lean +%%DATADIR%%/src/lean/Lean/Meta/Constructions/CtorElim.lean +%%DATADIR%%/src/lean/Lean/Meta/Constructions/CtorIdx.lean %%DATADIR%%/src/lean/Lean/Meta/Constructions/NoConfusion.lean -%%DATADIR%%/src/lean/Lean/Meta/Constructions/NoConfusionLinear.lean %%DATADIR%%/src/lean/Lean/Meta/Constructions/RecOn.lean %%DATADIR%%/src/lean/Lean/Meta/CtorRecognizer.lean %%DATADIR%%/src/lean/Lean/Meta/DecLevel.lean @@ -9610,7 +10941,10 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Match/MatcherInfo.lean %%DATADIR%%/src/lean/Lean/Meta/Match/Value.lean %%DATADIR%%/src/lean/Lean/Meta/MatchUtil.lean +%%DATADIR%%/src/lean/Lean/Meta/MethodSpecs.lean +%%DATADIR%%/src/lean/Lean/Meta/MkIffOfInductiveProp.lean %%DATADIR%%/src/lean/Lean/Meta/NatInstTesters.lean +%%DATADIR%%/src/lean/Lean/Meta/NatTable.lean %%DATADIR%%/src/lean/Lean/Meta/Offset.lean %%DATADIR%%/src/lean/Lean/Meta/Order.lean %%DATADIR%%/src/lean/Lean/Meta/PPGoal.lean @@ -9618,6 +10952,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/RecursorInfo.lean %%DATADIR%%/src/lean/Lean/Meta/Reduce.lean %%DATADIR%%/src/lean/Lean/Meta/ReduceEval.lean +%%DATADIR%%/src/lean/Lean/Meta/SameCtorUtils.lean %%DATADIR%%/src/lean/Lean/Meta/SizeOf.lean %%DATADIR%%/src/lean/Lean/Meta/Sorry.lean %%DATADIR%%/src/lean/Lean/Meta/Structure.lean @@ -9647,24 +10982,49 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/FunIndInfo.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Generalize.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/AC.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/AC/Action.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/AC/DenoteExpr.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/AC/Eq.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/AC/Internalize.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/AC/Inv.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/AC/PP.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/AC/Proof.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/AC/Seq.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/AC/ToExpr.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/AC/Types.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/AC/Util.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/AC/Var.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/AC/VarRename.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Action.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/AlphaShareCommon.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Anchor.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Action.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Functions.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadCanon.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadRing.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadSemiring.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommRingM.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommSemiringM.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/PP.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/ToExpr.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean -%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean -%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Var.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/VarRename.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Action.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean @@ -9683,17 +11043,19 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/VarRename.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/EvalNum.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Insts.lean -%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Internalize.lean -%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Inv.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Linear.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Action.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Internalize.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Inv.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Linear/LinearM.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Linear/MBTC.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Model.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Linear/OfNatModule.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Linear/PP.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean @@ -9705,6 +11067,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Var.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Linear/VarRename.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Main.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Model.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/ModelUtil.lean @@ -9714,7 +11077,6 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Proof.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Types.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.lean -%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Simproc.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Types.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Util.lean @@ -9723,17 +11085,22 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Canon.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Cases.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/CasesMatch.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/CastLike.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/CheckResult.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Core.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Ctor.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Diseq.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/EMatch.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/EMatchAction.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/EMatchTheoremParam.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/EqResolution.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/ExprPtr.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Ext.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/ExtAttr.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/ForallProp.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Injection.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Injective.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Internalize.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Intro.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Inv.lean @@ -9744,11 +11111,22 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/MatchCond.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/MatchDiscrOnly.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Order.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Order/Assert.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Order/Internalize.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Order/OrderM.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Order/Proof.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Order/StructId.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Order/Types.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Order/Util.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/OrderInsts.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/PP.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Parser.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Proj.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Proof.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/ProofUtil.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Propagate.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/PropagateInj.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/PropagatorAttr.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/ProveEq.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/ReflCmp.lean @@ -9759,8 +11137,10 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Solve.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Split.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/SynthInstance.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Theorems.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Types.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Util.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/VarRename.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/IndependentOf.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Induction.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Injection.lean @@ -9791,9 +11171,11 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/CtorIdx.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/MethodSpecs.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/SInt.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean @@ -9843,11 +11225,14 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Parser/Tactic.lean %%DATADIR%%/src/lean/Lean/Parser/Tactic/Doc.lean %%DATADIR%%/src/lean/Lean/Parser/Term.lean +%%DATADIR%%/src/lean/Lean/Parser/Term/Basic.lean %%DATADIR%%/src/lean/Lean/Parser/Term/Doc.lean %%DATADIR%%/src/lean/Lean/Parser/Types.lean %%DATADIR%%/src/lean/Lean/ParserCompiler.lean %%DATADIR%%/src/lean/Lean/ParserCompiler/Attribute.lean %%DATADIR%%/src/lean/Lean/PremiseSelection.lean +%%DATADIR%%/src/lean/Lean/PremiseSelection/Basic.lean +%%DATADIR%%/src/lean/Lean/PremiseSelection/MePo.lean %%DATADIR%%/src/lean/Lean/PrettyPrinter.lean %%DATADIR%%/src/lean/Lean/PrettyPrinter/Basic.lean %%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator.lean @@ -9878,7 +11263,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Server/Completion.lean %%DATADIR%%/src/lean/Lean/Server/Completion/CompletionCollectors.lean %%DATADIR%%/src/lean/Lean/Server/Completion/CompletionInfoSelection.lean -%%DATADIR%%/src/lean/Lean/Server/Completion/CompletionItemData.lean +%%DATADIR%%/src/lean/Lean/Server/Completion/CompletionItemCompression.lean %%DATADIR%%/src/lean/Lean/Server/Completion/CompletionResolution.lean %%DATADIR%%/src/lean/Lean/Server/Completion/CompletionUtils.lean %%DATADIR%%/src/lean/Lean/Server/Completion/EligibleHeaderDecls.lean @@ -9908,6 +11293,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Server/Snapshots.lean %%DATADIR%%/src/lean/Lean/Server/Test.lean %%DATADIR%%/src/lean/Lean/Server/Test/Cancel.lean +%%DATADIR%%/src/lean/Lean/Server/Test/Refs.lean %%DATADIR%%/src/lean/Lean/Server/Test/Runner.lean %%DATADIR%%/src/lean/Lean/Server/Utils.lean %%DATADIR%%/src/lean/Lean/Server/Watchdog.lean @@ -9952,9 +11338,9 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Util/Recognizers.lean %%DATADIR%%/src/lean/Lean/Util/ReplaceExpr.lean %%DATADIR%%/src/lean/Lean/Util/ReplaceLevel.lean +%%DATADIR%%/src/lean/Lean/Util/Reprove.lean %%DATADIR%%/src/lean/Lean/Util/SCC.lean %%DATADIR%%/src/lean/Lean/Util/SafeExponentiation.lean -%%DATADIR%%/src/lean/Lean/Util/SearchPath.lean %%DATADIR%%/src/lean/Lean/Util/ShareCommon.lean %%DATADIR%%/src/lean/Lean/Util/Sorry.lean %%DATADIR%%/src/lean/Lean/Util/SortExprs.lean @@ -9962,6 +11348,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Util/Trace.lean %%DATADIR%%/src/lean/Lean/Widget.lean %%DATADIR%%/src/lean/Lean/Widget/Basic.lean +%%DATADIR%%/src/lean/Lean/Widget/Commands.lean %%DATADIR%%/src/lean/Lean/Widget/Diff.lean %%DATADIR%%/src/lean/Lean/Widget/InteractiveCode.lean %%DATADIR%%/src/lean/Lean/Widget/InteractiveDiagnostic.lean @@ -9971,19 +11358,13 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Widget/UserWidget.lean %%DATADIR%%/src/lean/Leanc.lean %%DATADIR%%/src/lean/Std.lean -%%DATADIR%%/src/lean/Std/Classes.lean -%%DATADIR%%/src/lean/Std/Classes/Ord.lean -%%DATADIR%%/src/lean/Std/Classes/Ord/Basic.lean -%%DATADIR%%/src/lean/Std/Classes/Ord/BitVec.lean -%%DATADIR%%/src/lean/Std/Classes/Ord/SInt.lean -%%DATADIR%%/src/lean/Std/Classes/Ord/String.lean -%%DATADIR%%/src/lean/Std/Classes/Ord/UInt.lean -%%DATADIR%%/src/lean/Std/Classes/Ord/Vector.lean %%DATADIR%%/src/lean/Std/Data.lean +%%DATADIR%%/src/lean/Std/Data/ByteSlice.lean %%DATADIR%%/src/lean/Std/Data/DHashMap.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/AdditionalOperations.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/Basic.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/AssocList/Basic.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/AssocList/Iterator.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Defs.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/HashesTo.lean @@ -9992,6 +11373,8 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Raw.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/WF.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Iterator.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/IteratorLemmas.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/Lemmas.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/Raw.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/RawDef.lean @@ -10037,11 +11420,15 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Std/Data/HashMap.lean %%DATADIR%%/src/lean/Std/Data/HashMap/AdditionalOperations.lean %%DATADIR%%/src/lean/Std/Data/HashMap/Basic.lean +%%DATADIR%%/src/lean/Std/Data/HashMap/Iterator.lean +%%DATADIR%%/src/lean/Std/Data/HashMap/IteratorLemmas.lean %%DATADIR%%/src/lean/Std/Data/HashMap/Lemmas.lean %%DATADIR%%/src/lean/Std/Data/HashMap/Raw.lean %%DATADIR%%/src/lean/Std/Data/HashMap/RawLemmas.lean %%DATADIR%%/src/lean/Std/Data/HashSet.lean %%DATADIR%%/src/lean/Std/Data/HashSet/Basic.lean +%%DATADIR%%/src/lean/Std/Data/HashSet/Iterator.lean +%%DATADIR%%/src/lean/Std/Data/HashSet/IteratorLemmas.lean %%DATADIR%%/src/lean/Std/Data/HashSet/Lemmas.lean %%DATADIR%%/src/lean/Std/Data/HashSet/Raw.lean %%DATADIR%%/src/lean/Std/Data/HashSet/RawLemmas.lean @@ -10134,6 +11521,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Std/Do/SPred/DerivedLaws.lean %%DATADIR%%/src/lean/Std/Do/SPred/Laws.lean %%DATADIR%%/src/lean/Std/Do/SPred/Notation.lean +%%DATADIR%%/src/lean/Std/Do/SPred/Notation/Basic.lean %%DATADIR%%/src/lean/Std/Do/SPred/SPred.lean %%DATADIR%%/src/lean/Std/Do/SPred/SVal.lean %%DATADIR%%/src/lean/Std/Do/Triple.lean @@ -10148,8 +11536,10 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Std/Internal/Async.lean %%DATADIR%%/src/lean/Std/Internal/Async/Basic.lean %%DATADIR%%/src/lean/Std/Internal/Async/DNS.lean +%%DATADIR%%/src/lean/Std/Internal/Async/IO.lean %%DATADIR%%/src/lean/Std/Internal/Async/Process.lean %%DATADIR%%/src/lean/Std/Internal/Async/Select.lean +%%DATADIR%%/src/lean/Std/Internal/Async/Signal.lean %%DATADIR%%/src/lean/Std/Internal/Async/System.lean %%DATADIR%%/src/lean/Std/Internal/Async/TCP.lean %%DATADIR%%/src/lean/Std/Internal/Async/Timer.lean @@ -10158,10 +11548,10 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Std/Internal/Parsec/Basic.lean %%DATADIR%%/src/lean/Std/Internal/Parsec/ByteArray.lean %%DATADIR%%/src/lean/Std/Internal/Parsec/String.lean -%%DATADIR%%/src/lean/Std/Internal/Rat.lean %%DATADIR%%/src/lean/Std/Internal/UV.lean %%DATADIR%%/src/lean/Std/Internal/UV/DNS.lean %%DATADIR%%/src/lean/Std/Internal/UV/Loop.lean +%%DATADIR%%/src/lean/Std/Internal/UV/Signal.lean %%DATADIR%%/src/lean/Std/Internal/UV/System.lean %%DATADIR%%/src/lean/Std/Internal/UV/TCP.lean %%DATADIR%%/src/lean/Std/Internal/UV/Timer.lean @@ -10196,10 +11586,14 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Std/Sync.lean %%DATADIR%%/src/lean/Std/Sync/Barrier.lean %%DATADIR%%/src/lean/Std/Sync/Basic.lean +%%DATADIR%%/src/lean/Std/Sync/Broadcast.lean +%%DATADIR%%/src/lean/Std/Sync/CancellationToken.lean %%DATADIR%%/src/lean/Std/Sync/Channel.lean %%DATADIR%%/src/lean/Std/Sync/Mutex.lean +%%DATADIR%%/src/lean/Std/Sync/Notify.lean %%DATADIR%%/src/lean/Std/Sync/RecursiveMutex.lean %%DATADIR%%/src/lean/Std/Sync/SharedMutex.lean +%%DATADIR%%/src/lean/Std/Sync/StreamMap.lean %%DATADIR%%/src/lean/Std/Tactic.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast.lean @@ -10351,6 +11745,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/Build/Fetch.lean %%DATADIR%%/src/lean/lake/Lake/Build/Index.lean %%DATADIR%%/src/lean/lake/Lake/Build/Info.lean +%%DATADIR%%/src/lean/lake/Lake/Build/Infos.lean %%DATADIR%%/src/lean/lake/Lake/Build/InitFacets.lean %%DATADIR%%/src/lean/lake/Lake/Build/InputFile.lean %%DATADIR%%/src/lean/lake/Lake/Build/Job.lean @@ -10406,11 +11801,13 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/Config/LeanLib.lean %%DATADIR%%/src/lean/lake/Lake/Config/LeanLibConfig.lean %%DATADIR%%/src/lean/lake/Lake/Config/Meta.lean +%%DATADIR%%/src/lean/lake/Lake/Config/MetaClasses.lean %%DATADIR%%/src/lean/lake/Lake/Config/Module.lean %%DATADIR%%/src/lean/lake/Lake/Config/Monad.lean %%DATADIR%%/src/lean/lake/Lake/Config/Opaque.lean %%DATADIR%%/src/lean/lake/Lake/Config/OutFormat.lean %%DATADIR%%/src/lean/lake/Lake/Config/Package.lean +%%DATADIR%%/src/lean/lake/Lake/Config/PackageConfig.lean %%DATADIR%%/src/lean/lake/Lake/Config/Pattern.lean %%DATADIR%%/src/lean/lake/Lake/Config/Script.lean %%DATADIR%%/src/lean/lake/Lake/Config/TargetConfig.lean @@ -10455,6 +11852,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/Toml/Grammar.lean %%DATADIR%%/src/lean/lake/Lake/Toml/Load.lean %%DATADIR%%/src/lean/lake/Lake/Toml/ParserUtil.lean +%%DATADIR%%/src/lean/lake/Lake/Util.lean %%DATADIR%%/src/lean/lake/Lake/Util/Binder.lean %%DATADIR%%/src/lean/lake/Lake/Util/Casing.lean %%DATADIR%%/src/lean/lake/Lake/Util/Cli.lean @@ -10470,7 +11868,6 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/Util/IO.lean %%DATADIR%%/src/lean/lake/Lake/Util/JsonObject.lean %%DATADIR%%/src/lean/lake/Lake/Util/Lift.lean -%%DATADIR%%/src/lean/lake/Lake/Util/List.lean %%DATADIR%%/src/lean/lake/Lake/Util/Lock.lean %%DATADIR%%/src/lean/lake/Lake/Util/Log.lean %%DATADIR%%/src/lean/lake/Lake/Util/MainM.lean @@ -10483,173 +11880,13 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/Util/OrderedTagAttribute.lean %%DATADIR%%/src/lean/lake/Lake/Util/Proc.lean %%DATADIR%%/src/lean/lake/Lake/Util/RBArray.lean +%%DATADIR%%/src/lean/lake/Lake/Util/Reservoir.lean %%DATADIR%%/src/lean/lake/Lake/Util/Store.lean %%DATADIR%%/src/lean/lake/Lake/Util/StoreInsts.lean -%%DATADIR%%/src/lean/lake/Lake/Util/Sugar.lean +%%DATADIR%%/src/lean/lake/Lake/Util/String.lean %%DATADIR%%/src/lean/lake/Lake/Util/Task.lean +%%DATADIR%%/src/lean/lake/Lake/Util/Url.lean %%DATADIR%%/src/lean/lake/Lake/Util/Version.lean %%DATADIR%%/src/lean/lake/Lake/Version.lean %%DATADIR%%/src/lean/lake/LakeMain.lean %%DATADIR%%/src/lean/lake/README.md -%%DATADIR%%/src/lean/lake/tests/8448/A.lean -%%DATADIR%%/src/lean/lake/tests/8448/B.lean -%%DATADIR%%/src/lean/lake/tests/8448/C.lean -%%DATADIR%%/src/lean/lake/tests/8448/D.lean -%%DATADIR%%/src/lean/lake/tests/8448/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/api/keys.lean -%%DATADIR%%/src/lean/lake/tests/badImport/Etc.lean -%%DATADIR%%/src/lean/lake/tests/badImport/Lib/B.lean -%%DATADIR%%/src/lean/lake/tests/badImport/Lib/B1.lean -%%DATADIR%%/src/lean/lake/tests/badImport/Lib/S.lean -%%DATADIR%%/src/lean/lake/tests/badImport/Lib/U.lean -%%DATADIR%%/src/lean/lake/tests/badImport/X.lean -%%DATADIR%%/src/lean/lake/tests/badImport/X1.lean -%%DATADIR%%/src/lean/lake/tests/badImport/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/buildArgs/Hello.lean -%%DATADIR%%/src/lean/lake/tests/buildArgs/Main.lean -%%DATADIR%%/src/lean/lake/tests/buildArgs/foo.lean -%%DATADIR%%/src/lean/lake/tests/buildArgs/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/cache/Main.lean -%%DATADIR%%/src/lean/lake/tests/cache/Module.lean -%%DATADIR%%/src/lean/lake/tests/cache/Test.lean -%%DATADIR%%/src/lean/lake/tests/cache/Test/Imported.lean -%%DATADIR%%/src/lean/lake/tests/clone/test/Main.lean -%%DATADIR%%/src/lean/lake/tests/clone/test/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/driver/Test.lean -%%DATADIR%%/src/lean/lake/tests/driver/build.lean -%%DATADIR%%/src/lean/lake/tests/driver/dep-invalid.lean -%%DATADIR%%/src/lean/lake/tests/driver/dep-unknown.lean -%%DATADIR%%/src/lean/lake/tests/driver/dep.lean -%%DATADIR%%/src/lean/lake/tests/driver/dep/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/driver/driver.lean -%%DATADIR%%/src/lean/lake/tests/driver/exe.lean -%%DATADIR%%/src/lean/lake/tests/driver/lib.lean -%%DATADIR%%/src/lean/lake/tests/driver/none.lean -%%DATADIR%%/src/lean/lake/tests/driver/runner.lean -%%DATADIR%%/src/lean/lake/tests/driver/script.lean -%%DATADIR%%/src/lean/lake/tests/driver/two.lean -%%DATADIR%%/src/lean/lake/tests/driver/unknown.lean -%%DATADIR%%/src/lean/lake/tests/externLib/Main.lean -%%DATADIR%%/src/lean/lake/tests/externLib/Test.lean -%%DATADIR%%/src/lean/lake/tests/externLib/ffi/FFI.lean -%%DATADIR%%/src/lean/lake/tests/externLib/ffi/Main.lean -%%DATADIR%%/src/lean/lake/tests/externLib/ffi/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/globs/TBA.lean -%%DATADIR%%/src/lean/lake/tests/globs/TBA/Eulerian.lean -%%DATADIR%%/src/lean/lake/tests/globs/TBA/Eulerian/A.lean -%%DATADIR%%/src/lean/lake/tests/globs/Test/1.lean -%%DATADIR%%/src/lean/lake/tests/globs/Test/Subtest/1.lean -%%DATADIR%%/src/lean/lake/tests/globs/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/inputFile/lakefile.expected.lean -%%DATADIR%%/src/lean/lake/tests/inputFile/lakefileAlt.lean -%%DATADIR%%/src/lean/lake/tests/inputFile/test.lean -%%DATADIR%%/src/lean/lake/tests/kinds/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/lean/Lib.lean -%%DATADIR%%/src/lean/lake/tests/lean/Lib/Basic.lean -%%DATADIR%%/src/lean/lake/tests/lean/Lib/Foo.Bar.lean -%%DATADIR%%/src/lean/lake/tests/lean/Test.lean -%%DATADIR%%/src/lean/lake/tests/lean/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/llvm-bitcode-gen/LlvmBitcodeGen.lean -%%DATADIR%%/src/lean/lake/tests/llvm-bitcode-gen/LlvmBitcodeGen/Basic.lean -%%DATADIR%%/src/lean/lake/tests/llvm-bitcode-gen/Main.lean -%%DATADIR%%/src/lean/lake/tests/llvm-bitcode-gen/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/lock/Error.lean -%%DATADIR%%/src/lean/lake/tests/lock/Loop.lean -%%DATADIR%%/src/lean/lake/tests/lock/Nop.lean -%%DATADIR%%/src/lean/lake/tests/lock/Wait.lean -%%DATADIR%%/src/lean/lake/tests/lock/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/logLevel/Log/Error.lean -%%DATADIR%%/src/lean/lake/tests/logLevel/Log/Info.lean -%%DATADIR%%/src/lean/lake/tests/logLevel/Log/Warning.lean -%%DATADIR%%/src/lean/lake/tests/logLevel/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/manifest/bar/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/manifest/foo/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/manifest/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/meta/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/module/ErrorTest/CrossPackageImportAll.lean -%%DATADIR%%/src/lean/lake/tests/module/Test/Module/Import.lean -%%DATADIR%%/src/lean/lake/tests/module/Test/Module/ImportAll.lean -%%DATADIR%%/src/lean/lake/tests/module/Test/Module/ImportAllImport.lean -%%DATADIR%%/src/lean/lake/tests/module/Test/Module/ImportAllImportAll.lean -%%DATADIR%%/src/lean/lake/tests/module/Test/Module/ImportAllMetaImport.lean -%%DATADIR%%/src/lean/lake/tests/module/Test/Module/ImportImport.lean -%%DATADIR%%/src/lean/lake/tests/module/Test/Module/ImportImportAll.lean -%%DATADIR%%/src/lean/lake/tests/module/Test/Module/ImportMetaImport.lean -%%DATADIR%%/src/lean/lake/tests/module/Test/Module/ImportPublicMetaImport.lean -%%DATADIR%%/src/lean/lake/tests/module/Test/Module/MetaImport.lean -%%DATADIR%%/src/lean/lake/tests/module/Test/Module/MetaImportPublicImport.lean -%%DATADIR%%/src/lean/lake/tests/module/Test/Module/PromoteImport.lean -%%DATADIR%%/src/lean/lake/tests/module/Test/Module/PromoteTransImport.lean -%%DATADIR%%/src/lean/lake/tests/module/Test/Module/PublicImport.lean -%%DATADIR%%/src/lean/lake/tests/module/Test/Module/PublicMetaImport.lean -%%DATADIR%%/src/lean/lake/tests/module/Test/NonModule/Import.lean -%%DATADIR%%/src/lean/lake/tests/module/Test/NonModule/ImportModuleImport.lean -%%DATADIR%%/src/lean/lake/tests/module/dep/Dep/Module.lean -%%DATADIR%%/src/lean/lake/tests/noBuild/ImportTest.lean -%%DATADIR%%/src/lean/lake/tests/noBuild/Test.lean -%%DATADIR%%/src/lean/lake/tests/noBuild/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/noRelease/Test.lean -%%DATADIR%%/src/lean/lake/tests/noRelease/dep/Dep.lean -%%DATADIR%%/src/lean/lake/tests/noRelease/dep/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/noRelease/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/online/barrel.lean -%%DATADIR%%/src/lean/lake/tests/online/require.lean -%%DATADIR%%/src/lean/lake/tests/order/A.lean -%%DATADIR%%/src/lean/lake/tests/order/A/B.lean -%%DATADIR%%/src/lean/lake/tests/order/A/B/C.lean -%%DATADIR%%/src/lean/lake/tests/order/Y.lean -%%DATADIR%%/src/lean/lake/tests/order/bar/X.lean -%%DATADIR%%/src/lean/lake/tests/order/bar/Y.lean -%%DATADIR%%/src/lean/lake/tests/order/bar/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/order/baz/X.lean -%%DATADIR%%/src/lean/lake/tests/order/baz/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/order/foo/X.lean -%%DATADIR%%/src/lean/lake/tests/order/foo/Y.lean -%%DATADIR%%/src/lean/lake/tests/order/foo/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/order/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/order/leaf/Z.lean -%%DATADIR%%/src/lean/lake/tests/order/leaf/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/packageOverrides/bar1/bar.lean -%%DATADIR%%/src/lean/lake/tests/packageOverrides/bar2/bar.lean -%%DATADIR%%/src/lean/lake/tests/packageOverrides/foo/foo.lean -%%DATADIR%%/src/lean/lake/tests/packageOverrides/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/postUpdate/dep/hello.lean -%%DATADIR%%/src/lean/lake/tests/postUpdate/dep/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/postUpdate/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/precompileLink/Downstream.lean -%%DATADIR%%/src/lean/lake/tests/precompileLink/Downstream/Import.lean -%%DATADIR%%/src/lean/lake/tests/precompileLink/Foo.lean -%%DATADIR%%/src/lean/lake/tests/precompileLink/Foo/Bar.lean -%%DATADIR%%/src/lean/lake/tests/precompileLink/Foo/Baz.lean -%%DATADIR%%/src/lean/lake/tests/precompileLink/FooDep.lean -%%DATADIR%%/src/lean/lake/tests/precompileLink/FooDepDep.lean -%%DATADIR%%/src/lean/lake/tests/precompileLink/ImportDownstream.lean -%%DATADIR%%/src/lean/lake/tests/precompileLink/Indirect.lean -%%DATADIR%%/src/lean/lake/tests/precompileLink/LakeTest.lean -%%DATADIR%%/src/lean/lake/tests/precompileLink/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/precompileLink/orderTest.lean -%%DATADIR%%/src/lean/lake/tests/query/exe.lean -%%DATADIR%%/src/lean/lake/tests/query/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/query/lib/A.lean -%%DATADIR%%/src/lean/lake/tests/query/lib/B.lean -%%DATADIR%%/src/lean/lake/tests/query/lib/C.lean -%%DATADIR%%/src/lean/lake/tests/rebuild/Main.lean -%%DATADIR%%/src/lean/lake/tests/rebuild/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/reservoirConfig/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/reversion/Hello.lean -%%DATADIR%%/src/lean/lake/tests/reversion/Main.lean -%%DATADIR%%/src/lean/lake/tests/reversion/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/setupFile/ImportFoo.lean -%%DATADIR%%/src/lean/lake/tests/setupFile/ImportTest.lean -%%DATADIR%%/src/lean/lake/tests/setupFile/Test.lean -%%DATADIR%%/src/lean/lake/tests/setupFile/Test/Foo.Bar.lean -%%DATADIR%%/src/lean/lake/tests/setupFile/invalid.lean -%%DATADIR%%/src/lean/lake/tests/toml/README.md -%%DATADIR%%/src/lean/lake/tests/toml/Test.lean -%%DATADIR%%/src/lean/lake/tests/toolchain/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/trace/Foo.lean -%%DATADIR%%/src/lean/lake/tests/translateConfig/out.expected.lean -%%DATADIR%%/src/lean/lake/tests/translateConfig/source.lean -%%DATADIR%%/src/lean/lake/tests/updateToolchain/test.lean -%%DATADIR%%/src/lean/lake/tests/versionTags/lakefile.lean -@dir lib/lean/Leanc diff --git a/math/libformfactor/Makefile b/math/libformfactor/Makefile index 6b7759aaeff6..27f6a3c80614 100644 --- a/math/libformfactor/Makefile +++ b/math/libformfactor/Makefile @@ -1,5 +1,5 @@ PORTNAME= libformfactor -DISTVERSION= 0.3.1 +DISTVERSION= 0.3.2 CATEGORIES= math MASTER_SITES= https://jugit.fz-juelich.de/mlz/libformfactor/-/archive/v${DISTVERSION}/ DISTNAME= ${PORTNAME}-v${DISTVERSION} @@ -19,6 +19,6 @@ USE_LDCONFIG= yes CMAKE_OFF= BUILD_TESTING CMAKE_TESTING_ON= BUILD_TESTING -# tests as of 0.3.1: 100% tests passed, 0 tests failed out of 18 +# tests as of 0.3.2: 100% tests passed, 0 tests failed out of 18 .include <bsd.port.mk> diff --git a/math/libformfactor/distinfo b/math/libformfactor/distinfo index 740bbdeadc2c..4f2b8d7d0faa 100644 --- a/math/libformfactor/distinfo +++ b/math/libformfactor/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1737283223 -SHA256 (libformfactor-v0.3.1.tar.gz) = bd03cf8dc77c87116d89932f923e7592e59edecb1bab520a188644198bfe0d68 -SIZE (libformfactor-v0.3.1.tar.gz) = 317693 +TIMESTAMP = 1764046052 +SHA256 (libformfactor-v0.3.2.tar.gz) = 093acaa061afa957d8776e3713a891ca6f9240ab539ca902fca9953d6056c7e1 +SIZE (libformfactor-v0.3.2.tar.gz) = 318758 diff --git a/math/libformfactor/pkg-plist b/math/libformfactor/pkg-plist index 94646141525d..604b37cdd769 100644 --- a/math/libformfactor/pkg-plist +++ b/math/libformfactor/pkg-plist @@ -10,4 +10,4 @@ include/ff/Polyhedron.h include/ff/Prism.h include/ff/Topology.h lib/libformfactor.so -lib/libformfactor.so.0.3.1 +lib/libformfactor.so.0.3.2 diff --git a/math/libpoly/Makefile b/math/libpoly/Makefile index 0e85bafaadcb..7e2002e705f9 100644 --- a/math/libpoly/Makefile +++ b/math/libpoly/Makefile @@ -1,6 +1,6 @@ PORTNAME= libpoly DISTVERSIONPREFIX= v -DISTVERSION= 0.2.0 +DISTVERSION= 0.2.1 CATEGORIES= math MAINTAINER= yuri@FreeBSD.org @@ -26,6 +26,6 @@ CMAKE_OFF= LIBPOLY_BUILD_PYTHON_API LIBPOLY_BUILD_STATIC LIBPOLY_BUILD_STATIC_PI CFLAGS+= -Wno-error=unused-but-set-variable .endif -# tests as of 0.2.0: 100% tests passed, 0 tests failed out of 14 +# tests as of 0.2.1: 100% tests passed, 0 tests failed out of 15 .include <bsd.port.post.mk> diff --git a/math/libpoly/distinfo b/math/libpoly/distinfo index 831611f67b9c..5851b332dd36 100644 --- a/math/libpoly/distinfo +++ b/math/libpoly/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1746379622 -SHA256 (SRI-CSL-libpoly-v0.2.0_GH0.tar.gz) = 146adc0d3f6fe8038adb6b8b69dd16114a4be12f520d5c1fb333f3746d233abe -SIZE (SRI-CSL-libpoly-v0.2.0_GH0.tar.gz) = 641486 +TIMESTAMP = 1764441566 +SHA256 (SRI-CSL-libpoly-v0.2.1_GH0.tar.gz) = b662ea4d7515426aeccda090339dbb086629a2f6ba4688b7710a892f7d2c7c58 +SIZE (SRI-CSL-libpoly-v0.2.1_GH0.tar.gz) = 629599 diff --git a/math/lmfit/Makefile b/math/lmfit/Makefile index efd8b1b0dff4..e2136ff525b6 100644 --- a/math/lmfit/Makefile +++ b/math/lmfit/Makefile @@ -1,5 +1,5 @@ PORTNAME= lmfit -DISTVERSION= 9.0 +DISTVERSION= 10.0 CATEGORIES= math MASTER_SITES= https://jugit.fz-juelich.de/mlz/${PORTNAME}/-/archive/v${DISTVERSION}/ DISTNAME= ${PORTNAME}-v${DISTVERSION} @@ -23,4 +23,6 @@ CMAKE_TESTING_ON= BUILD_TESTING OPTIONS_DEFINE= DOCS PORTDOCS= * +# tests as of 10.0 fail: 100% tests passed, 0 tests failed out of 3 + .include <bsd.port.mk> diff --git a/math/lmfit/distinfo b/math/lmfit/distinfo index 297874a06a49..a02e392faff8 100644 --- a/math/lmfit/distinfo +++ b/math/lmfit/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1674550325 -SHA256 (lmfit-v9.0.tar.gz) = 2e854c4b0a8f0ecddd4b8a63cfb8266ace02d191c4362762cb80aa84e781b0c3 -SIZE (lmfit-v9.0.tar.gz) = 36686 +TIMESTAMP = 1764046230 +SHA256 (lmfit-v10.0.tar.gz) = ac8d5c36a168d5e09b2cd128b752b704a0572c4c29afa8bbff0894eb721482f3 +SIZE (lmfit-v10.0.tar.gz) = 36887 diff --git a/math/lmfit/pkg-plist b/math/lmfit/pkg-plist index 5be0a2f8a774..91e72f00e8dd 100644 --- a/math/lmfit/pkg-plist +++ b/math/lmfit/pkg-plist @@ -4,9 +4,13 @@ include/lmdecls.h include/lmfit.hpp include/lmmin.h include/lmstruct.h +lib/cmake/lmfit/lmfitConfig.cmake +lib/cmake/lmfit/lmfitConfigVersion.cmake +lib/cmake/lmfit/lmfitTargets-%%CMAKE_BUILD_TYPE%%.cmake +lib/cmake/lmfit/lmfitTargets.cmake lib/liblmfit.so -lib/liblmfit.so.9 -lib/liblmfit.so.9.0.0 +lib/liblmfit.so.10 +lib/liblmfit.so.10.0.0 libdata/pkgconfig/lmfit.pc share/man/man3/lmcurve.3.gz share/man/man3/lmcurve2.3.gz diff --git a/math/mpfrc++/Makefile b/math/mpfrc++/Makefile index 3da3ee5f551d..e09f182d508a 100644 --- a/math/mpfrc++/Makefile +++ b/math/mpfrc++/Makefile @@ -1,11 +1,12 @@ PORTNAME= mpfrc++ DISTVERSIONPREFIX= ${PORTNAME}- -DISTVERSION= 3.7.1 +DISTVERSION= 3.7.2 CATEGORIES= math devel MAINTAINER= yuri@FreeBSD.org COMMENT= High-performance C++ interface for MPFR library -WWW= http://www.holoborodko.com/pavel/mpfr/ +WWW= http://www.holoborodko.com/pavel/mpfr/ \ + https://github.com/advanpix/mpreal LICENSE= GPLv3 LICENSE_FILE= ${WRKSRC}/copying.txt diff --git a/math/mpfrc++/distinfo b/math/mpfrc++/distinfo index a53aaba09016..87596b5182ff 100644 --- a/math/mpfrc++/distinfo +++ b/math/mpfrc++/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1713282177 -SHA256 (advanpix-mpreal-mpfrc++-3.7.1_GH0.tar.gz) = f83b4a850e6f93e7770286fd615a656142d6ca856768e2c43a72df2d077e939b -SIZE (advanpix-mpreal-mpfrc++-3.7.1_GH0.tar.gz) = 38993 +TIMESTAMP = 1763916663 +SHA256 (advanpix-mpreal-mpfrc++-3.7.2_GH0.tar.gz) = 5e31deda0809da078bff43eda7d1117545818f4704f97289c92c34b6f91c2923 +SIZE (advanpix-mpreal-mpfrc++-3.7.2_GH0.tar.gz) = 39460 diff --git a/math/mumps4/Makefile b/math/mumps4/Makefile index 72ab350a3fbf..d519ac452426 100644 --- a/math/mumps4/Makefile +++ b/math/mumps4/Makefile @@ -15,7 +15,7 @@ WWW= https://mumps-solver.org/ LICENSE= PD LICENSE_FILE= ${WRKSRC}/LICENSE -USES= fortran +USES= fortran:gfortran MAKE_JOBS_UNSAFE=yes diff --git a/math/octave-forge-llms/Makefile b/math/octave-forge-llms/Makefile index 0d12ef804dd1..21c9fc32b8f4 100644 --- a/math/octave-forge-llms/Makefile +++ b/math/octave-forge-llms/Makefile @@ -17,6 +17,8 @@ USE_GITHUB= yes GH_ACCOUNT= pr0m1th3as GH_PROJECT= octave-llms +BROKEN_arm64= does not build + OCTAVE_SRC= ${GH_PROJECT}-release-${DISTVERSION} .include <bsd.port.mk> diff --git a/math/octave-forge-quaternion/Makefile b/math/octave-forge-quaternion/Makefile index 115514edb48e..494f37a34803 100644 --- a/math/octave-forge-quaternion/Makefile +++ b/math/octave-forge-quaternion/Makefile @@ -1,6 +1,5 @@ PORTNAME= octave-forge-quaternion -PORTVERSION= 2.4.0 -PORTREVISION= 20 +PORTVERSION= 2.4.1 CATEGORIES= math MASTER_SITES= SF/octave/Octave%20Forge%20Packages/Individual%20Package%20Releases DISTNAME= ${OCTAVE_PKGNAME}-${DISTVERSIONFULL} @@ -14,6 +13,6 @@ LICENSE_FILE= ${WRKDIR}/${OCTAVE_SRC}/COPYING USES= octave -OCTAVE_SRC= ${OCTAVE_PKGNAME} +OCTAVE_SRC= ${OCTAVE_PKGNAME}-${PORTVERSION} .include <bsd.port.mk> diff --git a/math/octave-forge-quaternion/distinfo b/math/octave-forge-quaternion/distinfo index c70b821119a3..855452469379 100644 --- a/math/octave-forge-quaternion/distinfo +++ b/math/octave-forge-quaternion/distinfo @@ -1,2 +1,3 @@ -SHA256 (octave-forge/quaternion-2.4.0.tar.gz) = 4c2d4dd8f1d213f080519c6f9dfbbdca068087ee0411122b16e377e0f4641610 -SIZE (octave-forge/quaternion-2.4.0.tar.gz) = 236821 +TIMESTAMP = 1764038244 +SHA256 (octave-forge/quaternion-2.4.1.tar.gz) = 918e6653b749b948e9aee6fe2d3735047e9819d1273fdc9d5f49515347e63981 +SIZE (octave-forge/quaternion-2.4.1.tar.gz) = 43766 diff --git a/math/octave-forge-quaternion/files/patch-is__real__array.cc b/math/octave-forge-quaternion/files/patch-is__real__array.cc deleted file mode 100644 index e39f8fa46d0a..000000000000 --- a/math/octave-forge-quaternion/files/patch-is__real__array.cc +++ /dev/null @@ -1,13 +0,0 @@ ---- is_real_array.cc.orig 2021-02-21 22:03:11 UTC -+++ is_real_array.cc -@@ -46,8 +46,8 @@ Avoid nasty stuff like @code{true = isreal (\"a\")}.\n - { - // args(i).ndims () should be always >= 2 - if (args(i).ndims () < 2 -- || ! ((args(i).is_numeric_type () && args(i).is_real_type ()) -- || args(i).is_bool_type ())) -+ || ! ((args(i).isnumeric () && args(i).isreal ()) -+ || args(i).islogical ())) - { - retval = false; - break; diff --git a/math/pari/Makefile b/math/pari/Makefile index 89e0e68cb132..6206e7116fb3 100644 --- a/math/pari/Makefile +++ b/math/pari/Makefile @@ -1,5 +1,5 @@ PORTNAME= pari -DISTVERSION= 2.17.2 +DISTVERSION= 2.17.3 PORTEPOCH= 2 CATEGORIES= math MASTER_SITES= https://pari.math.u-bordeaux.fr/pub/pari/unix/ diff --git a/math/pari/distinfo b/math/pari/distinfo index e463c27ba4d5..06c2dfd2fc5b 100644 --- a/math/pari/distinfo +++ b/math/pari/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1741278431 -SHA256 (pari-2.17.2.tar.gz) = 7d30578f5cf97b137a281f4548d131aafc0cde86bcfd10cc1e1bd72a81e65061 -SIZE (pari-2.17.2.tar.gz) = 5326642 +TIMESTAMP = 1764209412 +SHA256 (pari-2.17.3.tar.gz) = 8d9c4fcd584c468d27e0f23c36836587284452094c4b1c404c20c4b810462dcb +SIZE (pari-2.17.3.tar.gz) = 5331018 diff --git a/math/py-altgraph/Makefile b/math/py-altgraph/Makefile index 4a764dd24deb..fbd12f453542 100644 --- a/math/py-altgraph/Makefile +++ b/math/py-altgraph/Makefile @@ -1,6 +1,5 @@ PORTNAME= altgraph -PORTVERSION= 0.17.4 -PORTREVISION= 1 +PORTVERSION= 0.17.5 CATEGORIES= math python MASTER_SITES= PYPI PKGNAMEPREFIX= ${PYTHON_PKGNAMEPREFIX} @@ -13,8 +12,11 @@ WWW= https://altgraph.readthedocs.io/en/latest/ \ LICENSE= MIT LICENSE_FILE= ${WRKSRC}/LICENSE +BUILD_DEPENDS= ${PYTHON_PKGNAMEPREFIX}setuptools>=0:devel/py-setuptools@${PY_FLAVOR} \ + ${PYTHON_PKGNAMEPREFIX}wheel>=0:devel/py-wheel@${PY_FLAVOR} + USES= python -USE_PYTHON= autoplist concurrent distutils unittest +USE_PYTHON= autoplist concurrent pep517 unittest NO_ARCH= yes diff --git a/math/py-altgraph/distinfo b/math/py-altgraph/distinfo index f3a8245c8a7b..119092672f50 100644 --- a/math/py-altgraph/distinfo +++ b/math/py-altgraph/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1696002170 -SHA256 (altgraph-0.17.4.tar.gz) = 1b5afbb98f6c4dcadb2e2ae6ab9fa994bbb8c1d75f4fa96d340f9437ae454406 -SIZE (altgraph-0.17.4.tar.gz) = 48418 +TIMESTAMP = 1763854462 +SHA256 (altgraph-0.17.5.tar.gz) = c87b395dd12fabde9c99573a9749d67da8d29ef9de0125c7f536699b4a9bc9e7 +SIZE (altgraph-0.17.5.tar.gz) = 48428 diff --git a/math/py-blis/Makefile b/math/py-blis/Makefile index 153586695a61..dd807038540f 100644 --- a/math/py-blis/Makefile +++ b/math/py-blis/Makefile @@ -1,6 +1,5 @@ PORTNAME= blis -PORTVERSION= 1.3.0 -PORTREVISION= 1 +PORTVERSION= 1.3.3 CATEGORIES= math python MASTER_SITES= PYPI \ https://github.com/explosion/cython-blis/releases/download/release-v${PORTVERSION}/ diff --git a/math/py-blis/distinfo b/math/py-blis/distinfo index cf8b341a2188..8bff8e95d68f 100644 --- a/math/py-blis/distinfo +++ b/math/py-blis/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1744289022 -SHA256 (blis-1.3.0.tar.gz) = 1695a87e3fc4c20d9b9140f5238cac0514c411b750e8cdcec5d8320c71f62e99 -SIZE (blis-1.3.0.tar.gz) = 2510328 +TIMESTAMP = 1763853416 +SHA256 (blis-1.3.3.tar.gz) = 034d4560ff3cc43e8aa37e188451b0440e3261d989bb8a42ceee865607715ecd +SIZE (blis-1.3.3.tar.gz) = 2644873 diff --git a/math/py-blis/files/patch-pyproject.toml b/math/py-blis/files/patch-pyproject.toml new file mode 100644 index 000000000000..5c1f19fb2327 --- /dev/null +++ b/math/py-blis/files/patch-pyproject.toml @@ -0,0 +1,11 @@ +--- pyproject.toml.orig 2025-11-14 15:00:34 UTC ++++ pyproject.toml +@@ -2,7 +2,7 @@ requires = [ + requires = [ + "setuptools", + "cython>=3.0,<4.0", +- "numpy>=2.0.0,<3.0.0", ++ "numpy>=1.19.3,<3.0.0", + ] + build-backend = "setuptools.build_meta" + diff --git a/math/py-blis/files/patch-setup.py b/math/py-blis/files/patch-setup.py index ebd4020cd70d..7e23157a3e80 100644 --- a/math/py-blis/files/patch-setup.py +++ b/math/py-blis/files/patch-setup.py @@ -1,11 +1,11 @@ ---- setup.py.orig 2025-04-03 12:23:45 UTC +--- setup.py.orig 2025-11-14 15:00:34 UTC +++ setup.py @@ -303,7 +303,7 @@ setup( setup( setup_requires=[ "cython>=3.0,<4.0", - "numpy>=2.0.0,<3.0.0", -+ "numpy>=1.19.0,<3.0.0", ++ "numpy>=1.19.3,<3.0.0", ], install_requires=[ "numpy>=1.15.0,<3.0.0; python_version < '3.9'", diff --git a/math/py-faiss/Makefile b/math/py-faiss/Makefile index 355434f96dc8..6801ffbd259d 100644 --- a/math/py-faiss/Makefile +++ b/math/py-faiss/Makefile @@ -1,6 +1,6 @@ PORTNAME= faiss DISTVERSIONPREFIX= v -DISTVERSION= 1.11.0 +DISTVERSION= 1.13.0 CATEGORIES= math PKGNAMEPREFIX= ${PYTHON_PKGNAMEPREFIX} diff --git a/math/py-faiss/distinfo b/math/py-faiss/distinfo index 840cf5ea3b37..946b7027702e 100644 --- a/math/py-faiss/distinfo +++ b/math/py-faiss/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1745711421 -SHA256 (facebookresearch-faiss-v1.11.0_GH0.tar.gz) = c5d517da6deb6a6d74290d7145331fc7474426025e2d826fa4a6d40670f4493c -SIZE (facebookresearch-faiss-v1.11.0_GH0.tar.gz) = 1138777 +TIMESTAMP = 1763960009 +SHA256 (facebookresearch-faiss-v1.13.0_GH0.tar.gz) = 6db002fc020fb8d02adaafd06e1b3b8fb4f9301d25d18392e27eb6e63be0361b +SIZE (facebookresearch-faiss-v1.13.0_GH0.tar.gz) = 1214369 diff --git a/math/py-libpoly/Makefile b/math/py-libpoly/Makefile index 0a3164e63fa5..9efa08bd608d 100644 --- a/math/py-libpoly/Makefile +++ b/math/py-libpoly/Makefile @@ -1,13 +1,9 @@ PORTNAME= libpoly DISTVERSIONPREFIX= v -DISTVERSION= 0.1.13 -PORTREVISION= 1 +DISTVERSION= 0.2.1 CATEGORIES= math PKGNAMEPREFIX= ${PYTHON_PKGNAMEPREFIX} -PATCH_SITES= https://github.com/SRI-CSL/libpoly/commit/ -PATCHFILES= 48f48f945111ab021bed4ad4f192f2cac0c2e84b.patch:-p1 - MAINTAINER= yuri@FreeBSD.org COMMENT= Python binding for libpoly WWW= https://github.com/SRI-CSL/libpoly diff --git a/math/py-libpoly/distinfo b/math/py-libpoly/distinfo index e6c77d6e3e06..d25953bd1e9b 100644 --- a/math/py-libpoly/distinfo +++ b/math/py-libpoly/distinfo @@ -1,5 +1,5 @@ -TIMESTAMP = 1707514827 -SHA256 (SRI-CSL-libpoly-v0.1.13_GH0.tar.gz) = ca7092eeeced3dd8bd86cdd3410207802ef1752d7052d92eee3e9e6bb496763c -SIZE (SRI-CSL-libpoly-v0.1.13_GH0.tar.gz) = 621704 +TIMESTAMP = 1764445691 +SHA256 (SRI-CSL-libpoly-v0.2.1_GH0.tar.gz) = b662ea4d7515426aeccda090339dbb086629a2f6ba4688b7710a892f7d2c7c58 +SIZE (SRI-CSL-libpoly-v0.2.1_GH0.tar.gz) = 629599 SHA256 (48f48f945111ab021bed4ad4f192f2cac0c2e84b.patch) = 6ea0843a890445bf54b267111bf6515ba8931f72b8d2dd509bdf4d171f3be692 SIZE (48f48f945111ab021bed4ad4f192f2cac0c2e84b.patch) = 2511 diff --git a/math/py-libpoly/files/patch-CMakeLists.txt b/math/py-libpoly/files/patch-CMakeLists.txt index d2ba6e85d001..2080180203fd 100644 --- a/math/py-libpoly/files/patch-CMakeLists.txt +++ b/math/py-libpoly/files/patch-CMakeLists.txt @@ -1,6 +1,6 @@ ---- CMakeLists.txt.orig 2021-04-12 16:09:58 UTC +--- CMakeLists.txt.orig 2025-11-28 09:04:30 UTC +++ CMakeLists.txt -@@ -58,7 +58,7 @@ if(HAVE_OPEN_MEMSTREAM) +@@ -61,7 +61,7 @@ endif() endif() # Configure the library source @@ -9,17 +9,19 @@ # Configure the headers add_subdirectory(include) -@@ -72,11 +72,11 @@ if(LIBPOLY_BUILD_PYTHON_API) +@@ -71,13 +71,13 @@ if(LIBPOLY_BUILD_PYTHON_API) + # Configure the Python bindings add_subdirectory(python) - # Configure the Python tests - add_subdirectory(test/python) + #add_subdirectory(test/python) - endif() - # Configure the C++ tests - enable_testing() --add_subdirectory(test/polyxx) -+#add_subdirectory(test/polyxx) + if (BUILD_TESTING) + # Configure the C++ tests + enable_testing() + add_subdirectory(test/poly) +- add_subdirectory(test/polyxx) ++ #add_subdirectory(test/polyxx) + endif() diff --git a/math/py-narwhals/Makefile b/math/py-narwhals/Makefile index 3afa162e0cf5..0e7bea008c3a 100644 --- a/math/py-narwhals/Makefile +++ b/math/py-narwhals/Makefile @@ -1,5 +1,5 @@ PORTNAME= narwhals -PORTVERSION= 2.10.2 +PORTVERSION= 2.12.0 CATEGORIES= math python MASTER_SITES= PYPI \ https://github.com/narwhals-dev/narwhals/releases/download/v${PORTVERSION}/ diff --git a/math/py-narwhals/distinfo b/math/py-narwhals/distinfo index 95cdb407d079..d1c65fcfa66b 100644 --- a/math/py-narwhals/distinfo +++ b/math/py-narwhals/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1762586868 -SHA256 (narwhals-2.10.2.tar.gz) = ff738a08bc993cbb792266bec15346c1d85cc68fdfe82a23283c3713f78bd354 -SIZE (narwhals-2.10.2.tar.gz) = 584954 +TIMESTAMP = 1763853418 +SHA256 (narwhals-2.12.0.tar.gz) = 075b6d56f3a222613793e025744b129439ecdff9292ea6615dd983af7ba6ea44 +SIZE (narwhals-2.12.0.tar.gz) = 590404 diff --git a/math/py-ndindex/Makefile b/math/py-ndindex/Makefile index 9d430fe0b40b..a999d47f6c8c 100644 --- a/math/py-ndindex/Makefile +++ b/math/py-ndindex/Makefile @@ -1,5 +1,5 @@ PORTNAME= ndindex -PORTVERSION= 1.10.0 +PORTVERSION= 1.10.1 CATEGORIES= math python MASTER_SITES= PYPI \ https://github.com/Quansight-Labs/ndindex/releases/download/${PORTVERSION}/ diff --git a/math/py-ndindex/distinfo b/math/py-ndindex/distinfo index 0d88beeb05c0..5265a9ceed60 100644 --- a/math/py-ndindex/distinfo +++ b/math/py-ndindex/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1748495833 -SHA256 (ndindex-1.10.0.tar.gz) = 20e3a2f0a8ed4646abf0f13296aab0b5b9cc8c5bc182b71b5945e76eb6f558bb -SIZE (ndindex-1.10.0.tar.gz) = 258688 +TIMESTAMP = 1763853420 +SHA256 (ndindex-1.10.1.tar.gz) = 0f6113c1f031248f8818cbee1aa92aa3c9472b7701debcce9fddebcd2f610f11 +SIZE (ndindex-1.10.1.tar.gz) = 271395 diff --git a/math/py-pandas/Makefile b/math/py-pandas/Makefile index f83bee22da83..44476ac761f2 100644 --- a/math/py-pandas/Makefile +++ b/math/py-pandas/Makefile @@ -1,6 +1,5 @@ PORTNAME= pandas -PORTVERSION= 2.2.3 -PORTREVISION= 3 +PORTVERSION= 2.3.3 PORTEPOCH= 1 CATEGORIES= math devel python MASTER_SITES= PYPI diff --git a/math/py-pandas/distinfo b/math/py-pandas/distinfo index d01f6f1c0848..17254bd19453 100644 --- a/math/py-pandas/distinfo +++ b/math/py-pandas/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1743573899 -SHA256 (pandas-2.2.3.tar.gz) = 4f18ba62b61d7e192368b84517265a99b4d7ee8912f8708660fb4a366cc82667 -SIZE (pandas-2.2.3.tar.gz) = 4399213 +TIMESTAMP = 1761643378 +SHA256 (pandas-2.3.3.tar.gz) = e05e1af93b977f7eafa636d043f9f94c7ee3ac81af99c13508215942e64c993b +SIZE (pandas-2.3.3.tar.gz) = 4495223 diff --git a/math/py-pandas/files/patch-pyproject.toml b/math/py-pandas/files/patch-pyproject.toml index 63506fa05bea..749855e94b58 100644 --- a/math/py-pandas/files/patch-pyproject.toml +++ b/math/py-pandas/files/patch-pyproject.toml @@ -1,20 +1,10 @@ --- pyproject.toml.orig 1970-01-01 00:00:00 UTC +++ pyproject.toml -@@ -2,13 +2,13 @@ requires = [ - # Minimum requirements for the build system to execute. - # See https://github.com/scipy/scipy/pull/12940 for the AIX issue. - requires = [ -- "meson-python==0.13.1", -- "meson==1.2.1", -+ "meson-python>=0.13.1", -+ "meson>=1.2.1", - "wheel", -- "Cython~=3.0.5", # Note: sync with setup.py, environment.yml and asv.conf.json -+ "Cython>=3.0.5", # Note: sync with setup.py, environment.yml and asv.conf.json +@@ -8,7 +8,7 @@ # Force numpy higher than 2.0, so that built wheels are compatible # with both numpy 1 and 2 - "numpy>=2.0", + "numpy", "versioneer[toml]" ] - + diff --git a/math/py-pyreadstat/Makefile b/math/py-pyreadstat/Makefile index 89f5c1217df5..f5bdbba14618 100644 --- a/math/py-pyreadstat/Makefile +++ b/math/py-pyreadstat/Makefile @@ -1,5 +1,5 @@ PORTNAME= pyreadstat -PORTVERSION= 1.3.1 +PORTVERSION= 1.3.2 CATEGORIES= math python MASTER_SITES= PYPI PKGNAMEPREFIX= ${PYTHON_PKGNAMEPREFIX} diff --git a/math/py-pyreadstat/distinfo b/math/py-pyreadstat/distinfo index 6c4da3f3c0f6..dd117626e9e1 100644 --- a/math/py-pyreadstat/distinfo +++ b/math/py-pyreadstat/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1757120790 -SHA256 (pyreadstat-1.3.1.tar.gz) = 5e22b4000570cc0b0b850c7fedc13129546729ca413d67697ede0074423b1ef6 -SIZE (pyreadstat-1.3.1.tar.gz) = 610773 +TIMESTAMP = 1763853422 +SHA256 (pyreadstat-1.3.2.tar.gz) = 4ebb105119e4d4026328cd611e5e582e7456d14057be25070d5ebf7ff730ed78 +SIZE (pyreadstat-1.3.2.tar.gz) = 611876 diff --git a/math/py-spreg/Makefile b/math/py-spreg/Makefile index 0ddac6656e38..77c0be86a4a9 100644 --- a/math/py-spreg/Makefile +++ b/math/py-spreg/Makefile @@ -1,5 +1,5 @@ PORTNAME= spreg -PORTVERSION= 1.8.3 +PORTVERSION= 1.8.4 CATEGORIES= math python MASTER_SITES= PYPI PKGNAMEPREFIX= ${PYTHON_PKGNAMEPREFIX} diff --git a/math/py-spreg/distinfo b/math/py-spreg/distinfo index 35b75d796693..5e6adf165e32 100644 --- a/math/py-spreg/distinfo +++ b/math/py-spreg/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1748107938 -SHA256 (spreg-1.8.3.tar.gz) = ef162161baf6aafd247233f68c479da777c4a3a360d6f768dae292bde3294131 -SIZE (spreg-1.8.3.tar.gz) = 601179 +TIMESTAMP = 1763853424 +SHA256 (spreg-1.8.4.tar.gz) = 4aaef8a99396a230febc06f1a32e095e47a0f95106dd6093cc4776eca6ff0b07 +SIZE (spreg-1.8.4.tar.gz) = 607948 diff --git a/math/zimpl/Makefile b/math/zimpl/Makefile index 7c58ccd87854..54d113377bcc 100644 --- a/math/zimpl/Makefile +++ b/math/zimpl/Makefile @@ -1,5 +1,6 @@ PORTNAME= zimpl -DISTVERSION= 3.6.2 +DISTVERSIONPREFIX= v +DISTVERSION= 3.7.0 CATEGORIES= math MAINTAINER= yuri@FreeBSD.org @@ -21,7 +22,6 @@ USE_LDCONFIG= yes USE_GITHUB= yes GH_ACCOUNT= scipopt -GH_TAGNAME= v${DISTVERSION:S/.//g} CMAKE_ON= BUILD_SHARED_LIBS diff --git a/math/zimpl/distinfo b/math/zimpl/distinfo index d332293e6908..a2a8ca96a292 100644 --- a/math/zimpl/distinfo +++ b/math/zimpl/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1731123417 -SHA256 (scipopt-zimpl-3.6.2-v362_GH0.tar.gz) = d99bdfa227d8871560b92dd90026280b185ce8f28b0d3fe295b871f0eca8d4f1 -SIZE (scipopt-zimpl-3.6.2-v362_GH0.tar.gz) = 5257233 +TIMESTAMP = 1764037777 +SHA256 (scipopt-zimpl-v3.7.0_GH0.tar.gz) = a95771124823fd8ea38310a50314359041ba58e5812a105e3fa9a2e33d5cc18f +SIZE (scipopt-zimpl-v3.7.0_GH0.tar.gz) = 5275073 |