feat: print profiling information into a folder per-file, instead of …

…one large file
opencompl · Apr 1, 2024 · 0295b50 · 0295b50
1 parent 3893b21
commit 0295b50
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 6 deletions.
diff --git 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
@@ -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,23 +847,31 @@ 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";
         } else {
           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);
           }
         }