1use 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#[derive(Debug, Clone, PartialEq, Eq)]
17pub struct DiscoveredPaths {
18 pub workspace_paths: Vec<PathBuf>,
20 pub dependency_paths: Vec<PathBuf>,
22}
23
24impl DiscoveredPaths {
25 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#[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
88pub 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
147pub fn workspace_path_label(workdir: &Path, absolute_path: &Path) -> std::sync::Arc<PathBuf> {
153 if workdir.is_file() {
154 assert_eq!(
155 absolute_path, workdir,
156 "BUG: single-file workspace discover must yield the workdir path"
157 );
158 let name = workdir
159 .file_name()
160 .expect("BUG: workspace file path must have a file name");
161 return std::sync::Arc::new(PathBuf::from(name));
162 }
163 let relative = absolute_path.strip_prefix(workdir).unwrap_or_else(|_| {
164 panic!(
165 "BUG: discovered path {} is not under workdir {}",
166 absolute_path.display(),
167 workdir.display()
168 )
169 });
170 std::sync::Arc::new(relative.to_path_buf())
171}
172
173pub fn load_workspace(engine: &mut Engine, workdir: &Path) -> Result<(), WorkspaceDiskError> {
175 load_workspace_excluding(engine, workdir, &[])
176}
177
178pub fn load_workspace_excluding(
183 engine: &mut Engine,
184 workdir: &Path,
185 exclude: &[&Path],
186) -> Result<(), WorkspaceDiskError> {
187 let discovered = discover_lemma_paths(workdir)?;
188 let mut sources = Vec::with_capacity(
189 discovered
190 .dependency_paths
191 .len()
192 .saturating_add(discovered.workspace_paths.len()),
193 );
194
195 for dep_path in &discovered.dependency_paths {
196 if exclude.contains(&dep_path.as_path()) {
197 continue;
198 }
199 let dependency_id = dependency_identifier_from_dependency_path(workdir, dep_path);
200 let content = fs::read_to_string(dep_path)?;
201 sources.push((
202 lemma::SourceType::Dependency(dependency_id.to_string()),
203 content,
204 ));
205 }
206 for path in &discovered.workspace_paths {
207 if exclude.contains(&path.as_path()) {
208 continue;
209 }
210 let content = fs::read_to_string(path)?;
211 sources.push((
212 lemma::SourceType::Path(workspace_path_label(workdir, path)),
213 content,
214 ));
215 }
216
217 if sources.is_empty() {
218 return Ok(());
219 }
220
221 match engine.load(sources) {
222 Ok(()) => Ok(()),
223 Err(errors) => Err(WorkspaceDiskError::EngineLoad(errors)),
224 }
225}
226
227pub fn refresh_workspace_via_update(
235 engine: &mut Engine,
236 workdir: &Path,
237) -> Result<(), WorkspaceDiskError> {
238 let discovered = discover_lemma_paths(workdir)?;
239 let mut sources: Vec<(lemma::SourceType, String)> = Vec::new();
240
241 for dep_path in &discovered.dependency_paths {
242 let dependency_id = dependency_identifier_from_dependency_path(workdir, dep_path);
243 let source_type = lemma::SourceType::Dependency(dependency_id.to_string());
244 let content = fs::read_to_string(dep_path)?;
245 sources.push((source_type, content));
246 }
247 for path in &discovered.workspace_paths {
248 let source_type = lemma::SourceType::Path(workspace_path_label(workdir, path));
249 let content = fs::read_to_string(path)?;
250 sources.push((source_type, content));
251 }
252
253 let mut scratch = Engine::new();
254 scratch
255 .load(sources)
256 .map_err(WorkspaceDiskError::EngineLoad)?;
257 *engine = scratch;
258 Ok(())
259}
260
261type ModifiedSnapshot = BTreeMap<PathBuf, SystemTime>;
262
263fn collect_modified_times(workdir: &Path) -> Result<ModifiedSnapshot, WorkspaceDiskError> {
264 let discovered = discover_lemma_paths(workdir)?;
265 let mut snapshot = BTreeMap::new();
266 for path in discovered.all_paths() {
267 let metadata = fs::metadata(path)?;
268 let modified = metadata.modified()?;
269 snapshot.insert(path.clone(), modified);
270 }
271 Ok(snapshot)
272}
273
274type WatchTarget = (PathBuf, bool);
276
277fn push_ancestor_dirs(targets: &mut Vec<WatchTarget>, workdir: &Path, file_path: &Path) {
278 let mut current = match file_path.parent() {
279 Some(parent) => parent,
280 None => return,
281 };
282 loop {
283 targets.push((current.to_path_buf(), false));
284 if current == workdir {
285 break;
286 }
287 match current.parent() {
288 Some(parent) if parent != current => current = parent,
289 _ => break,
290 }
291 }
292}
293
294fn desired_watch_targets(workdir: &Path) -> Result<Vec<WatchTarget>, WorkspaceDiskError> {
295 let mut targets = Vec::new();
296
297 if workdir.is_dir() {
300 targets.push((workdir.to_path_buf(), false));
301 }
302
303 let deps_dir = lemma_deps_dir(workdir);
304 if deps_dir.is_dir() {
305 targets.push((deps_dir.clone(), true));
306 }
307
308 let discovered = discover_lemma_paths(workdir)?;
309 for path in &discovered.workspace_paths {
310 push_ancestor_dirs(&mut targets, workdir, path);
311 }
312
313 if workdir.is_dir() {
317 for entry in ignore::WalkBuilder::new(workdir)
318 .hidden(true)
319 .git_ignore(true)
320 .git_global(false)
321 .git_exclude(false)
322 .require_git(false)
323 .build()
324 {
325 let entry = entry?;
326 let path = entry.path();
327 if path.starts_with(&deps_dir) {
328 continue;
329 }
330 if path.is_dir() {
331 targets.push((path.to_path_buf(), false));
332 }
333 }
334 }
335
336 targets.sort_by(|left, right| left.0.cmp(&right.0).then_with(|| left.1.cmp(&right.1)));
337 targets.dedup();
338 Ok(targets)
339}
340
341fn plant_watches(
342 watcher: &mut dyn notify::Watcher,
343 workdir: &Path,
344 currently_watched: &Mutex<std::collections::BTreeSet<WatchTarget>>,
345) -> Result<(), WorkspaceDiskError> {
346 let desired = desired_watch_targets(workdir)?;
347 let desired_set: std::collections::BTreeSet<WatchTarget> = desired.into_iter().collect();
348
349 let mut current = match currently_watched.lock() {
350 Ok(guard) => guard,
351 Err(poisoned) => poisoned.into_inner(),
352 };
353
354 for target in current.difference(&desired_set) {
355 let _ = watcher.unwatch(&target.0);
356 }
357 for target in desired_set.difference(¤t) {
358 let mode = if target.1 {
359 notify::RecursiveMode::Recursive
360 } else {
361 notify::RecursiveMode::NonRecursive
362 };
363 watcher
364 .watch(&target.0, mode)
365 .map_err(|error| WorkspaceDiskError::Io(std::io::Error::other(error)))?;
366 }
367 *current = desired_set;
368 Ok(())
369}
370
371pub struct WatchGuard {
377 debouncer: Arc<Mutex<Option<notify_debouncer_mini::Debouncer<notify::RecommendedWatcher>>>>,
378}
379
380impl Drop for WatchGuard {
381 fn drop(&mut self) {
382 let mut slot = match self.debouncer.lock() {
383 Ok(guard) => guard,
384 Err(poisoned) => poisoned.into_inner(),
385 };
386 let _ = slot.take();
387 }
388}
389
390pub fn watch_lemma_workspace(
400 workdir: PathBuf,
401 on_change: Arc<dyn Fn(Result<(), WorkspaceDiskError>) + Send + Sync + 'static>,
402) -> Result<WatchGuard, WorkspaceDiskError> {
403 let initial_snapshot = collect_modified_times(&workdir)?;
404 let last_snapshot: Arc<Mutex<ModifiedSnapshot>> = Arc::new(Mutex::new(initial_snapshot));
405 let currently_watched: Arc<Mutex<std::collections::BTreeSet<WatchTarget>>> =
406 Arc::new(Mutex::new(std::collections::BTreeSet::new()));
407 let debouncer_slot: Arc<
408 Mutex<Option<notify_debouncer_mini::Debouncer<notify::RecommendedWatcher>>>,
409 > = Arc::new(Mutex::new(None));
410 let on_change = Arc::clone(&on_change);
411
412 let workdir_for_callback = workdir.clone();
413 let snapshot_for_callback = Arc::clone(&last_snapshot);
414 let watched_for_callback = Arc::clone(¤tly_watched);
415 let slot_for_callback = Arc::clone(&debouncer_slot);
416 let on_change_for_callback = Arc::clone(&on_change);
417
418 let mut debouncer = notify_debouncer_mini::new_debouncer(
419 Duration::from_millis(500),
420 move |result: Result<Vec<notify_debouncer_mini::DebouncedEvent>, notify::Error>| {
421 if let Err(error) = result {
422 on_change_for_callback(Err(WorkspaceDiskError::Io(std::io::Error::other(error))));
423 return;
424 }
425
426 let current_snapshot = match collect_modified_times(&workdir_for_callback) {
427 Ok(snapshot) => snapshot,
428 Err(error) => {
429 on_change_for_callback(Err(error));
430 return;
431 }
432 };
433
434 let files_changed = {
435 let previous = match snapshot_for_callback.lock() {
436 Ok(guard) => guard,
437 Err(poisoned) => poisoned.into_inner(),
438 };
439 current_snapshot != *previous
440 };
441 if !files_changed {
442 let mut slot = match slot_for_callback.lock() {
444 Ok(guard) => guard,
445 Err(poisoned) => poisoned.into_inner(),
446 };
447 if let Some(debouncer) = slot.as_mut() {
448 if let Err(error) = plant_watches(
449 debouncer.watcher(),
450 &workdir_for_callback,
451 &watched_for_callback,
452 ) {
453 on_change_for_callback(Err(error));
454 }
455 }
456 return;
457 }
458
459 {
460 let mut previous = match snapshot_for_callback.lock() {
461 Ok(guard) => guard,
462 Err(poisoned) => poisoned.into_inner(),
463 };
464 *previous = current_snapshot;
465 }
466
467 on_change_for_callback(Ok(()));
468
469 let mut slot = match slot_for_callback.lock() {
470 Ok(guard) => guard,
471 Err(poisoned) => poisoned.into_inner(),
472 };
473 if let Some(debouncer) = slot.as_mut() {
474 if let Err(error) = plant_watches(
475 debouncer.watcher(),
476 &workdir_for_callback,
477 &watched_for_callback,
478 ) {
479 on_change_for_callback(Err(error));
480 }
481 }
482 },
483 )
484 .map_err(|error| WorkspaceDiskError::Io(std::io::Error::other(error)))?;
485
486 plant_watches(debouncer.watcher(), &workdir, ¤tly_watched)?;
487
488 {
489 let mut slot = match debouncer_slot.lock() {
490 Ok(guard) => guard,
491 Err(poisoned) => poisoned.into_inner(),
492 };
493 *slot = Some(debouncer);
494 }
495
496 Ok(WatchGuard {
497 debouncer: debouncer_slot,
498 })
499}
500
501pub fn read_disk_lemma_files(
503 workdir: &Path,
504) -> Result<Vec<lemma_lsp::workspace_files::DiskLemmaFile>, WorkspaceDiskError> {
505 let discovered = discover_lemma_paths(workdir)?;
506 let mut files = Vec::with_capacity(
507 discovered
508 .dependency_paths
509 .len()
510 .saturating_add(discovered.workspace_paths.len()),
511 );
512
513 for path in &discovered.dependency_paths {
514 let text = fs::read_to_string(path)?;
515 files.push(lemma_lsp::workspace_files::DiskLemmaFile {
516 path: path.clone(),
517 text,
518 });
519 }
520 for path in &discovered.workspace_paths {
521 let text = fs::read_to_string(path)?;
522 files.push(lemma_lsp::workspace_files::DiskLemmaFile {
523 path: path.clone(),
524 text,
525 });
526 }
527 Ok(files)
528}
529
530pub struct CliWorkspaceFiles;
532
533impl lemma_lsp::workspace_files::WorkspaceFiles for CliWorkspaceFiles {
534 fn load(
535 &self,
536 root: &Path,
537 ) -> Result<
538 Vec<lemma_lsp::workspace_files::DiskLemmaFile>,
539 lemma_lsp::workspace_files::WorkspaceFilesError,
540 > {
541 read_disk_lemma_files(root).map_err(|error| {
542 lemma_lsp::workspace_files::WorkspaceFilesError::new(error.to_string())
543 })
544 }
545
546 fn watch(
547 &self,
548 root: PathBuf,
549 on_change: Arc<
550 dyn Fn(
551 Result<
552 Vec<lemma_lsp::workspace_files::DiskLemmaFile>,
553 lemma_lsp::workspace_files::WorkspaceFilesError,
554 >,
555 ) + Send
556 + Sync,
557 >,
558 ) -> Result<
559 lemma_lsp::workspace_files::WatchGuard,
560 lemma_lsp::workspace_files::WorkspaceFilesError,
561 > {
562 let root_for_callback = root.clone();
563 let guard = watch_lemma_workspace(
564 root,
565 Arc::new(move |watch_result| match watch_result {
566 Ok(()) => {
567 let result = read_disk_lemma_files(&root_for_callback).map_err(|error| {
568 lemma_lsp::workspace_files::WorkspaceFilesError::new(error.to_string())
569 });
570 on_change(result);
571 }
572 Err(error) => {
573 on_change(Err(lemma_lsp::workspace_files::WorkspaceFilesError::new(
574 error.to_string(),
575 )));
576 }
577 }),
578 )
579 .map_err(|error| lemma_lsp::workspace_files::WorkspaceFilesError::new(error.to_string()))?;
580
581 Ok(lemma_lsp::workspace_files::WatchGuard::from_keep_alive(
582 Box::new(guard),
583 ))
584 }
585}
586
587#[cfg(test)]
588mod tests {
589 use super::*;
590 use std::fs;
591 use std::sync::atomic::{AtomicBool, Ordering};
592 use std::time::Duration;
593
594 fn write_file(path: &Path, contents: &str) {
595 if let Some(parent) = path.parent() {
596 fs::create_dir_all(parent).expect("create parent");
597 }
598 fs::write(path, contents).expect("write file");
599 }
600
601 fn wait_until_fired(fired: &AtomicBool, message: &str) {
602 let deadline = std::time::Instant::now() + Duration::from_secs(3);
603 while std::time::Instant::now() < deadline {
604 if fired.load(Ordering::SeqCst) {
605 return;
606 }
607 std::thread::sleep(Duration::from_millis(50));
608 }
609 panic!("{message}");
610 }
611
612 #[test]
613 fn discover_excludes_gitignored_target_includes_lemma_deps() {
614 let root = tempfile::tempdir().expect("tempdir");
615 write_file(&root.path().join(".gitignore"), "/target\nlemma_deps/\n");
616 write_file(&root.path().join("src/app.lemma"), "spec app\ndata x: 1\n");
617 write_file(
618 &root.path().join("target/junk.lemma"),
619 "spec junk\ndata x: 1\n",
620 );
621 write_file(
622 &root.path().join("lemma_deps/@org/dep.lemma"),
623 "spec dep\ndata x: 1\n",
624 );
625
626 let discovered = discover_lemma_paths(root.path()).expect("discover");
627 assert_eq!(discovered.workspace_paths.len(), 1);
628 assert!(discovered.workspace_paths[0].ends_with("src/app.lemma"));
629 assert_eq!(discovered.dependency_paths.len(), 1);
630 assert!(discovered.dependency_paths[0].ends_with("lemma_deps/@org/dep.lemma"));
631 }
632
633 #[test]
634 fn load_workspace_stores_workdir_relative_path_labels() {
635 let root = tempfile::tempdir().expect("tempdir");
636 write_file(
637 &root.path().join("src/app.lemma"),
638 "spec app\ndata x: 1\nrule r: x\n",
639 );
640
641 let mut engine = Engine::new();
642 load_workspace(&mut engine, root.path()).expect("load");
643 let shown = engine
644 .show(None, "app", None)
645 .expect("app must show after load");
646 assert_eq!(
647 shown.source_type,
648 Some(lemma::SourceType::Path(std::sync::Arc::new(PathBuf::from(
649 "src/app.lemma"
650 )))),
651 "Engine Path identity must be workdir-relative, not absolute"
652 );
653 }
654
655 #[test]
656 fn refresh_resolves_consumer_that_sorts_before_provider() {
657 let root = tempfile::tempdir().expect("tempdir");
658 write_file(
659 &root.path().join("z_provider.lemma"),
660 "spec person\ndata name: \"Alice\"\n",
661 );
662 write_file(
663 &root.path().join("a_consumer.lemma"),
664 "spec company\nuses employee: person\n -> with name: \"Bob\"\n",
665 );
666
667 let mut engine = Engine::new();
668 refresh_workspace_via_update(&mut engine, root.path()).expect("two-pass refresh");
669 assert!(engine.show(None, "person", None).is_ok());
670 assert!(engine.show(None, "company", None).is_ok());
671 }
672
673 #[test]
674 fn watch_fires_when_lemma_deps_file_appears() {
675 let root = tempfile::tempdir().expect("tempdir");
676 write_file(&root.path().join(".gitignore"), "lemma_deps/\n");
677 write_file(&root.path().join("src/app.lemma"), "spec app\ndata x: 1\n");
678 fs::create_dir_all(root.path().join("lemma_deps")).expect("create lemma_deps");
679
680 let fired = Arc::new(AtomicBool::new(false));
681 let fired_flag = Arc::clone(&fired);
682 let _guard = watch_lemma_workspace(
683 root.path().to_path_buf(),
684 Arc::new(move |result| {
685 if result.is_ok() {
686 fired_flag.store(true, Ordering::SeqCst);
687 }
688 }),
689 )
690 .expect("start watch");
691
692 write_file(
693 &root.path().join("lemma_deps/@org/dep.lemma"),
694 "spec dep\ndata x: 1\n",
695 );
696
697 wait_until_fired(&fired, "watch did not fire after creating lemma_deps file");
698 }
699
700 #[test]
701 fn watch_does_not_fire_for_gitignored_target_lemma() {
702 let root = tempfile::tempdir().expect("tempdir");
703 write_file(&root.path().join(".gitignore"), "/target\n");
704 write_file(&root.path().join("src/app.lemma"), "spec app\ndata x: 1\n");
705 fs::create_dir_all(root.path().join("target")).expect("create target");
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 write_file(
720 &root.path().join("target/junk.lemma"),
721 "spec junk\ndata x: 1\n",
722 );
723
724 std::thread::sleep(Duration::from_millis(800));
725 assert!(
726 !fired.load(Ordering::SeqCst),
727 "gitignored target/*.lemma must not change discover snapshot"
728 );
729 }
730
731 #[test]
732 fn watch_fires_when_discovered_workspace_file_changes() {
733 let root = tempfile::tempdir().expect("tempdir");
734 let app = root.path().join("src/app.lemma");
735 write_file(&app, "spec app\ndata x: 1\n");
736
737 let fired = Arc::new(AtomicBool::new(false));
738 let fired_flag = Arc::clone(&fired);
739 let _guard = watch_lemma_workspace(
740 root.path().to_path_buf(),
741 Arc::new(move |result| {
742 if result.is_ok() {
743 fired_flag.store(true, Ordering::SeqCst);
744 }
745 }),
746 )
747 .expect("start watch");
748
749 write_file(&app, "spec app\ndata x: 2\n");
750
751 wait_until_fired(
752 &fired,
753 "watch did not fire after modifying discovered workspace file",
754 );
755 }
756
757 #[test]
758 fn watch_fires_when_sibling_workspace_file_appears() {
759 let root = tempfile::tempdir().expect("tempdir");
760 write_file(&root.path().join("src/app.lemma"), "spec app\ndata x: 1\n");
761
762 let fired = Arc::new(AtomicBool::new(false));
763 let fired_flag = Arc::clone(&fired);
764 let _guard = watch_lemma_workspace(
765 root.path().to_path_buf(),
766 Arc::new(move |result| {
767 if result.is_ok() {
768 fired_flag.store(true, Ordering::SeqCst);
769 }
770 }),
771 )
772 .expect("start watch");
773
774 write_file(
775 &root.path().join("src/other.lemma"),
776 "spec other\ndata y: 2\n",
777 );
778
779 wait_until_fired(
780 &fired,
781 "watch did not fire after creating sibling workspace file",
782 );
783 }
784
785 #[test]
786 fn watch_fires_when_nested_workspace_file_appears() {
787 let root = tempfile::tempdir().expect("tempdir");
788 write_file(&root.path().join("src/app.lemma"), "spec app\ndata x: 1\n");
789
790 let fired = Arc::new(AtomicBool::new(false));
791 let fired_flag = Arc::clone(&fired);
792 let _guard = watch_lemma_workspace(
793 root.path().to_path_buf(),
794 Arc::new(move |result| {
795 if result.is_ok() {
796 fired_flag.store(true, Ordering::SeqCst);
797 }
798 }),
799 )
800 .expect("start watch");
801
802 fs::create_dir_all(root.path().join("src/nested")).expect("create nested");
803 std::thread::sleep(Duration::from_millis(600));
804 write_file(
805 &root.path().join("src/nested/foo.lemma"),
806 "spec foo\ndata z: 3\n",
807 );
808
809 wait_until_fired(
810 &fired,
811 "watch did not fire after creating nested workspace file",
812 );
813 }
814
815 #[test]
816 fn watch_plants_lemma_deps_after_directory_is_created() {
817 let root = tempfile::tempdir().expect("tempdir");
818 write_file(&root.path().join(".gitignore"), "lemma_deps/\n");
819 write_file(&root.path().join("src/app.lemma"), "spec app\ndata x: 1\n");
820
821 let fired = Arc::new(AtomicBool::new(false));
822 let fired_flag = Arc::clone(&fired);
823 let _guard = watch_lemma_workspace(
824 root.path().to_path_buf(),
825 Arc::new(move |result| {
826 if result.is_ok() {
827 fired_flag.store(true, Ordering::SeqCst);
828 }
829 }),
830 )
831 .expect("start watch");
832
833 fs::create_dir_all(root.path().join("lemma_deps")).expect("create lemma_deps");
834 std::thread::sleep(Duration::from_millis(600));
835 write_file(
836 &root.path().join("lemma_deps/@org/dep.lemma"),
837 "spec dep\ndata x: 1\n",
838 );
839
840 wait_until_fired(
841 &fired,
842 "watch did not fire after creating lemma_deps then a dep file",
843 );
844 }
845
846 #[test]
847 fn watch_guard_drop_stops_further_callbacks() {
848 let root = tempfile::tempdir().expect("tempdir");
849 let app = root.path().join("src/app.lemma");
850 write_file(&app, "spec app\ndata x: 1\n");
851
852 let fired = Arc::new(AtomicBool::new(false));
853 let fired_flag = Arc::clone(&fired);
854 let guard = watch_lemma_workspace(
855 root.path().to_path_buf(),
856 Arc::new(move |result| {
857 if result.is_ok() {
858 fired_flag.store(true, Ordering::SeqCst);
859 }
860 }),
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}