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