Date: Sun, 14 Jan 2024 03:50:22 GMT From: Yuri Victorovich <yuri@FreeBSD.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org Subject: git: 27b9012337ee - main - math/lean4: New port: Theorem prover and functional language for math (new gen) Message-ID: <202401140350.40E3oMx4022382@gitrepo.freebsd.org>
next in thread | raw e-mail | index | archive | help
The branch main has been updated by yuri: URL: https://cgit.FreeBSD.org/ports/commit/?id=27b9012337ee58a0ecc220dfd079cc2189dc99e2 commit 27b9012337ee58a0ecc220dfd079cc2189dc99e2 Author: Yuri Victorovich <yuri@FreeBSD.org> AuthorDate: 2024-01-14 03:49:56 +0000 Commit: Yuri Victorovich <yuri@FreeBSD.org> CommitDate: 2024-01-14 03:50:20 +0000 math/lean4: New port: Theorem prover and functional language for math (new gen) --- math/Makefile | 1 + math/lean4/Makefile | 40 + math/lean4/distinfo | 3 + math/lean4/files/patch-src_CMakeLists.txt | 23 + math/lean4/files/patch-src_runtime_io.cpp | 17 + .../files/patch-src_runtime_stack__overflow.cpp | 12 + math/lean4/files/patch-stage0_src_CMakeLists.txt | 23 + math/lean4/files/patch-stage0_src_runtime_io.cpp | 16 + .../patch-stage0_src_runtime_stack__overflow.cpp | 21 + math/lean4/pkg-descr | 6 + math/lean4/pkg-message | 22 + math/lean4/pkg-plist | 2259 ++++++++++++++++++++ 12 files changed, 2443 insertions(+) diff --git a/math/Makefile b/math/Makefile index 345406ce012f..a933bb237101 100644 --- a/math/Makefile +++ b/math/Makefile @@ -436,6 +436,7 @@ SUBDIR += lcalc SUBDIR += ldouble SUBDIR += lean + SUBDIR += lean4 SUBDIR += lemon SUBDIR += levmar SUBDIR += lib2geom diff --git a/math/lean4/Makefile b/math/lean4/Makefile new file mode 100644 index 000000000000..a43194860970 --- /dev/null +++ b/math/lean4/Makefile @@ -0,0 +1,40 @@ +PORTNAME= lean4 +DISTVERSIONPREFIX= v +DISTVERSION= 4.5.0-rc1 +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 +COMMENT= Theorem prover and functional language for math (new gen) +WWW= https://lean-lang.org/ + +LICENSE= APACHE20 +LICENSE_FILE= ${WRKSRC}/LICENSE + +BUILD_DEPENDS= bash:shells/bash +LIB_DEPENDS= libgmp.so:math/gmp + +USES= cmake:noninja,testing compiler:c++14-lang gmake python:build # ninja fails + gmake scripts are included in the project + +USE_GITHUB= yes +GH_ACCOUNT= leanprover + +CFLAGS+= -fPIC +CXXFLAGS+= -fPIC + +BINARY_ALIAS= make=${GMAKE} python=${PYTHON_CMD} + +post-install: + # remove empty dirs + @${FIND} ${STAGEDIR}${DATADIR} -type d -empty -delete + # remove stray files + @${RM} ${STAGEDIR}${PREFIX}/LICENSE* + # strip binaries + @cd ${STAGEDIR}${PREFIX} && ${STRIP_CMD} \ + bin/lake \ + bin/lean \ + bin/leanc \ + lib/lean/libleanshared.so + +# 6 tests are known to fail due to bugs in the testcase code, see https://github.com/leanprover/lean4/issues/3179 + +.include <bsd.port.mk> diff --git a/math/lean4/distinfo b/math/lean4/distinfo new file mode 100644 index 000000000000..d307f90be676 --- /dev/null +++ b/math/lean4/distinfo @@ -0,0 +1,3 @@ +TIMESTAMP = 1705134061 +SHA256 (leanprover-lean4-v4.5.0-rc1_GH0.tar.gz) = 8b5ae344816670adb2a68859b2f4c309592feb32674d477e46e061275f9e8129 +SIZE (leanprover-lean4-v4.5.0-rc1_GH0.tar.gz) = 17060956 diff --git a/math/lean4/files/patch-src_CMakeLists.txt b/math/lean4/files/patch-src_CMakeLists.txt new file mode 100644 index 000000000000..6109d2793eac --- /dev/null +++ b/math/lean4/files/patch-src_CMakeLists.txt @@ -0,0 +1,23 @@ +--- src/CMakeLists.txt.orig 2023-12-21 22:11:33 UTC ++++ src/CMakeLists.txt +@@ -352,6 +352,11 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") + string(APPEND LEANC_EXTRA_FLAGS " -fPIC") + string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") + string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean") ++elseif(${CMAKE_SYSTEM_NAME} MATCHES "FreeBSD") ++ string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec") ++ string(APPEND LEANC_EXTRA_FLAGS " -fPIC") ++ string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") ++ string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean") + elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") + string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec") + string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib") +@@ -592,7 +597,7 @@ endif() + file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC) + endif() + +-install(DIRECTORY "${CMAKE_SOURCE_DIR}/" DESTINATION src/lean ++install(DIRECTORY "${CMAKE_SOURCE_DIR}/" DESTINATION share/lean4/src/lean + FILES_MATCHING + PATTERN "*.lean" + PATTERN "*.md" diff --git a/math/lean4/files/patch-src_runtime_io.cpp b/math/lean4/files/patch-src_runtime_io.cpp new file mode 100644 index 000000000000..767ad0a1625f --- /dev/null +++ b/math/lean4/files/patch-src_runtime_io.cpp @@ -0,0 +1,17 @@ +--- src/runtime/io.cpp.orig 2024-01-13 17:13:25 UTC ++++ src/runtime/io.cpp +@@ -855,7 +855,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); ++#elif defined(__FreeBSD__) ++ snprintf(path, PATH_MAX, "/proc/%d/file", pid); ++#else ++# error "Unknown platform" ++#endif + if (readlink(path, dest, PATH_MAX) == -1) { + return io_result_mk_error("failed to locate application"); + } else { diff --git a/math/lean4/files/patch-src_runtime_stack__overflow.cpp b/math/lean4/files/patch-src_runtime_stack__overflow.cpp new file mode 100644 index 000000000000..06914304dbaa --- /dev/null +++ b/math/lean4/files/patch-src_runtime_stack__overflow.cpp @@ -0,0 +1,12 @@ +--- src/runtime/stack_overflow.cpp.orig 2023-12-21 22:11:33 UTC ++++ src/runtime/stack_overflow.cpp +@@ -20,6 +20,9 @@ Port of the corresponding Rust code (see links below). + #include <lean/lean.h> + #include "runtime/stack_overflow.h" + ++#include <pthread_np.h> ++#define pthread_getattr_np pthread_attr_get_np ++ + namespace lean { + // stack guard of the main thread + static stack_guard * g_stack_guard; diff --git a/math/lean4/files/patch-stage0_src_CMakeLists.txt b/math/lean4/files/patch-stage0_src_CMakeLists.txt new file mode 100644 index 000000000000..e8af91b549aa --- /dev/null +++ b/math/lean4/files/patch-stage0_src_CMakeLists.txt @@ -0,0 +1,23 @@ +--- stage0/src/CMakeLists.txt.orig 2023-12-21 22:11:33 UTC ++++ stage0/src/CMakeLists.txt +@@ -352,6 +352,11 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") + string(APPEND LEANC_EXTRA_FLAGS " -fPIC") + string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") + string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean") ++elseif(${CMAKE_SYSTEM_NAME} MATCHES "FreeBSD") ++ string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec") ++ string(APPEND LEANC_EXTRA_FLAGS " -fPIC") ++ string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") ++ string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean") + elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") + string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec") + string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib") +@@ -592,7 +597,7 @@ endif() + file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC) + endif() + +-install(DIRECTORY "${CMAKE_SOURCE_DIR}/" DESTINATION src/lean ++install(DIRECTORY "${CMAKE_SOURCE_DIR}/" DESTINATION share/lean4/src/lean + FILES_MATCHING + PATTERN "*.lean" + PATTERN "*.md" diff --git a/math/lean4/files/patch-stage0_src_runtime_io.cpp b/math/lean4/files/patch-stage0_src_runtime_io.cpp new file mode 100644 index 000000000000..67d799f2a916 --- /dev/null +++ b/math/lean4/files/patch-stage0_src_runtime_io.cpp @@ -0,0 +1,16 @@ +--- stage0/src/runtime/io.cpp.orig 2024-01-13 09:36:50 UTC ++++ stage0/src/runtime/io.cpp +@@ -855,7 +855,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(); ++#if defined(__linux__) + snprintf(path, PATH_MAX, "/proc/%d/exe", pid); ++#elif defined(__FreeBSD__) ++ snprintf(path, PATH_MAX, "/proc/%d/file", pid); ++#else ++# error "Unknown platform" ++#endif + if (readlink(path, dest, PATH_MAX) == -1) { + return io_result_mk_error("failed to locate application"); + } else { diff --git a/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp b/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp new file mode 100644 index 000000000000..5296c0cf49c2 --- /dev/null +++ b/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp @@ -0,0 +1,21 @@ +--- stage0/src/runtime/stack_overflow.cpp.orig 2023-12-21 22:11:33 UTC ++++ stage0/src/runtime/stack_overflow.cpp +@@ -7,6 +7,10 @@ Port of the corresponding Rust code (see links below). + Print a nicer error message on stack overflow. + Port of the corresponding Rust code (see links below). + */ ++ ++#include <pthread_np.h> ++#define pthread_getattr_np pthread_attr_get_np ++ + #ifdef LEAN_WINDOWS + #include <windows.h> + #else +@@ -19,6 +23,7 @@ Port of the corresponding Rust code (see links below). + #include <cstring> + #include <lean/lean.h> + #include "runtime/stack_overflow.h" ++ + + namespace lean { + // stack guard of the main thread diff --git a/math/lean4/pkg-descr b/math/lean4/pkg-descr new file mode 100644 index 000000000000..d549a156950f --- /dev/null +++ b/math/lean4/pkg-descr @@ -0,0 +1,6 @@ +Lean is an open source theorem prover and programming language being developed +at Microsoft Research. Lean aims to bridge the gap between interactive and +automated theorem proving, by situating automated tools and methods in a +framework that supports user interaction and the construction of fully specified +axiomatic proofs. The mathematical components library mathlib for Lean is being +developed at Carnegie Mellon University. diff --git a/math/lean4/pkg-message b/math/lean4/pkg-message new file mode 100644 index 000000000000..e0c1a26dc720 --- /dev/null +++ b/math/lean4/pkg-message @@ -0,0 +1,22 @@ +[ +{ type: install + message: <<EOM +================================================================================ +You installed Lean: The Theorem Prover. + +(1) Please note that Lean requires /proc to be mounted. + + The usual way to do this is to add this line to /etc/fstab: + proc /proc procfs rw 0 0 + + and then run this command as root: + # mount /proc + +(2) You might also want to install mathlibtools (math/mathlibtools) in case + you need to use the mathematical library of Lean. + mathlibtools download this library to user's home directory for further + use by Lean. +================================================================================ +EOM +} +] diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist new file mode 100644 index 000000000000..516a35d47fdb --- /dev/null +++ b/math/lean4/pkg-plist @@ -0,0 +1,2259 @@ +bin/lake +bin/lean +bin/leanc +bin/leanmake +include/lean/config.h +include/lean/lean.h +include/lean/lean_gmp.h +include/lean/version.h +lib/lean/Init.ilean +lib/lean/Init.olean +lib/lean/Init/Classical.ilean +lib/lean/Init/Classical.olean +lib/lean/Init/Coe.ilean +lib/lean/Init/Coe.olean +lib/lean/Init/Control.ilean +lib/lean/Init/Control.olean +lib/lean/Init/Control/Basic.ilean +lib/lean/Init/Control/Basic.olean +lib/lean/Init/Control/EState.ilean +lib/lean/Init/Control/EState.olean +lib/lean/Init/Control/Except.ilean +lib/lean/Init/Control/Except.olean +lib/lean/Init/Control/ExceptCps.ilean +lib/lean/Init/Control/ExceptCps.olean +lib/lean/Init/Control/Id.ilean +lib/lean/Init/Control/Id.olean +lib/lean/Init/Control/Lawful.ilean +lib/lean/Init/Control/Lawful.olean +lib/lean/Init/Control/Option.ilean +lib/lean/Init/Control/Option.olean +lib/lean/Init/Control/Reader.ilean +lib/lean/Init/Control/Reader.olean +lib/lean/Init/Control/State.ilean +lib/lean/Init/Control/State.olean +lib/lean/Init/Control/StateCps.ilean +lib/lean/Init/Control/StateCps.olean +lib/lean/Init/Control/StateRef.ilean +lib/lean/Init/Control/StateRef.olean +lib/lean/Init/Conv.ilean +lib/lean/Init/Conv.olean +lib/lean/Init/Core.ilean +lib/lean/Init/Core.olean +lib/lean/Init/Data.ilean +lib/lean/Init/Data.olean +lib/lean/Init/Data/AC.ilean +lib/lean/Init/Data/AC.olean +lib/lean/Init/Data/Array.ilean +lib/lean/Init/Data/Array.olean +lib/lean/Init/Data/Array/Basic.ilean +lib/lean/Init/Data/Array/Basic.olean +lib/lean/Init/Data/Array/BasicAux.ilean +lib/lean/Init/Data/Array/BasicAux.olean +lib/lean/Init/Data/Array/BinSearch.ilean +lib/lean/Init/Data/Array/BinSearch.olean +lib/lean/Init/Data/Array/DecidableEq.ilean +lib/lean/Init/Data/Array/DecidableEq.olean +lib/lean/Init/Data/Array/InsertionSort.ilean +lib/lean/Init/Data/Array/InsertionSort.olean +lib/lean/Init/Data/Array/Mem.ilean +lib/lean/Init/Data/Array/Mem.olean +lib/lean/Init/Data/Array/QSort.ilean +lib/lean/Init/Data/Array/QSort.olean +lib/lean/Init/Data/Array/Subarray.ilean +lib/lean/Init/Data/Array/Subarray.olean +lib/lean/Init/Data/Basic.ilean +lib/lean/Init/Data/Basic.olean +lib/lean/Init/Data/ByteArray.ilean +lib/lean/Init/Data/ByteArray.olean +lib/lean/Init/Data/ByteArray/Basic.ilean +lib/lean/Init/Data/ByteArray/Basic.olean +lib/lean/Init/Data/Channel.ilean +lib/lean/Init/Data/Channel.olean +lib/lean/Init/Data/Char.ilean +lib/lean/Init/Data/Char.olean +lib/lean/Init/Data/Char/Basic.ilean +lib/lean/Init/Data/Char/Basic.olean +lib/lean/Init/Data/Fin.ilean +lib/lean/Init/Data/Fin.olean +lib/lean/Init/Data/Fin/Basic.ilean +lib/lean/Init/Data/Fin/Basic.olean +lib/lean/Init/Data/Fin/Log2.ilean +lib/lean/Init/Data/Fin/Log2.olean +lib/lean/Init/Data/Float.ilean +lib/lean/Init/Data/Float.olean +lib/lean/Init/Data/FloatArray.ilean +lib/lean/Init/Data/FloatArray.olean +lib/lean/Init/Data/FloatArray/Basic.ilean +lib/lean/Init/Data/FloatArray/Basic.olean +lib/lean/Init/Data/Format.ilean +lib/lean/Init/Data/Format.olean +lib/lean/Init/Data/Format/Basic.ilean +lib/lean/Init/Data/Format/Basic.olean +lib/lean/Init/Data/Format/Instances.ilean +lib/lean/Init/Data/Format/Instances.olean +lib/lean/Init/Data/Format/Macro.ilean +lib/lean/Init/Data/Format/Macro.olean +lib/lean/Init/Data/Format/Syntax.ilean +lib/lean/Init/Data/Format/Syntax.olean +lib/lean/Init/Data/Hashable.ilean +lib/lean/Init/Data/Hashable.olean +lib/lean/Init/Data/Int.ilean +lib/lean/Init/Data/Int.olean +lib/lean/Init/Data/Int/Basic.ilean +lib/lean/Init/Data/Int/Basic.olean +lib/lean/Init/Data/List.ilean +lib/lean/Init/Data/List.olean +lib/lean/Init/Data/List/Basic.ilean +lib/lean/Init/Data/List/Basic.olean +lib/lean/Init/Data/List/BasicAux.ilean +lib/lean/Init/Data/List/BasicAux.olean +lib/lean/Init/Data/List/Control.ilean +lib/lean/Init/Data/List/Control.olean +lib/lean/Init/Data/Nat.ilean +lib/lean/Init/Data/Nat.olean +lib/lean/Init/Data/Nat/Basic.ilean +lib/lean/Init/Data/Nat/Basic.olean +lib/lean/Init/Data/Nat/Bitwise.ilean +lib/lean/Init/Data/Nat/Bitwise.olean +lib/lean/Init/Data/Nat/Control.ilean +lib/lean/Init/Data/Nat/Control.olean +lib/lean/Init/Data/Nat/Div.ilean +lib/lean/Init/Data/Nat/Div.olean +lib/lean/Init/Data/Nat/Gcd.ilean +lib/lean/Init/Data/Nat/Gcd.olean +lib/lean/Init/Data/Nat/Linear.ilean +lib/lean/Init/Data/Nat/Linear.olean +lib/lean/Init/Data/Nat/Log2.ilean +lib/lean/Init/Data/Nat/Log2.olean +lib/lean/Init/Data/Nat/Power2.ilean +lib/lean/Init/Data/Nat/Power2.olean +lib/lean/Init/Data/Nat/SOM.ilean +lib/lean/Init/Data/Nat/SOM.olean +lib/lean/Init/Data/OfScientific.ilean +lib/lean/Init/Data/OfScientific.olean +lib/lean/Init/Data/Option.ilean +lib/lean/Init/Data/Option.olean +lib/lean/Init/Data/Option/Basic.ilean +lib/lean/Init/Data/Option/Basic.olean +lib/lean/Init/Data/Option/BasicAux.ilean +lib/lean/Init/Data/Option/BasicAux.olean +lib/lean/Init/Data/Option/Instances.ilean +lib/lean/Init/Data/Option/Instances.olean +lib/lean/Init/Data/Ord.ilean +lib/lean/Init/Data/Ord.olean +lib/lean/Init/Data/Prod.ilean +lib/lean/Init/Data/Prod.olean +lib/lean/Init/Data/Queue.ilean +lib/lean/Init/Data/Queue.olean +lib/lean/Init/Data/Random.ilean +lib/lean/Init/Data/Random.olean +lib/lean/Init/Data/Range.ilean +lib/lean/Init/Data/Range.olean +lib/lean/Init/Data/Repr.ilean +lib/lean/Init/Data/Repr.olean +lib/lean/Init/Data/Stream.ilean +lib/lean/Init/Data/Stream.olean +lib/lean/Init/Data/String.ilean +lib/lean/Init/Data/String.olean +lib/lean/Init/Data/String/Basic.ilean +lib/lean/Init/Data/String/Basic.olean +lib/lean/Init/Data/String/Extra.ilean +lib/lean/Init/Data/String/Extra.olean +lib/lean/Init/Data/ToString.ilean +lib/lean/Init/Data/ToString.olean +lib/lean/Init/Data/ToString/Basic.ilean +lib/lean/Init/Data/ToString/Basic.olean +lib/lean/Init/Data/ToString/Macro.ilean +lib/lean/Init/Data/ToString/Macro.olean +lib/lean/Init/Data/UInt.ilean +lib/lean/Init/Data/UInt.olean +lib/lean/Init/Data/UInt/Basic.ilean +lib/lean/Init/Data/UInt/Basic.olean +lib/lean/Init/Data/UInt/Log2.ilean +lib/lean/Init/Data/UInt/Log2.olean +lib/lean/Init/Dynamic.ilean +lib/lean/Init/Dynamic.olean +lib/lean/Init/Hints.ilean +lib/lean/Init/Hints.olean +lib/lean/Init/Meta.ilean +lib/lean/Init/Meta.olean +lib/lean/Init/MetaTypes.ilean +lib/lean/Init/MetaTypes.olean +lib/lean/Init/Notation.ilean +lib/lean/Init/Notation.olean +lib/lean/Init/NotationExtra.ilean +lib/lean/Init/NotationExtra.olean +lib/lean/Init/Prelude.ilean +lib/lean/Init/Prelude.olean +lib/lean/Init/ShareCommon.ilean +lib/lean/Init/ShareCommon.olean +lib/lean/Init/SimpLemmas.ilean +lib/lean/Init/SimpLemmas.olean +lib/lean/Init/SizeOf.ilean +lib/lean/Init/SizeOf.olean +lib/lean/Init/SizeOfLemmas.ilean +lib/lean/Init/SizeOfLemmas.olean +lib/lean/Init/System.ilean +lib/lean/Init/System.olean +lib/lean/Init/System/FilePath.ilean +lib/lean/Init/System/FilePath.olean +lib/lean/Init/System/IO.ilean +lib/lean/Init/System/IO.olean +lib/lean/Init/System/IOError.ilean +lib/lean/Init/System/IOError.olean +lib/lean/Init/System/Mutex.ilean +lib/lean/Init/System/Mutex.olean +lib/lean/Init/System/Platform.ilean +lib/lean/Init/System/Platform.olean +lib/lean/Init/System/Promise.ilean +lib/lean/Init/System/Promise.olean +lib/lean/Init/System/ST.ilean +lib/lean/Init/System/ST.olean +lib/lean/Init/System/Uri.ilean +lib/lean/Init/System/Uri.olean +lib/lean/Init/Tactics.ilean +lib/lean/Init/Tactics.olean +lib/lean/Init/Util.ilean +lib/lean/Init/Util.olean +lib/lean/Init/WF.ilean +lib/lean/Init/WF.olean +lib/lean/Init/WFTactics.ilean +lib/lean/Init/WFTactics.olean +lib/lean/Lake.ilean +lib/lean/Lake.olean +lib/lean/Lake/Build.ilean +lib/lean/Lake/Build.olean +lib/lean/Lake/Build/Actions.ilean +lib/lean/Lake/Build/Actions.olean +lib/lean/Lake/Build/Common.ilean +lib/lean/Lake/Build/Common.olean +lib/lean/Lake/Build/Context.ilean +lib/lean/Lake/Build/Context.olean +lib/lean/Lake/Build/Data.ilean +lib/lean/Lake/Build/Data.olean +lib/lean/Lake/Build/Executable.ilean +lib/lean/Lake/Build/Executable.olean +lib/lean/Lake/Build/Facets.ilean +lib/lean/Lake/Build/Facets.olean +lib/lean/Lake/Build/Imports.ilean +lib/lean/Lake/Build/Imports.olean +lib/lean/Lake/Build/Index.ilean +lib/lean/Lake/Build/Index.olean +lib/lean/Lake/Build/Info.ilean +lib/lean/Lake/Build/Info.olean +lib/lean/Lake/Build/Job.ilean +lib/lean/Lake/Build/Job.olean +lib/lean/Lake/Build/Key.ilean +lib/lean/Lake/Build/Key.olean +lib/lean/Lake/Build/Library.ilean +lib/lean/Lake/Build/Library.olean +lib/lean/Lake/Build/Module.ilean +lib/lean/Lake/Build/Module.olean +lib/lean/Lake/Build/Monad.ilean +lib/lean/Lake/Build/Monad.olean +lib/lean/Lake/Build/Package.ilean +lib/lean/Lake/Build/Package.olean +lib/lean/Lake/Build/Store.ilean +lib/lean/Lake/Build/Store.olean +lib/lean/Lake/Build/Targets.ilean +lib/lean/Lake/Build/Targets.olean +lib/lean/Lake/Build/Topological.ilean +lib/lean/Lake/Build/Topological.olean +lib/lean/Lake/Build/Trace.ilean +lib/lean/Lake/Build/Trace.olean +lib/lean/Lake/CLI.ilean +lib/lean/Lake/CLI.olean +lib/lean/Lake/CLI/Actions.ilean +lib/lean/Lake/CLI/Actions.olean +lib/lean/Lake/CLI/Build.ilean +lib/lean/Lake/CLI/Build.olean +lib/lean/Lake/CLI/Error.ilean +lib/lean/Lake/CLI/Error.olean +lib/lean/Lake/CLI/Help.ilean +lib/lean/Lake/CLI/Help.olean +lib/lean/Lake/CLI/Init.ilean +lib/lean/Lake/CLI/Init.olean +lib/lean/Lake/CLI/Main.ilean +lib/lean/Lake/CLI/Main.olean +lib/lean/Lake/CLI/Serve.ilean +lib/lean/Lake/CLI/Serve.olean +lib/lean/Lake/Config.ilean +lib/lean/Lake/Config.olean +lib/lean/Lake/Config/Context.ilean +lib/lean/Lake/Config/Context.olean +lib/lean/Lake/Config/Dependency.ilean +lib/lean/Lake/Config/Dependency.olean +lib/lean/Lake/Config/Env.ilean +lib/lean/Lake/Config/Env.olean +lib/lean/Lake/Config/ExternLib.ilean +lib/lean/Lake/Config/ExternLib.olean +lib/lean/Lake/Config/ExternLibConfig.ilean +lib/lean/Lake/Config/ExternLibConfig.olean +lib/lean/Lake/Config/FacetConfig.ilean +lib/lean/Lake/Config/FacetConfig.olean +lib/lean/Lake/Config/Glob.ilean +lib/lean/Lake/Config/Glob.olean +lib/lean/Lake/Config/InstallPath.ilean +lib/lean/Lake/Config/InstallPath.olean +lib/lean/Lake/Config/LeanConfig.ilean +lib/lean/Lake/Config/LeanConfig.olean +lib/lean/Lake/Config/LeanExe.ilean +lib/lean/Lake/Config/LeanExe.olean +lib/lean/Lake/Config/LeanExeConfig.ilean +lib/lean/Lake/Config/LeanExeConfig.olean +lib/lean/Lake/Config/LeanLib.ilean +lib/lean/Lake/Config/LeanLib.olean +lib/lean/Lake/Config/LeanLibConfig.ilean +lib/lean/Lake/Config/LeanLibConfig.olean +lib/lean/Lake/Config/Module.ilean +lib/lean/Lake/Config/Module.olean +lib/lean/Lake/Config/Monad.ilean +lib/lean/Lake/Config/Monad.olean +lib/lean/Lake/Config/Opaque.ilean +lib/lean/Lake/Config/Opaque.olean +lib/lean/Lake/Config/Package.ilean +lib/lean/Lake/Config/Package.olean +lib/lean/Lake/Config/Script.ilean +lib/lean/Lake/Config/Script.olean +lib/lean/Lake/Config/TargetConfig.ilean +lib/lean/Lake/Config/TargetConfig.olean +lib/lean/Lake/Config/Workspace.ilean +lib/lean/Lake/Config/Workspace.olean +lib/lean/Lake/Config/WorkspaceConfig.ilean +lib/lean/Lake/Config/WorkspaceConfig.olean +lib/lean/Lake/DSL.ilean +lib/lean/Lake/DSL.olean +lib/lean/Lake/DSL/Attributes.ilean +lib/lean/Lake/DSL/Attributes.olean +lib/lean/Lake/DSL/Config.ilean +lib/lean/Lake/DSL/Config.olean +lib/lean/Lake/DSL/DeclUtil.ilean +lib/lean/Lake/DSL/DeclUtil.olean +lib/lean/Lake/DSL/Extensions.ilean +lib/lean/Lake/DSL/Extensions.olean +lib/lean/Lake/DSL/Meta.ilean +lib/lean/Lake/DSL/Meta.olean +lib/lean/Lake/DSL/Package.ilean +lib/lean/Lake/DSL/Package.olean +lib/lean/Lake/DSL/Require.ilean +lib/lean/Lake/DSL/Require.olean +lib/lean/Lake/DSL/Script.ilean +lib/lean/Lake/DSL/Script.olean +lib/lean/Lake/DSL/Targets.ilean +lib/lean/Lake/DSL/Targets.olean +lib/lean/Lake/Load.ilean +lib/lean/Lake/Load.olean +lib/lean/Lake/Load/Config.ilean +lib/lean/Lake/Load/Config.olean +lib/lean/Lake/Load/Elab.ilean +lib/lean/Lake/Load/Elab.olean +lib/lean/Lake/Load/Main.ilean +lib/lean/Lake/Load/Main.olean +lib/lean/Lake/Load/Manifest.ilean +lib/lean/Lake/Load/Manifest.olean +lib/lean/Lake/Load/Materialize.ilean +lib/lean/Lake/Load/Materialize.olean +lib/lean/Lake/Load/Package.ilean +lib/lean/Lake/Load/Package.olean +lib/lean/Lake/Main.ilean +lib/lean/Lake/Main.olean +lib/lean/Lake/Util/Async.ilean +lib/lean/Lake/Util/Async.olean +lib/lean/Lake/Util/Binder.ilean +lib/lean/Lake/Util/Binder.olean +lib/lean/Lake/Util/Casing.ilean +lib/lean/Lake/Util/Casing.olean +lib/lean/Lake/Util/Cli.ilean +lib/lean/Lake/Util/Cli.olean +lib/lean/Lake/Util/Compare.ilean +lib/lean/Lake/Util/Compare.olean +lib/lean/Lake/Util/Cycle.ilean +lib/lean/Lake/Util/Cycle.olean +lib/lean/Lake/Util/DRBMap.ilean +lib/lean/Lake/Util/DRBMap.olean +lib/lean/Lake/Util/EStateT.ilean +lib/lean/Lake/Util/EStateT.olean +lib/lean/Lake/Util/EquipT.ilean +lib/lean/Lake/Util/EquipT.olean +lib/lean/Lake/Util/Error.ilean +lib/lean/Lake/Util/Error.olean +lib/lean/Lake/Util/Exit.ilean +lib/lean/Lake/Util/Exit.olean +lib/lean/Lake/Util/Family.ilean +lib/lean/Lake/Util/Family.olean +lib/lean/Lake/Util/Git.ilean +lib/lean/Lake/Util/Git.olean +lib/lean/Lake/Util/Lift.ilean +lib/lean/Lake/Util/Lift.olean +lib/lean/Lake/Util/List.ilean +lib/lean/Lake/Util/List.olean +lib/lean/Lake/Util/Log.ilean +lib/lean/Lake/Util/Log.olean +lib/lean/Lake/Util/MainM.ilean +lib/lean/Lake/Util/MainM.olean +lib/lean/Lake/Util/Name.ilean +lib/lean/Lake/Util/Name.olean +lib/lean/Lake/Util/NativeLib.ilean +lib/lean/Lake/Util/NativeLib.olean +lib/lean/Lake/Util/Opaque.ilean +lib/lean/Lake/Util/Opaque.olean +lib/lean/Lake/Util/OptionIO.ilean +lib/lean/Lake/Util/OptionIO.olean +lib/lean/Lake/Util/OrdHashSet.ilean +lib/lean/Lake/Util/OrdHashSet.olean +lib/lean/Lake/Util/OrderedTagAttribute.ilean +lib/lean/Lake/Util/OrderedTagAttribute.olean +lib/lean/Lake/Util/Platform.ilean +lib/lean/Lake/Util/Platform.olean +lib/lean/Lake/Util/Proc.ilean +lib/lean/Lake/Util/Proc.olean +lib/lean/Lake/Util/RBArray.ilean +lib/lean/Lake/Util/RBArray.olean +lib/lean/Lake/Util/Store.ilean +lib/lean/Lake/Util/Store.olean +lib/lean/Lake/Util/StoreInsts.ilean +lib/lean/Lake/Util/StoreInsts.olean +lib/lean/Lake/Util/Sugar.ilean +lib/lean/Lake/Util/Sugar.olean +lib/lean/Lake/Util/Task.ilean +lib/lean/Lake/Util/Task.olean +lib/lean/Lake/Version.ilean +lib/lean/Lake/Version.olean +lib/lean/Lean.ilean +lib/lean/Lean.olean +lib/lean/Lean/Attributes.ilean +lib/lean/Lean/Attributes.olean +lib/lean/Lean/AuxRecursor.ilean +lib/lean/Lean/AuxRecursor.olean +lib/lean/Lean/Class.ilean +lib/lean/Lean/Class.olean +lib/lean/Lean/Compiler.ilean +lib/lean/Lean/Compiler.olean +lib/lean/Lean/Compiler/AtMostOnce.ilean +lib/lean/Lean/Compiler/AtMostOnce.olean +lib/lean/Lean/Compiler/BorrowedAnnotation.ilean +lib/lean/Lean/Compiler/BorrowedAnnotation.olean +lib/lean/Lean/Compiler/CSimpAttr.ilean +lib/lean/Lean/Compiler/CSimpAttr.olean +lib/lean/Lean/Compiler/ClosedTermCache.ilean +lib/lean/Lean/Compiler/ClosedTermCache.olean +lib/lean/Lean/Compiler/ConstFolding.ilean +lib/lean/Lean/Compiler/ConstFolding.olean +lib/lean/Lean/Compiler/ExportAttr.ilean +lib/lean/Lean/Compiler/ExportAttr.olean +lib/lean/Lean/Compiler/ExternAttr.ilean +lib/lean/Lean/Compiler/ExternAttr.olean +lib/lean/Lean/Compiler/FFI.ilean +lib/lean/Lean/Compiler/FFI.olean +lib/lean/Lean/Compiler/IR.ilean +lib/lean/Lean/Compiler/IR.olean +lib/lean/Lean/Compiler/IR/Basic.ilean +lib/lean/Lean/Compiler/IR/Basic.olean +lib/lean/Lean/Compiler/IR/Borrow.ilean +lib/lean/Lean/Compiler/IR/Borrow.olean +lib/lean/Lean/Compiler/IR/Boxing.ilean +lib/lean/Lean/Compiler/IR/Boxing.olean +lib/lean/Lean/Compiler/IR/Checker.ilean +lib/lean/Lean/Compiler/IR/Checker.olean +lib/lean/Lean/Compiler/IR/CompilerM.ilean +lib/lean/Lean/Compiler/IR/CompilerM.olean +lib/lean/Lean/Compiler/IR/CtorLayout.ilean +lib/lean/Lean/Compiler/IR/CtorLayout.olean +lib/lean/Lean/Compiler/IR/ElimDeadBranches.ilean +lib/lean/Lean/Compiler/IR/ElimDeadBranches.olean +lib/lean/Lean/Compiler/IR/ElimDeadVars.ilean +lib/lean/Lean/Compiler/IR/ElimDeadVars.olean +lib/lean/Lean/Compiler/IR/EmitC.ilean +lib/lean/Lean/Compiler/IR/EmitC.olean +lib/lean/Lean/Compiler/IR/EmitLLVM.ilean +lib/lean/Lean/Compiler/IR/EmitLLVM.olean +lib/lean/Lean/Compiler/IR/EmitUtil.ilean +lib/lean/Lean/Compiler/IR/EmitUtil.olean +lib/lean/Lean/Compiler/IR/ExpandResetReuse.ilean +lib/lean/Lean/Compiler/IR/ExpandResetReuse.olean +lib/lean/Lean/Compiler/IR/Format.ilean +lib/lean/Lean/Compiler/IR/Format.olean +lib/lean/Lean/Compiler/IR/FreeVars.ilean +lib/lean/Lean/Compiler/IR/FreeVars.olean +lib/lean/Lean/Compiler/IR/LLVMBindings.ilean +lib/lean/Lean/Compiler/IR/LLVMBindings.olean +lib/lean/Lean/Compiler/IR/LiveVars.ilean +lib/lean/Lean/Compiler/IR/LiveVars.olean +lib/lean/Lean/Compiler/IR/NormIds.ilean +lib/lean/Lean/Compiler/IR/NormIds.olean +lib/lean/Lean/Compiler/IR/PushProj.ilean +lib/lean/Lean/Compiler/IR/PushProj.olean +lib/lean/Lean/Compiler/IR/RC.ilean +lib/lean/Lean/Compiler/IR/RC.olean +lib/lean/Lean/Compiler/IR/ResetReuse.ilean +lib/lean/Lean/Compiler/IR/ResetReuse.olean +lib/lean/Lean/Compiler/IR/SimpCase.ilean +lib/lean/Lean/Compiler/IR/SimpCase.olean +lib/lean/Lean/Compiler/IR/Sorry.ilean +lib/lean/Lean/Compiler/IR/Sorry.olean +lib/lean/Lean/Compiler/IR/UnboxResult.ilean +lib/lean/Lean/Compiler/IR/UnboxResult.olean +lib/lean/Lean/Compiler/ImplementedByAttr.ilean +lib/lean/Lean/Compiler/ImplementedByAttr.olean +lib/lean/Lean/Compiler/InitAttr.ilean +lib/lean/Lean/Compiler/InitAttr.olean +lib/lean/Lean/Compiler/InlineAttrs.ilean +lib/lean/Lean/Compiler/InlineAttrs.olean +lib/lean/Lean/Compiler/LCNF.ilean +lib/lean/Lean/Compiler/LCNF.olean +lib/lean/Lean/Compiler/LCNF/AlphaEqv.ilean +lib/lean/Lean/Compiler/LCNF/AlphaEqv.olean +lib/lean/Lean/Compiler/LCNF/AuxDeclCache.ilean +lib/lean/Lean/Compiler/LCNF/AuxDeclCache.olean +lib/lean/Lean/Compiler/LCNF/BaseTypes.ilean +lib/lean/Lean/Compiler/LCNF/BaseTypes.olean +lib/lean/Lean/Compiler/LCNF/Basic.ilean +lib/lean/Lean/Compiler/LCNF/Basic.olean +lib/lean/Lean/Compiler/LCNF/Bind.ilean +lib/lean/Lean/Compiler/LCNF/Bind.olean +lib/lean/Lean/Compiler/LCNF/CSE.ilean +lib/lean/Lean/Compiler/LCNF/CSE.olean +lib/lean/Lean/Compiler/LCNF/Check.ilean +lib/lean/Lean/Compiler/LCNF/Check.olean +lib/lean/Lean/Compiler/LCNF/Closure.ilean +lib/lean/Lean/Compiler/LCNF/Closure.olean +lib/lean/Lean/Compiler/LCNF/CompatibleTypes.ilean +lib/lean/Lean/Compiler/LCNF/CompatibleTypes.olean +lib/lean/Lean/Compiler/LCNF/CompilerM.ilean +lib/lean/Lean/Compiler/LCNF/CompilerM.olean +lib/lean/Lean/Compiler/LCNF/ConfigOptions.ilean +lib/lean/Lean/Compiler/LCNF/ConfigOptions.olean +lib/lean/Lean/Compiler/LCNF/DeclHash.ilean +lib/lean/Lean/Compiler/LCNF/DeclHash.olean +lib/lean/Lean/Compiler/LCNF/DependsOn.ilean +lib/lean/Lean/Compiler/LCNF/DependsOn.olean +lib/lean/Lean/Compiler/LCNF/ElimDead.ilean +lib/lean/Lean/Compiler/LCNF/ElimDead.olean +lib/lean/Lean/Compiler/LCNF/ElimDeadBranches.ilean +lib/lean/Lean/Compiler/LCNF/ElimDeadBranches.olean +lib/lean/Lean/Compiler/LCNF/FVarUtil.ilean +lib/lean/Lean/Compiler/LCNF/FVarUtil.olean +lib/lean/Lean/Compiler/LCNF/FixedParams.ilean +lib/lean/Lean/Compiler/LCNF/FixedParams.olean +lib/lean/Lean/Compiler/LCNF/FloatLetIn.ilean +lib/lean/Lean/Compiler/LCNF/FloatLetIn.olean +lib/lean/Lean/Compiler/LCNF/ForEachExpr.ilean +lib/lean/Lean/Compiler/LCNF/ForEachExpr.olean +lib/lean/Lean/Compiler/LCNF/InferType.ilean +lib/lean/Lean/Compiler/LCNF/InferType.olean +lib/lean/Lean/Compiler/LCNF/Internalize.ilean +lib/lean/Lean/Compiler/LCNF/Internalize.olean +lib/lean/Lean/Compiler/LCNF/JoinPoints.ilean +lib/lean/Lean/Compiler/LCNF/JoinPoints.olean +lib/lean/Lean/Compiler/LCNF/LCtx.ilean +lib/lean/Lean/Compiler/LCNF/LCtx.olean +lib/lean/Lean/Compiler/LCNF/LambdaLifting.ilean +lib/lean/Lean/Compiler/LCNF/LambdaLifting.olean +lib/lean/Lean/Compiler/LCNF/Level.ilean +lib/lean/Lean/Compiler/LCNF/Level.olean +lib/lean/Lean/Compiler/LCNF/Main.ilean +lib/lean/Lean/Compiler/LCNF/Main.olean +lib/lean/Lean/Compiler/LCNF/MonadScope.ilean +lib/lean/Lean/Compiler/LCNF/MonadScope.olean +lib/lean/Lean/Compiler/LCNF/MonoTypes.ilean +lib/lean/Lean/Compiler/LCNF/MonoTypes.olean +lib/lean/Lean/Compiler/LCNF/OtherDecl.ilean +lib/lean/Lean/Compiler/LCNF/OtherDecl.olean +lib/lean/Lean/Compiler/LCNF/PassManager.ilean +lib/lean/Lean/Compiler/LCNF/PassManager.olean +lib/lean/Lean/Compiler/LCNF/Passes.ilean +lib/lean/Lean/Compiler/LCNF/Passes.olean +lib/lean/Lean/Compiler/LCNF/PhaseExt.ilean +lib/lean/Lean/Compiler/LCNF/PhaseExt.olean +lib/lean/Lean/Compiler/LCNF/PrettyPrinter.ilean +lib/lean/Lean/Compiler/LCNF/PrettyPrinter.olean +lib/lean/Lean/Compiler/LCNF/Probing.ilean +lib/lean/Lean/Compiler/LCNF/Probing.olean +lib/lean/Lean/Compiler/LCNF/PullFunDecls.ilean +lib/lean/Lean/Compiler/LCNF/PullFunDecls.olean +lib/lean/Lean/Compiler/LCNF/PullLetDecls.ilean +lib/lean/Lean/Compiler/LCNF/PullLetDecls.olean +lib/lean/Lean/Compiler/LCNF/ReduceArity.ilean +lib/lean/Lean/Compiler/LCNF/ReduceArity.olean +lib/lean/Lean/Compiler/LCNF/ReduceJpArity.ilean +lib/lean/Lean/Compiler/LCNF/ReduceJpArity.olean +lib/lean/Lean/Compiler/LCNF/Renaming.ilean +lib/lean/Lean/Compiler/LCNF/Renaming.olean +lib/lean/Lean/Compiler/LCNF/ScopeM.ilean +lib/lean/Lean/Compiler/LCNF/ScopeM.olean +lib/lean/Lean/Compiler/LCNF/Simp.ilean +lib/lean/Lean/Compiler/LCNF/Simp.olean +lib/lean/Lean/Compiler/LCNF/Simp/Basic.ilean +lib/lean/Lean/Compiler/LCNF/Simp/Basic.olean +lib/lean/Lean/Compiler/LCNF/Simp/Config.ilean +lib/lean/Lean/Compiler/LCNF/Simp/Config.olean +lib/lean/Lean/Compiler/LCNF/Simp/ConstantFold.ilean +lib/lean/Lean/Compiler/LCNF/Simp/ConstantFold.olean +lib/lean/Lean/Compiler/LCNF/Simp/DefaultAlt.ilean +lib/lean/Lean/Compiler/LCNF/Simp/DefaultAlt.olean +lib/lean/Lean/Compiler/LCNF/Simp/DiscrM.ilean +lib/lean/Lean/Compiler/LCNF/Simp/DiscrM.olean +lib/lean/Lean/Compiler/LCNF/Simp/FunDeclInfo.ilean +lib/lean/Lean/Compiler/LCNF/Simp/FunDeclInfo.olean +lib/lean/Lean/Compiler/LCNF/Simp/InlineCandidate.ilean +lib/lean/Lean/Compiler/LCNF/Simp/InlineCandidate.olean +lib/lean/Lean/Compiler/LCNF/Simp/InlineProj.ilean +lib/lean/Lean/Compiler/LCNF/Simp/InlineProj.olean +lib/lean/Lean/Compiler/LCNF/Simp/JpCases.ilean +lib/lean/Lean/Compiler/LCNF/Simp/JpCases.olean +lib/lean/Lean/Compiler/LCNF/Simp/Main.ilean +lib/lean/Lean/Compiler/LCNF/Simp/Main.olean +lib/lean/Lean/Compiler/LCNF/Simp/SimpM.ilean +lib/lean/Lean/Compiler/LCNF/Simp/SimpM.olean +lib/lean/Lean/Compiler/LCNF/Simp/SimpValue.ilean +lib/lean/Lean/Compiler/LCNF/Simp/SimpValue.olean +lib/lean/Lean/Compiler/LCNF/Simp/Used.ilean +lib/lean/Lean/Compiler/LCNF/Simp/Used.olean +lib/lean/Lean/Compiler/LCNF/SpecInfo.ilean +lib/lean/Lean/Compiler/LCNF/SpecInfo.olean +lib/lean/Lean/Compiler/LCNF/Specialize.ilean +lib/lean/Lean/Compiler/LCNF/Specialize.olean +lib/lean/Lean/Compiler/LCNF/Testing.ilean +lib/lean/Lean/Compiler/LCNF/Testing.olean +lib/lean/Lean/Compiler/LCNF/ToDecl.ilean +lib/lean/Lean/Compiler/LCNF/ToDecl.olean +lib/lean/Lean/Compiler/LCNF/ToExpr.ilean +lib/lean/Lean/Compiler/LCNF/ToExpr.olean +lib/lean/Lean/Compiler/LCNF/ToLCNF.ilean +lib/lean/Lean/Compiler/LCNF/ToLCNF.olean +lib/lean/Lean/Compiler/LCNF/ToMono.ilean +lib/lean/Lean/Compiler/LCNF/ToMono.olean +lib/lean/Lean/Compiler/LCNF/Types.ilean +lib/lean/Lean/Compiler/LCNF/Types.olean +lib/lean/Lean/Compiler/LCNF/Util.ilean +lib/lean/Lean/Compiler/LCNF/Util.olean +lib/lean/Lean/Compiler/Main.ilean +lib/lean/Lean/Compiler/Main.olean +lib/lean/Lean/Compiler/NameMangling.ilean +lib/lean/Lean/Compiler/NameMangling.olean +lib/lean/Lean/Compiler/NeverExtractAttr.ilean +lib/lean/Lean/Compiler/NeverExtractAttr.olean +lib/lean/Lean/Compiler/NoncomputableAttr.ilean +lib/lean/Lean/Compiler/NoncomputableAttr.olean +lib/lean/Lean/Compiler/Old.ilean +lib/lean/Lean/Compiler/Old.olean +lib/lean/Lean/Compiler/Options.ilean +lib/lean/Lean/Compiler/Options.olean +lib/lean/Lean/Compiler/Specialize.ilean +lib/lean/Lean/Compiler/Specialize.olean +lib/lean/Lean/CoreM.ilean +lib/lean/Lean/CoreM.olean +lib/lean/Lean/Data.ilean +lib/lean/Lean/Data.olean +lib/lean/Lean/Data/Array.ilean +lib/lean/Lean/Data/Array.olean +lib/lean/Lean/Data/AssocList.ilean +lib/lean/Lean/Data/AssocList.olean +lib/lean/Lean/Data/Format.ilean +lib/lean/Lean/Data/Format.olean +lib/lean/Lean/Data/FuzzyMatching.ilean +lib/lean/Lean/Data/FuzzyMatching.olean +lib/lean/Lean/Data/HashMap.ilean +lib/lean/Lean/Data/HashMap.olean +lib/lean/Lean/Data/HashSet.ilean +lib/lean/Lean/Data/HashSet.olean +lib/lean/Lean/Data/Json.ilean +lib/lean/Lean/Data/Json.olean +lib/lean/Lean/Data/Json/Basic.ilean +lib/lean/Lean/Data/Json/Basic.olean +lib/lean/Lean/Data/Json/FromToJson.ilean +lib/lean/Lean/Data/Json/FromToJson.olean +lib/lean/Lean/Data/Json/Parser.ilean +lib/lean/Lean/Data/Json/Parser.olean +lib/lean/Lean/Data/Json/Printer.ilean +lib/lean/Lean/Data/Json/Printer.olean +lib/lean/Lean/Data/Json/Stream.ilean +lib/lean/Lean/Data/Json/Stream.olean +lib/lean/Lean/Data/JsonRpc.ilean +lib/lean/Lean/Data/JsonRpc.olean +lib/lean/Lean/Data/KVMap.ilean +lib/lean/Lean/Data/KVMap.olean +lib/lean/Lean/Data/LBool.ilean +lib/lean/Lean/Data/LBool.olean +lib/lean/Lean/Data/LOption.ilean +lib/lean/Lean/Data/LOption.olean +lib/lean/Lean/Data/Lsp.ilean +lib/lean/Lean/Data/Lsp.olean +lib/lean/Lean/Data/Lsp/Basic.ilean +lib/lean/Lean/Data/Lsp/Basic.olean +lib/lean/Lean/Data/Lsp/Capabilities.ilean +lib/lean/Lean/Data/Lsp/Capabilities.olean +lib/lean/Lean/Data/Lsp/Client.ilean +lib/lean/Lean/Data/Lsp/Client.olean +lib/lean/Lean/Data/Lsp/CodeActions.ilean +lib/lean/Lean/Data/Lsp/CodeActions.olean +lib/lean/Lean/Data/Lsp/Communication.ilean +lib/lean/Lean/Data/Lsp/Communication.olean +lib/lean/Lean/Data/Lsp/Diagnostics.ilean +lib/lean/Lean/Data/Lsp/Diagnostics.olean +lib/lean/Lean/Data/Lsp/Extra.ilean +lib/lean/Lean/Data/Lsp/Extra.olean +lib/lean/Lean/Data/Lsp/InitShutdown.ilean +lib/lean/Lean/Data/Lsp/InitShutdown.olean +lib/lean/Lean/Data/Lsp/Internal.ilean *** 1560 LINES SKIPPED ***
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?202401140350.40E3oMx4022382>