From 80fba97c3c5a885e318e780506179165c3d636c2 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 4 Dec 2024 05:53:57 -0800
Subject: [PATCH] fixes paths thing

---
 crates/flux-config/src/lib.rs       | 24 +++++++++++++-----------
 crates/flux-driver/src/callbacks.rs |  2 +-
 2 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/crates/flux-config/src/lib.rs b/crates/flux-config/src/lib.rs
index fac779925c..cb5ef96c31 100644
--- a/crates/flux-config/src/lib.rs
+++ b/crates/flux-config/src/lib.rs
@@ -48,7 +48,7 @@ pub fn is_cache_enabled() -> bool {
 }
 
 pub fn is_checked_file(file: &str) -> bool {
-    CONFIG.check_files.is_empty() || CONFIG.check_files.contains(file)
+    CONFIG.check_files.is_checked_file(file)
 }
 
 pub fn cache_path() -> PathBuf {
@@ -94,16 +94,14 @@ struct Config {
 
 #[derive(Default)]
 struct Paths {
-    paths: Vec<PathBuf>,
+    paths: Option<Vec<PathBuf>>,
 }
 
 impl Paths {
-    fn is_empty(&self) -> bool {
-        self.paths.is_empty()
-    }
-
-    fn contains(&self, path: &str) -> bool {
-        self.paths.iter().any(|p| p.to_str().unwrap() == path)
+    fn is_checked_file(&self, file: &str) -> bool {
+        self.paths
+            .as_ref()
+            .map_or(true, |p| p.iter().any(|p| p.to_str().unwrap() == file))
     }
 }
 
@@ -112,11 +110,15 @@ impl<'de> Deserialize<'de> for Paths {
     where
         D: serde::Deserializer<'de>,
     {
-        let paths = String::deserialize(deserializer)?
-            .split(',')
-            .into_iter()
+        let paths: Vec<PathBuf> = String::deserialize(deserializer)?
+            .split(",")
+            .map(str::trim)
+            .filter(|s| !s.is_empty())
             .map(PathBuf::from)
             .collect();
+
+        let paths = if paths.is_empty() { None } else { Some(paths) };
+
         Ok(Paths { paths })
     }
 }
diff --git a/crates/flux-driver/src/callbacks.rs b/crates/flux-driver/src/callbacks.rs
index 5345ed6c37..604b52924a 100644
--- a/crates/flux-driver/src/callbacks.rs
+++ b/crates/flux-driver/src/callbacks.rs
@@ -164,7 +164,7 @@ impl<'genv, 'tcx> CrateChecker<'genv, 'tcx> {
                 return config::is_checked_file(&file);
             }
         }
-        return true;
+        true
     }
 
     fn check_def_catching_bugs(&mut self, def_id: LocalDefId) -> Result<(), ErrorGuaranteed> {