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 load_workspace(engine: &mut Engine, workdir: &Path) -> Result<(), WorkspaceDiskError> {
149 load_workspace_excluding(engine, workdir, &[])
150}
151
152pub 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
214type 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 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 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(¤t) {
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
311pub struct WatchGuard {
313 _debouncer: Arc<Mutex<Option<notify_debouncer_mini::Debouncer<notify::RecommendedWatcher>>>>,
314}
315
316pub 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(¤tly_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 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, ¤tly_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
427pub 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
456pub 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}