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::mpsc::Sender;
12use std::sync::{Arc, Mutex};
13use std::time::{Duration, SystemTime};
14use walkdir::WalkDir;
15
16#[derive(Debug, Clone, PartialEq, Eq)]
18pub struct DiscoveredPaths {
19 pub workspace_paths: Vec<PathBuf>,
21 pub dependency_paths: Vec<PathBuf>,
23}
24
25impl DiscoveredPaths {
26 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#[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
89pub 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
148pub 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
174pub fn load_workspace(engine: &mut Engine, workdir: &Path) -> Result<(), WorkspaceDiskError> {
176 load_workspace_excluding(engine, workdir, &[])
177}
178
179pub 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
228pub 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
275type 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 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 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(¤t) {
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
374pub 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
393fn deliver<T>(sink: &Sender<T>, event: T) {
395 if sink.send(event).is_err() {
396 }
398}
399
400pub 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(¤tly_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 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, ¤tly_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
513pub 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
542pub 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}