From 0295b501f26943637d15bfc26b7bfc5fc478c064 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Mon, 1 Apr 2024 12:49:43 +0100 Subject: [PATCH] feat: print profiling information into a folder per-file, instead of one large file --- src/CMakeLists.txt | 2 +- src/util/shell.cpp | 18 +++++++++++++----- 2 files changed, 14 insertions(+), 6 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 21769af7da73..0e320837f8ec 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -41,7 +41,7 @@ enable_testing() # Lean research options set (LEAN_RESEARCH_IS_REUSE_ACROSS_CONSTRUCTORS_ENABLED "0" CACHE STRING "research: enable reuse across constructors") message(STATUS "Research: reuse across ctor LEAN_RESEARCH_IS_REUSE_ACROSS_CONSTRUCTORS_ENABLED(${LEAN_RESEARCH_IS_REUSE_ACROSS_CONSTRUCTORS_ENABLED})") -set (LEAN_RESEARCH_COMPILER_PROFILE_CSV_PATH "" CACHE STRING "research: path where compiler dumps info") +set (LEAN_RESEARCH_COMPILER_PROFILE_CSV_PATH "/tmp/" CACHE STRING "research: folder where compiler dumps info") message(STATUS "Research: compiler profile CSV path LEAN_RESEARCH_COMPILER_PROFILE_CSV_PATH(${LEAN_RESEARCH_COMPILER_PROFILE_CSV_PATH})") option(MULTI_THREAD "MULTI_THREAD" ON) diff --git a/src/util/shell.cpp b/src/util/shell.cpp index 6b5520d75dbb..900bab9758b9 100644 --- a/src/util/shell.cpp +++ b/src/util/shell.cpp @@ -47,7 +47,7 @@ Author: Leonardo de Moura #include "util/path.h" #include "stdlib_flags.h" -namespace fs = std::filesystem; +namespace fs = std::__fs::filesystem; #ifdef LEAN_TRACY @@ -847,15 +847,23 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) { display_cumulative_profiling_times(std::cerr); - fs::path profile_filename = std::string(fs::current_path() / *c_output); + // take the output C path, normalize it, and use the normalized path for dumping CSV info. + const fs::path canonical_c_outpath = [&]() { + fs::path c_outpath = fs::absolute(fs::current_path() / (std::string(*c_output))); + std::error_code ec; + fs::path out = fs::canonical(c_outpath, ec); + if (ec) { return c_outpath; } + return out; + } + std::string profile_filename(std::string(canonical_c_outpath) + ".profile.csv"); // replace all '/' with '+' in filepath to avoid creating subdirectories std::replace(profile_filename.begin(), profile_filename.end(), '/', '+'); - fs::path outdir = LEAN_RESEARCH_COMPILER_PROFILE_CSV_PATH; + const fs::path outdir(LEAN_RESEARCH_COMPILER_PROFILE_CSV_PATH); assert(outdir.is_directory() && "LEAN_RESEARCH_COMPILER_PROFILE_CSV_PATH must be a directory"); assert(outdir.is_absolute() && "LEAN_RESEARCH_COMPILER_PROFILE_CSV_PATH must be an absolute path"); // make outdir if necessary if (!fs::exists(outdir)) { fs::create_directories(outdir); } - fs::path profiling_path = outdir / profile_filename; + const fs::path profiling_path = outdir / profile_filename; if (profiling_path == "") { std::cerr << "WARN: LEAN_RESEARCH_COMPILER_PROFILE_CSV_PATH ('" << profiling_path << "') is empty"; @@ -863,7 +871,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) { if (profiling_path == "-") { profiler.write_profiling_times(mod_fn, profiling_path, std::cerr, c_output); } else { - std::ofstream profiler_out_file(profiling_path, std::ios::app); + std::ofstream profiler_out_file(profiling_path); profiler.write_profiling_times(mod_fn, profiling_path, profiler_out_file, c_output); } }