Mac Malone e0a793ae20 feat: ignore lean -R if module name is in setup (#8874) ... This PR skips attempting to compute a module name from the file name and root directory (i.e., `lean -R`) if a name is already provided via `lean --setup`. This is accomplished by porting the rest of the frontend code in the `try` block to Lean.		2025-06-23 17:55:52 +00:00
..
alloc.h	perf: use mimalloc with important C++ hash maps (#7868)	2025-04-11 16:23:33 +00:00
ascii.cpp
ascii.h
bit_tricks.cpp	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
bit_tricks.h
CMakeLists.txt	fix: Windows needs more LEAN_EXPORTs	2024-08-12 14:14:42 +02:00
escaped.cpp
escaped.h
exception_with_pos.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
ffi.cpp	chore: CMAKE_CXX_SYSROOT_FLAG is also needed for linking (#6297)	2024-12-03 16:14:22 +00:00
freset.h
init_module.cpp	fix: Windows needs more LEAN_EXPORTs	2024-08-12 14:14:42 +02:00
init_module.h	fix: Windows needs more LEAN_EXPORTs	2024-08-12 14:14:42 +02:00
io.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
kvmap.cpp	feat: implement bool operator==(data_value const & a, data_value const & b) using Lean autogenerated code	2021-12-16 16:37:47 -08:00
kvmap.h	fix: Windows needs more LEAN_EXPORTs	2024-08-12 14:14:42 +02:00
lbool.cpp
lbool.h
list.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
list_fn.cpp
list_fn.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
macros.h
map_foreach.cpp	fix: dllexport functions not already annotated in header	2021-09-20 18:41:46 +02:00
map_foreach.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
message_definitions.h	feat: define Int8 (#5790)	2024-10-25 06:06:40 +00:00
name.cpp	fix: Windows needs more LEAN_EXPORTs	2024-08-12 14:14:42 +02:00
name.h	fix: Windows needs more LEAN_EXPORTs	2024-08-12 14:14:42 +02:00
name_generator.cpp	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
name_generator.h
name_hash_map.h
name_hash_set.h
name_map.h
name_set.cpp
name_set.h
nat.h	perf: fix implementation of move constructors and move assignment ope… (#4700)	2024-08-02 17:55:03 +00:00
null_ostream.h
option_declarations.cpp	feat: hover/go-to-def/refs for options	2022-11-07 20:01:13 +01:00
option_declarations.h	fix: Windows needs more LEAN_EXPORTs	2024-08-12 14:14:42 +02:00
options.cpp	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
options.h	fix: Windows needs more LEAN_EXPORTs	2024-08-12 14:14:42 +02:00
output_channel.h	chore: fix spelling mistakes in non-Lean files (#5430)	2024-09-23 21:11:20 +00:00
pair.h	chore: remove obsolete serializer code	2021-07-22 18:59:39 +02:00
path.cpp	fix: resolve symbolic links through IO.FS.realPath on windows (#8534)	2025-06-13 13:16:13 +00:00
path.h	fix: resolve symbolic links through IO.FS.realPath on windows (#8534)	2025-06-13 13:16:13 +00:00
rb_map.h
rb_tree.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
rc.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
shell.cpp	feat: ignore lean -R if module name is in setup (#8874)	2025-06-23 17:55:52 +00:00
test.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
timeit.cpp
timeit.h	fix: show exclusive profiling times everywhere	2021-06-17 11:25:58 +02:00
timer.cpp
timer.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
unit.h
unlock_guard.h