Skip to main content

lemma_cli/
workspace.rs

1//! Workspace disk policy: discover, load, and watch `.lemma` files.
2//!
3//! Discovery respects project `.gitignore` via the `ignore` crate, and always
4//! includes `<workdir>/lemma_deps/**/*.lemma` even when that directory is gitignored.
5
6use crate::deps::{dependency_identifier_from_dependency_path, lemma_deps_dir};
7use lemma::Engine;
8use std::collections::BTreeMap;
9use std::fs;
10use std::path::{Path, PathBuf};
11use std::sync::{Arc, Mutex};
12use std::time::{Duration, SystemTime};
13use walkdir::WalkDir;
14
15/// Paths discovered under a workspace root, partitioned by provenance.
16#[derive(Debug, Clone, PartialEq, Eq)]
17pub struct DiscoveredPaths {
18    /// Workspace `.lemma` files (not under `lemma_deps/`).
19    pub workspace_paths: Vec<PathBuf>,
20    /// Dependency bundles under `lemma_deps/`.
21    pub dependency_paths: Vec<PathBuf>,
22}
23
24impl DiscoveredPaths {
25    /// Every discovered path (dependencies first, then workspace), for snapshots.
26    pub fn all_paths(&self) -> impl Iterator<Item = &PathBuf> {
27        self.dependency_paths
28            .iter()
29            .chain(self.workspace_paths.iter())
30    }
31}
32
33/// Failure discovering or reading workspace sources from disk.
34#[derive(Debug)]
35pub enum WorkspaceDiskError {
36    Io(std::io::Error),
37    Ignore(ignore::Error),
38    Walkdir(walkdir::Error),
39    EngineLoad(lemma::Errors),
40}
41
42impl std::fmt::Display for WorkspaceDiskError {
43    fn fmt(&self, formatter: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
44        match self {
45            Self::Io(error) => write!(formatter, "{error}"),
46            Self::Ignore(error) => write!(formatter, "{error}"),
47            Self::Walkdir(error) => write!(formatter, "{error}"),
48            Self::EngineLoad(errors) => {
49                write!(
50                    formatter,
51                    "Workspace load failed ({} error(s))",
52                    errors.errors.len()
53                )
54            }
55        }
56    }
57}
58
59impl std::error::Error for WorkspaceDiskError {
60    fn source(&self) -> Option<&(dyn std::error::Error + 'static)> {
61        match self {
62            Self::Io(error) => Some(error),
63            Self::Ignore(error) => Some(error),
64            Self::Walkdir(error) => Some(error),
65            Self::EngineLoad(_) => None,
66        }
67    }
68}
69
70impl From<std::io::Error> for WorkspaceDiskError {
71    fn from(error: std::io::Error) -> Self {
72        Self::Io(error)
73    }
74}
75
76impl From<ignore::Error> for WorkspaceDiskError {
77    fn from(error: ignore::Error) -> Self {
78        Self::Ignore(error)
79    }
80}
81
82impl From<walkdir::Error> for WorkspaceDiskError {
83    fn from(error: walkdir::Error) -> Self {
84        Self::Walkdir(error)
85    }
86}
87
88/// Discover `.lemma` paths under `workdir` (or a single `.lemma` file).
89///
90/// Directory roots: gitignore-aware walk excluding `lemma_deps/`, plus an
91/// unconditional walk of `lemma_deps/` for dependency bundles.
92pub fn discover_lemma_paths(workdir: &Path) -> Result<DiscoveredPaths, WorkspaceDiskError> {
93    if workdir.is_file() {
94        return Ok(DiscoveredPaths {
95            workspace_paths: vec![workdir.to_path_buf()],
96            dependency_paths: Vec::new(),
97        });
98    }
99
100    let deps_dir = lemma_deps_dir(workdir);
101    let mut workspace_paths = Vec::new();
102    let mut dependency_paths = Vec::new();
103
104    for entry in ignore::WalkBuilder::new(workdir)
105        .hidden(true)
106        .git_ignore(true)
107        .git_global(false)
108        .git_exclude(false)
109        .require_git(false)
110        .build()
111    {
112        let entry = entry?;
113        let path = entry.path();
114        if path.starts_with(&deps_dir) {
115            continue;
116        }
117        if path.extension().and_then(|ext| ext.to_str()) != Some("lemma") {
118            continue;
119        }
120        if path.is_file() {
121            workspace_paths.push(path.to_path_buf());
122        }
123    }
124
125    if deps_dir.is_dir() {
126        for entry in WalkDir::new(&deps_dir) {
127            let entry = entry?;
128            let path = entry.path();
129            if path.extension().and_then(|ext| ext.to_str()) != Some("lemma") {
130                continue;
131            }
132            if path.is_file() {
133                dependency_paths.push(path.to_path_buf());
134            }
135        }
136    }
137
138    workspace_paths.sort();
139    dependency_paths.sort();
140
141    Ok(DiscoveredPaths {
142        workspace_paths,
143        dependency_paths,
144    })
145}
146
147/// Load discovered sources into `engine` (same provenance rules as the CLI always used).
148pub fn load_workspace(engine: &mut Engine, workdir: &Path) -> Result<(), WorkspaceDiskError> {
149    load_workspace_excluding(engine, workdir, &[])
150}
151
152/// Like [`load_workspace`], but skips paths in `exclude` (compared as [`Path`]).
153///
154/// Used by install plan probe so `destination_absolute` and pending force
155/// `conflict_paths` are not loaded; the candidate is loaded separately.
156pub fn load_workspace_excluding(
157    engine: &mut Engine,
158    workdir: &Path,
159    exclude: &[&Path],
160) -> Result<(), WorkspaceDiskError> {
161    let discovered = discover_lemma_paths(workdir)?;
162    let mut sources = Vec::with_capacity(
163        discovered
164            .dependency_paths
165            .len()
166            .saturating_add(discovered.workspace_paths.len()),
167    );
168
169    for dep_path in &discovered.dependency_paths {
170        if exclude.contains(&dep_path.as_path()) {
171            continue;
172        }
173        let dependency_id = dependency_identifier_from_dependency_path(workdir, dep_path);
174        let content = fs::read_to_string(dep_path)?;
175        sources.push((
176            lemma::SourceType::Dependency(dependency_id.to_string()),
177            content,
178        ));
179    }
180    for path in &discovered.workspace_paths {
181        if exclude.contains(&path.as_path()) {
182            continue;
183        }
184        let content = fs::read_to_string(path)?;
185        sources.push((
186            lemma::SourceType::Path(std::sync::Arc::new(path.clone())),
187            content,
188        ));
189    }
190
191    if sources.is_empty() {
192        return Ok(());
193    }
194
195    match engine.load(sources) {
196        Ok(()) => Ok(()),
197        Err(errors) => Err(WorkspaceDiskError::EngineLoad(errors)),
198    }
199}
200
201type ModifiedSnapshot = BTreeMap<PathBuf, SystemTime>;
202
203fn collect_modified_times(workdir: &Path) -> Result<ModifiedSnapshot, WorkspaceDiskError> {
204    let discovered = discover_lemma_paths(workdir)?;
205    let mut snapshot = BTreeMap::new();
206    for path in discovered.all_paths() {
207        let metadata = fs::metadata(path)?;
208        let modified = metadata.modified()?;
209        snapshot.insert(path.clone(), modified);
210    }
211    Ok(snapshot)
212}
213
214/// Watch target: path plus whether the watch is recursive.
215type WatchTarget = (PathBuf, bool);
216
217fn push_ancestor_dirs(targets: &mut Vec<WatchTarget>, workdir: &Path, file_path: &Path) {
218    let mut current = match file_path.parent() {
219        Some(parent) => parent,
220        None => return,
221    };
222    loop {
223        targets.push((current.to_path_buf(), false));
224        if current == workdir {
225            break;
226        }
227        match current.parent() {
228            Some(parent) if parent != current => current = parent,
229            _ => break,
230        }
231    }
232}
233
234fn desired_watch_targets(workdir: &Path) -> Result<Vec<WatchTarget>, WorkspaceDiskError> {
235    let mut targets = Vec::new();
236
237    // Non-recursive watch on the workspace root sees `lemma_deps/` appear without
238    // descending into `target/` or other large trees.
239    if workdir.is_dir() {
240        targets.push((workdir.to_path_buf(), false));
241    }
242
243    let deps_dir = lemma_deps_dir(workdir);
244    if deps_dir.is_dir() {
245        targets.push((deps_dir.clone(), true));
246    }
247
248    let discovered = discover_lemma_paths(workdir)?;
249    for path in &discovered.workspace_paths {
250        push_ancestor_dirs(&mut targets, workdir, path);
251    }
252
253    // Dynamic expand: non-recursive watch on every non-ignored directory under
254    // workdir (except lemma_deps, covered recursively). New child dirs become
255    // visible on the next plant after the parent wakes.
256    if workdir.is_dir() {
257        for entry in ignore::WalkBuilder::new(workdir)
258            .hidden(true)
259            .git_ignore(true)
260            .git_global(false)
261            .git_exclude(false)
262            .require_git(false)
263            .build()
264        {
265            let entry = entry?;
266            let path = entry.path();
267            if path.starts_with(&deps_dir) {
268                continue;
269            }
270            if path.is_dir() {
271                targets.push((path.to_path_buf(), false));
272            }
273        }
274    }
275
276    targets.sort_by(|left, right| left.0.cmp(&right.0).then_with(|| left.1.cmp(&right.1)));
277    targets.dedup();
278    Ok(targets)
279}
280
281fn plant_watches(
282    watcher: &mut dyn notify::Watcher,
283    workdir: &Path,
284    currently_watched: &Mutex<std::collections::BTreeSet<WatchTarget>>,
285) -> Result<(), WorkspaceDiskError> {
286    let desired = desired_watch_targets(workdir)?;
287    let desired_set: std::collections::BTreeSet<WatchTarget> = desired.into_iter().collect();
288
289    let mut current = match currently_watched.lock() {
290        Ok(guard) => guard,
291        Err(poisoned) => poisoned.into_inner(),
292    };
293
294    for target in current.difference(&desired_set) {
295        let _ = watcher.unwatch(&target.0);
296    }
297    for target in desired_set.difference(&current) {
298        let mode = if target.1 {
299            notify::RecursiveMode::Recursive
300        } else {
301            notify::RecursiveMode::NonRecursive
302        };
303        watcher
304            .watch(&target.0, mode)
305            .map_err(|error| WorkspaceDiskError::Io(std::io::Error::other(error)))?;
306    }
307    *current = desired_set;
308    Ok(())
309}
310
311/// Keeps the filesystem watcher alive until dropped.
312pub struct WatchGuard {
313    _debouncer: Arc<Mutex<Option<notify_debouncer_mini::Debouncer<notify::RecommendedWatcher>>>>,
314}
315
316/// Watch discovered `.lemma` paths under `workdir` (not the whole tree recursively).
317///
318/// Plants non-recursive watches on `workdir`, on every non-ignored directory under
319/// it, and on ancestors of discovered workspace `.lemma` files; plus `lemma_deps/`
320/// recursively when that directory exists.
321///
322/// `on_change` runs on the notify debouncer thread: `Ok(())` when the discover
323/// snapshot changed; `Err` when discover/watch maintenance failed. Callers that
324/// need async work must spawn their own runtime/thread.
325pub fn watch_lemma_workspace(
326    workdir: PathBuf,
327    on_change: Arc<dyn Fn(Result<(), WorkspaceDiskError>) + Send + Sync + 'static>,
328) -> Result<WatchGuard, WorkspaceDiskError> {
329    let initial_snapshot = collect_modified_times(&workdir)?;
330    let last_snapshot: Arc<Mutex<ModifiedSnapshot>> = Arc::new(Mutex::new(initial_snapshot));
331    let currently_watched: Arc<Mutex<std::collections::BTreeSet<WatchTarget>>> =
332        Arc::new(Mutex::new(std::collections::BTreeSet::new()));
333    let debouncer_slot: Arc<
334        Mutex<Option<notify_debouncer_mini::Debouncer<notify::RecommendedWatcher>>>,
335    > = Arc::new(Mutex::new(None));
336    let on_change = Arc::clone(&on_change);
337
338    let workdir_for_callback = workdir.clone();
339    let snapshot_for_callback = Arc::clone(&last_snapshot);
340    let watched_for_callback = Arc::clone(&currently_watched);
341    let slot_for_callback = Arc::clone(&debouncer_slot);
342    let on_change_for_callback = Arc::clone(&on_change);
343
344    let mut debouncer = notify_debouncer_mini::new_debouncer(
345        Duration::from_millis(500),
346        move |result: Result<Vec<notify_debouncer_mini::DebouncedEvent>, notify::Error>| {
347            if let Err(error) = result {
348                on_change_for_callback(Err(WorkspaceDiskError::Io(std::io::Error::other(error))));
349                return;
350            }
351
352            let current_snapshot = match collect_modified_times(&workdir_for_callback) {
353                Ok(snapshot) => snapshot,
354                Err(error) => {
355                    on_change_for_callback(Err(error));
356                    return;
357                }
358            };
359
360            let files_changed = {
361                let previous = match snapshot_for_callback.lock() {
362                    Ok(guard) => guard,
363                    Err(poisoned) => poisoned.into_inner(),
364                };
365                current_snapshot != *previous
366            };
367            if !files_changed {
368                // Still refresh watches when `lemma_deps/` or nested dirs appear.
369                let mut slot = match slot_for_callback.lock() {
370                    Ok(guard) => guard,
371                    Err(poisoned) => poisoned.into_inner(),
372                };
373                if let Some(debouncer) = slot.as_mut() {
374                    if let Err(error) = plant_watches(
375                        debouncer.watcher(),
376                        &workdir_for_callback,
377                        &watched_for_callback,
378                    ) {
379                        on_change_for_callback(Err(error));
380                    }
381                }
382                return;
383            }
384
385            {
386                let mut previous = match snapshot_for_callback.lock() {
387                    Ok(guard) => guard,
388                    Err(poisoned) => poisoned.into_inner(),
389                };
390                *previous = current_snapshot;
391            }
392
393            on_change_for_callback(Ok(()));
394
395            let mut slot = match slot_for_callback.lock() {
396                Ok(guard) => guard,
397                Err(poisoned) => poisoned.into_inner(),
398            };
399            if let Some(debouncer) = slot.as_mut() {
400                if let Err(error) = plant_watches(
401                    debouncer.watcher(),
402                    &workdir_for_callback,
403                    &watched_for_callback,
404                ) {
405                    on_change_for_callback(Err(error));
406                }
407            }
408        },
409    )
410    .map_err(|error| WorkspaceDiskError::Io(std::io::Error::other(error)))?;
411
412    plant_watches(debouncer.watcher(), &workdir, &currently_watched)?;
413
414    {
415        let mut slot = match debouncer_slot.lock() {
416            Ok(guard) => guard,
417            Err(poisoned) => poisoned.into_inner(),
418        };
419        *slot = Some(debouncer);
420    }
421
422    Ok(WatchGuard {
423        _debouncer: debouncer_slot,
424    })
425}
426
427/// Read all discovered `.lemma` files for LSP / tooling injection.
428pub fn read_disk_lemma_files(
429    workdir: &Path,
430) -> Result<Vec<lemma_lsp::workspace_files::DiskLemmaFile>, WorkspaceDiskError> {
431    let discovered = discover_lemma_paths(workdir)?;
432    let mut files = Vec::with_capacity(
433        discovered
434            .dependency_paths
435            .len()
436            .saturating_add(discovered.workspace_paths.len()),
437    );
438
439    for path in &discovered.dependency_paths {
440        let text = fs::read_to_string(path)?;
441        files.push(lemma_lsp::workspace_files::DiskLemmaFile {
442            path: path.clone(),
443            text,
444        });
445    }
446    for path in &discovered.workspace_paths {
447        let text = fs::read_to_string(path)?;
448        files.push(lemma_lsp::workspace_files::DiskLemmaFile {
449            path: path.clone(),
450            text,
451        });
452    }
453    Ok(files)
454}
455
456/// CLI implementation of [`lemma_lsp::workspace_files::WorkspaceFiles`].
457pub struct CliWorkspaceFiles;
458
459impl lemma_lsp::workspace_files::WorkspaceFiles for CliWorkspaceFiles {
460    fn load(
461        &self,
462        root: &Path,
463    ) -> Result<
464        Vec<lemma_lsp::workspace_files::DiskLemmaFile>,
465        lemma_lsp::workspace_files::WorkspaceFilesError,
466    > {
467        read_disk_lemma_files(root).map_err(|error| {
468            lemma_lsp::workspace_files::WorkspaceFilesError::new(error.to_string())
469        })
470    }
471
472    fn watch(
473        &self,
474        root: PathBuf,
475        on_change: Arc<
476            dyn Fn(
477                    Result<
478                        Vec<lemma_lsp::workspace_files::DiskLemmaFile>,
479                        lemma_lsp::workspace_files::WorkspaceFilesError,
480                    >,
481                ) + Send
482                + Sync,
483        >,
484    ) -> Result<
485        lemma_lsp::workspace_files::WatchGuard,
486        lemma_lsp::workspace_files::WorkspaceFilesError,
487    > {
488        let root_for_callback = root.clone();
489        let guard = watch_lemma_workspace(
490            root,
491            Arc::new(move |watch_result| match watch_result {
492                Ok(()) => {
493                    let result = read_disk_lemma_files(&root_for_callback).map_err(|error| {
494                        lemma_lsp::workspace_files::WorkspaceFilesError::new(error.to_string())
495                    });
496                    on_change(result);
497                }
498                Err(error) => {
499                    on_change(Err(lemma_lsp::workspace_files::WorkspaceFilesError::new(
500                        error.to_string(),
501                    )));
502                }
503            }),
504        )
505        .map_err(|error| lemma_lsp::workspace_files::WorkspaceFilesError::new(error.to_string()))?;
506
507        Ok(lemma_lsp::workspace_files::WatchGuard::from_keep_alive(
508            Box::new(guard),
509        ))
510    }
511}
512
513#[cfg(test)]
514mod tests {
515    use super::*;
516    use std::fs;
517    use std::sync::atomic::{AtomicBool, Ordering};
518    use std::time::Duration;
519
520    fn write_file(path: &Path, contents: &str) {
521        if let Some(parent) = path.parent() {
522            fs::create_dir_all(parent).expect("create parent");
523        }
524        fs::write(path, contents).expect("write file");
525    }
526
527    fn wait_until_fired(fired: &AtomicBool, message: &str) {
528        let deadline = std::time::Instant::now() + Duration::from_secs(3);
529        while std::time::Instant::now() < deadline {
530            if fired.load(Ordering::SeqCst) {
531                return;
532            }
533            std::thread::sleep(Duration::from_millis(50));
534        }
535        panic!("{message}");
536    }
537
538    #[test]
539    fn discover_excludes_gitignored_target_includes_lemma_deps() {
540        let root = tempfile::tempdir().expect("tempdir");
541        write_file(&root.path().join(".gitignore"), "/target\nlemma_deps/\n");
542        write_file(&root.path().join("src/app.lemma"), "spec app\ndata x: 1\n");
543        write_file(
544            &root.path().join("target/junk.lemma"),
545            "spec junk\ndata x: 1\n",
546        );
547        write_file(
548            &root.path().join("lemma_deps/@org/dep.lemma"),
549            "spec dep\ndata x: 1\n",
550        );
551
552        let discovered = discover_lemma_paths(root.path()).expect("discover");
553        assert_eq!(discovered.workspace_paths.len(), 1);
554        assert!(discovered.workspace_paths[0].ends_with("src/app.lemma"));
555        assert_eq!(discovered.dependency_paths.len(), 1);
556        assert!(discovered.dependency_paths[0].ends_with("lemma_deps/@org/dep.lemma"));
557    }
558
559    #[test]
560    fn watch_fires_when_lemma_deps_file_appears() {
561        let root = tempfile::tempdir().expect("tempdir");
562        write_file(&root.path().join(".gitignore"), "lemma_deps/\n");
563        write_file(&root.path().join("src/app.lemma"), "spec app\ndata x: 1\n");
564        fs::create_dir_all(root.path().join("lemma_deps")).expect("create lemma_deps");
565
566        let fired = Arc::new(AtomicBool::new(false));
567        let fired_flag = Arc::clone(&fired);
568        let _guard = watch_lemma_workspace(
569            root.path().to_path_buf(),
570            Arc::new(move |result| {
571                if result.is_ok() {
572                    fired_flag.store(true, Ordering::SeqCst);
573                }
574            }),
575        )
576        .expect("start watch");
577
578        write_file(
579            &root.path().join("lemma_deps/@org/dep.lemma"),
580            "spec dep\ndata x: 1\n",
581        );
582
583        wait_until_fired(&fired, "watch did not fire after creating lemma_deps file");
584    }
585
586    #[test]
587    fn watch_does_not_fire_for_gitignored_target_lemma() {
588        let root = tempfile::tempdir().expect("tempdir");
589        write_file(&root.path().join(".gitignore"), "/target\n");
590        write_file(&root.path().join("src/app.lemma"), "spec app\ndata x: 1\n");
591        fs::create_dir_all(root.path().join("target")).expect("create target");
592
593        let fired = Arc::new(AtomicBool::new(false));
594        let fired_flag = Arc::clone(&fired);
595        let _guard = watch_lemma_workspace(
596            root.path().to_path_buf(),
597            Arc::new(move |result| {
598                if result.is_ok() {
599                    fired_flag.store(true, Ordering::SeqCst);
600                }
601            }),
602        )
603        .expect("start watch");
604
605        write_file(
606            &root.path().join("target/junk.lemma"),
607            "spec junk\ndata x: 1\n",
608        );
609
610        std::thread::sleep(Duration::from_millis(800));
611        assert!(
612            !fired.load(Ordering::SeqCst),
613            "gitignored target/*.lemma must not change discover snapshot"
614        );
615    }
616
617    #[test]
618    fn watch_fires_when_discovered_workspace_file_changes() {
619        let root = tempfile::tempdir().expect("tempdir");
620        let app = root.path().join("src/app.lemma");
621        write_file(&app, "spec app\ndata x: 1\n");
622
623        let fired = Arc::new(AtomicBool::new(false));
624        let fired_flag = Arc::clone(&fired);
625        let _guard = watch_lemma_workspace(
626            root.path().to_path_buf(),
627            Arc::new(move |result| {
628                if result.is_ok() {
629                    fired_flag.store(true, Ordering::SeqCst);
630                }
631            }),
632        )
633        .expect("start watch");
634
635        write_file(&app, "spec app\ndata x: 2\n");
636
637        wait_until_fired(
638            &fired,
639            "watch did not fire after modifying discovered workspace file",
640        );
641    }
642
643    #[test]
644    fn watch_fires_when_sibling_workspace_file_appears() {
645        let root = tempfile::tempdir().expect("tempdir");
646        write_file(&root.path().join("src/app.lemma"), "spec app\ndata x: 1\n");
647
648        let fired = Arc::new(AtomicBool::new(false));
649        let fired_flag = Arc::clone(&fired);
650        let _guard = watch_lemma_workspace(
651            root.path().to_path_buf(),
652            Arc::new(move |result| {
653                if result.is_ok() {
654                    fired_flag.store(true, Ordering::SeqCst);
655                }
656            }),
657        )
658        .expect("start watch");
659
660        write_file(
661            &root.path().join("src/other.lemma"),
662            "spec other\ndata y: 2\n",
663        );
664
665        wait_until_fired(
666            &fired,
667            "watch did not fire after creating sibling workspace file",
668        );
669    }
670
671    #[test]
672    fn watch_fires_when_nested_workspace_file_appears() {
673        let root = tempfile::tempdir().expect("tempdir");
674        write_file(&root.path().join("src/app.lemma"), "spec app\ndata x: 1\n");
675
676        let fired = Arc::new(AtomicBool::new(false));
677        let fired_flag = Arc::clone(&fired);
678        let _guard = watch_lemma_workspace(
679            root.path().to_path_buf(),
680            Arc::new(move |result| {
681                if result.is_ok() {
682                    fired_flag.store(true, Ordering::SeqCst);
683                }
684            }),
685        )
686        .expect("start watch");
687
688        fs::create_dir_all(root.path().join("src/nested")).expect("create nested");
689        std::thread::sleep(Duration::from_millis(600));
690        write_file(
691            &root.path().join("src/nested/foo.lemma"),
692            "spec foo\ndata z: 3\n",
693        );
694
695        wait_until_fired(
696            &fired,
697            "watch did not fire after creating nested workspace file",
698        );
699    }
700
701    #[test]
702    fn watch_plants_lemma_deps_after_directory_is_created() {
703        let root = tempfile::tempdir().expect("tempdir");
704        write_file(&root.path().join(".gitignore"), "lemma_deps/\n");
705        write_file(&root.path().join("src/app.lemma"), "spec app\ndata x: 1\n");
706
707        let fired = Arc::new(AtomicBool::new(false));
708        let fired_flag = Arc::clone(&fired);
709        let _guard = watch_lemma_workspace(
710            root.path().to_path_buf(),
711            Arc::new(move |result| {
712                if result.is_ok() {
713                    fired_flag.store(true, Ordering::SeqCst);
714                }
715            }),
716        )
717        .expect("start watch");
718
719        fs::create_dir_all(root.path().join("lemma_deps")).expect("create lemma_deps");
720        std::thread::sleep(Duration::from_millis(600));
721        write_file(
722            &root.path().join("lemma_deps/@org/dep.lemma"),
723            "spec dep\ndata x: 1\n",
724        );
725
726        wait_until_fired(
727            &fired,
728            "watch did not fire after creating lemma_deps then a dep file",
729        );
730    }
731}