dv: DV_LOG=debug DV_LOG_FILE=$PWD/dv.log ./.github/gen_core.json.sh

add log file support

Author: zjp-CN

.github/gen_core.json.sh

@@ -12,8 +12,8 @@ export VERIFY_RUST_STD_LIBRARY=$WORKSPACE/verify-rust-std/library
 # test/verify-rust-std needs this, so remember to
 # * update runid after verify-rust-std submodule syncs
 # * update snapshots after runid changes
-rm tmp -rf
-gh run download -D tmp -R model-checking/verify-rust-std 16777123952
+# rm tmp -rf
+# gh run download -D tmp -R model-checking/verify-rust-std 16777123952
 
 ls -alh $VERIFY_RUST_STD_LIBRARY
 

.gitignore

@@ -13,5 +13,6 @@ core.json
 *.sqlite3
 *.db
 *.diff
+*.log
 
 tmp/

Cargo.lock

@@ -17,6 +17,7 @@ eyre = "0.6"
 color-eyre = "0.6"
 
 # logger
+log = "0.4.27"
 tracing = "0.1"
 tracing-subscriber = { version = "0.3", features = ["env-filter"] }
 tracing-error = "0.2"

Cargo.toml

@@ -18,6 +18,7 @@ mod utils;
 pub fn analyze(tcx: TyCtxt) -> Vec<SerFunction> {
     let local_items = all_local_items();
     let cap = local_items.len();
+    dbg!(cap);
 
     let mut entries = Vec::with_capacity(cap);
 

src/bin/distributed-verification/functions/mod.rs

@@ -1,19 +1,47 @@
+use std::{env, fs};
 use tracing_subscriber::{EnvFilter, fmt, prelude::*, registry};
 
+const ENV_LOG: &str = "DV_LOG";
+const ENV_LOG_FILE: &str = "DV_LOG_FILE";
+
 pub fn init() {
-    // let fmt_layer = fmt::layer();
     let fmt_layer = fmt::layer()
         .with_line_number(false)
         .with_level(false)
         .without_time()
         .with_file(false)
         .with_target(false);
-    let env_layer = EnvFilter::from_default_env();
+
+    let env_layer = EnvFilter::from_env(ENV_LOG);
     let error_layer = tracing_error::ErrorLayer::default();
 
-    if let Err(err) = registry().with(env_layer).with(error_layer).with(fmt_layer).try_init() {
+    let reg = registry().with(env_layer).with(error_layer);
+
+    // When DV_LOG and DV_LOG_FILE are specified and the file exists,
+    // append logs into the file. The reason to append rather than
+    // write logs is keeping records across the whole compilation.
+    let reg = if let Some(log_file) = env::var(ENV_LOG)
+        .map(|log| {
+            log.parse::<log::Level>().ok()?;
+            log_file()
+        })
+        .ok()
+        .flatten()
+    {
+        let fmt_layer = fmt_layer.with_writer(log_file);
+        reg.with(fmt_layer).try_init()
+    } else {
+        reg.with(fmt_layer).try_init()
+    };
+
+    if let Err(err) = reg {
         eprintln!("Logger already init: {err}");
     };
 
     color_eyre::install().unwrap();
 }
+
+fn log_file() -> Option<fs::File> {
+    let file = env::var(ENV_LOG_FILE).ok()?;
+    fs::OpenOptions::new().append(true).open(file).ok()
+}