@@ -46,6 +46,7 @@ Author: Leonardo de Moura
46
46
#include " util/path.h"
47
47
#include " stdlib_flags.h"
48
48
49
+
49
50
#ifdef LEAN_TRACY
50
51
#define TRACY_ENABLE
51
52
#include " tracy/Tracy.hpp"
@@ -69,6 +70,21 @@ Author: Leonardo de Moura
69
70
#include < dlfcn.h>
70
71
#endif
71
72
73
+ std::streampos fileSize (const char * filePath) {
74
+
75
+ std::streampos fsize = 0 ;
76
+ std::ifstream file ( filePath, std::ios::binary );
77
+
78
+ fsize = file.tellg ();
79
+ file.seekg ( 0 , std::ios::end );
80
+ fsize = file.tellg () - fsize;
81
+ file.close ();
82
+
83
+ return fsize;
84
+ }
85
+
86
+
87
+
72
88
#ifdef _MSC_VER
73
89
// extremely simple implementation of getopt.h
74
90
enum arg_opt { no_argument, required_argument, optional_argument };
@@ -462,7 +478,7 @@ struct Profiler {
462
478
: " reuse_across_ctor_disabled" )
463
479
<< " ," << name << " , " << val << " \n " ;
464
480
}
465
- void write_profiling_times (std::string src_path, std::string out_path, std::ostream &o) {
481
+ void write_profiling_times (std::string src_path, std::string out_path, std::ostream &o, optional<std::string> c_file_path ) {
466
482
// if (research_isResearchLogVerbose()) {
467
483
// std::cerr << "writing profiling information "
468
484
// << "[reuseEnabled=" << (isReuseEnabled() ? "true" : "false")
@@ -493,10 +509,14 @@ struct Profiler {
493
509
write_file_identifier<uint64_t >(o, src_path, " num_recycled_pages" ,
494
510
lean::allocator::get_num_recycled_pages ());
495
511
#endif
512
+ if (c_file_path) {
513
+ write_file_identifier<uint64_t >(o, src_path, " c_file_size" , uint64_t (fileSize ((*c_file_path).c_str ())));
514
+ }
496
515
write_file_identifier<uint64_t >(o, src_path, " time_elapsed_ms" , time_elapsed_ms);
497
516
}
498
517
};
499
518
519
+
500
520
extern " C" LEAN_EXPORT int lean_main (int argc, char ** argv) {
501
521
Profiler profiler;
502
522
#ifdef LEAN_EMSCRIPTEN
@@ -826,14 +846,14 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
826
846
827
847
const std::string profiling_path = LEAN_RESEARCH_COMPILER_PROFILE_CSV_PATH;
828
848
if (profiling_path == " " ) {
829
- std::cerr << " WARN: '" << profiling_path << " ' is empty" ;
830
- }
831
-
832
- if (profiling_path == " -" ) {
833
- profiler.write_profiling_times (mod_fn, profiling_path, std::cerr);
849
+ std::cerr << " WARN: LEAN_RESEARCH_COMPILER_PROFILE_CSV_PATH ('" << profiling_path << " ') is empty" ;
834
850
} else {
835
- std::ofstream profiler_out_file (profiling_path, std::ios::app);
836
- profiler.write_profiling_times (mod_fn, profiling_path, profiler_out_file);
851
+ if (profiling_path == " -" ) {
852
+ profiler.write_profiling_times (mod_fn, profiling_path, std::cerr, c_output);
853
+ } else {
854
+ std::ofstream profiler_out_file (profiling_path, std::ios::app);
855
+ profiler.write_profiling_times (mod_fn, profiling_path, profiler_out_file, c_output);
856
+ }
837
857
}
838
858
#ifdef LEAN_SMALL_ALLOCATOR
839
859
// If the small allocator is not enabled, then we assume we are not using the sanitizer.
0 commit comments