lemma/
deps.rs

1//! Dependency layout under `<workdir>/lemma_deps/`, shared by CLI fetch and LSP.
2
3use std::path::{Path, PathBuf};
4
5/// Workspace-relative directory name holding fetched registry bundles. Committed
6/// to version control: there is no lock file, so the on-disk source is authoritative.
7pub const LEMMA_DEPS_DIR_NAME: &str = "lemma_deps";
8
9#[must_use]
10pub fn lemma_deps_dir(workdir: &Path) -> PathBuf {
11    workdir.join(LEMMA_DEPS_DIR_NAME)
12}
13
14/// Relative path under `lemma_deps/` for a fetched registry bundle (`GET /@id.lemma` identity includes `@`).
15#[must_use]
16pub fn relative_dependency_cache_path(registry_attribute_display: &str) -> PathBuf {
17    let last_slash_position = registry_attribute_display.rfind('/');
18    let (directory_segment, leaf_segment) = match last_slash_position {
19        Some(slice_index) => (
20            &registry_attribute_display[..slice_index],
21            &registry_attribute_display[slice_index + 1..],
22        ),
23        None => ("", registry_attribute_display),
24    };
25    let filename_with_suffix = format!("{}.lemma", leaf_segment);
26    if directory_segment.is_empty() {
27        PathBuf::from(filename_with_suffix)
28    } else {
29        PathBuf::from(directory_segment).join(filename_with_suffix)
30    }
31}
32
33/// Derive registry dependency id from a `lemma_deps/` `.lemma` file path (same string CLI `load_batch` passes as `dependency_id`).
34#[must_use]
35pub fn dependency_identifier_from_dependency_path(
36    workdir: &Path,
37    dependency_path: &Path,
38) -> String {
39    let deps_dir = lemma_deps_dir(workdir);
40    let relative = dependency_path
41        .strip_prefix(&deps_dir)
42        .unwrap_or(dependency_path.as_ref());
43    let without_ext = relative.with_extension("");
44    without_ext.to_string_lossy().to_string()
45}
46
47/// Absolute path where `lemma fetch` writes the bundle for this registry qualifier.
48#[must_use]
49pub fn dependency_cache_file(workdir: &Path, registry_qualifier: &str) -> PathBuf {
50    lemma_deps_dir(workdir).join(relative_dependency_cache_path(registry_qualifier))
51}
52
53#[cfg(test)]
54mod tests {
55    use super::*;
56
57    #[test]
58    fn lemma_deps_dir_uses_lemma_deps_segment() {
59        let root = Path::new("/tmp/workspace");
60        assert_eq!(lemma_deps_dir(root), root.join("lemma_deps"));
61        assert_eq!(LEMMA_DEPS_DIR_NAME, "lemma_deps");
62    }
63
64    #[test]
65    fn dependency_cache_file_resolves_under_lemma_deps() {
66        let root = Path::new("/tmp/workspace");
67        assert_eq!(
68            dependency_cache_file(root, "@lemma/std"),
69            root.join("lemma_deps").join("@lemma").join("std.lemma"),
70        );
71        assert_eq!(
72            dependency_cache_file(root, "@org/project/bundle"),
73            root.join("lemma_deps")
74                .join("@org")
75                .join("project")
76                .join("bundle.lemma"),
77        );
78    }
79
80    #[test]
81    fn dependency_identifier_round_trips_through_lemma_deps() {
82        let root = Path::new("/tmp/workspace");
83        let dep_file = dependency_cache_file(root, "@lemma/std");
84        assert_eq!(
85            dependency_identifier_from_dependency_path(root, &dep_file),
86            "@lemma/std",
87        );
88    }
89}
lemma/deps.rs

lemma/
deps.rs
