lean_rs_interop_shims/
lib.rs

1//! Package-owned Lean source payload for the generic `lean-rs` interop shims.
2//!
3//! Downstream build scripts use this crate when they need a Lake dependency on
4//! `LeanRsInterop` without assuming a sibling `lean-rs` checkout. The helper
5//! copies only the Lean/C payload into a caller-owned root and writes a
6//! generated `lean-toolchain` for the downstream toolchain.
7
8use std::path::{Path, PathBuf};
9
10use lean_toolchain::{
11    SourcePackageError, SourcePackageManifestPolicy, SourcePackageMaterializationRequest,
12    materialize_source_package as materialize_with_toolchain,
13};
14use sha2::{Digest, Sha256};
15
16const SOURCE_ROOT: &str = env!("CARGO_MANIFEST_DIR");
17
18/// Lake package name for the generic interop shims.
19pub const PACKAGE_NAME: &str = "lean_rs_interop_shims";
20/// Lean library/root module name for the generic interop shims.
21pub const LIBRARY_NAME: &str = "LeanRsInterop";
22
23/// Request to materialize the packaged interop shim source for one toolchain.
24#[derive(Clone, Debug, Eq, PartialEq)]
25pub struct LeanRsInteropShimsSourcePackageRequest {
26    /// Caller-owned root below which the materialized source package is stored.
27    pub cache_root: PathBuf,
28    /// Lean toolchain label to write into the generated `lean-toolchain`.
29    pub toolchain_label: String,
30}
31
32/// Materialized interop shim source package.
33#[derive(Clone, Debug, Eq, PartialEq)]
34pub struct LeanRsInteropShimsSourcePackage {
35    /// Materialized Lake project root.
36    pub project_root: PathBuf,
37}
38
39/// Materialize the packaged interop shim source package.
40///
41/// # Errors
42///
43/// Returns [`SourcePackageError`] if the source payload cannot be copied, the
44/// generated `lean-toolchain` cannot be written, the provenance sidecar cannot
45/// be validated, or the materialized root cannot be installed.
46pub fn materialize_source_package(
47    input: LeanRsInteropShimsSourcePackageRequest,
48) -> Result<LeanRsInteropShimsSourcePackage, SourcePackageError> {
49    let LeanRsInteropShimsSourcePackageRequest {
50        cache_root,
51        toolchain_label,
52    } = input;
53    let request = SourcePackageMaterializationRequest {
54        source_root: PathBuf::from(SOURCE_ROOT),
55        cache_root,
56        package_name: PACKAGE_NAME.to_owned(),
57        materialized_package_name: PACKAGE_NAME.to_owned(),
58        library_name: LIBRARY_NAME.to_owned(),
59        source_digest: compute_source_digest()?,
60        source_revision: env!("CARGO_PKG_VERSION").to_owned(),
61        crate_name: env!("CARGO_PKG_NAME").to_owned(),
62        crate_version: env!("CARGO_PKG_VERSION").to_owned(),
63        toolchain_label,
64        include_paths: payload_include_paths(),
65        generated_files: Vec::new(),
66        sentinel_files: vec![
67            PathBuf::from("LeanRsInterop/Worker/Stream.lean"),
68            PathBuf::from("c/interop_callback.c"),
69        ],
70        manifest_policy: SourcePackageManifestPolicy::ZeroPackages,
71    };
72    let package = materialize_with_toolchain(&request)?;
73    Ok(LeanRsInteropShimsSourcePackage {
74        project_root: package.project_root,
75    })
76}
77
78fn payload_include_paths() -> Vec<PathBuf> {
79    [
80        "lakefile.lean",
81        "lake-manifest.json",
82        "LeanRsInterop.lean",
83        "LeanRsInterop",
84        "c",
85    ]
86    .into_iter()
87    .map(PathBuf::from)
88    .collect()
89}
90
91fn compute_source_digest() -> Result<String, SourcePackageError> {
92    let source_root = Path::new(SOURCE_ROOT);
93    let mut entries = Vec::new();
94    for include in payload_include_paths() {
95        collect_digest_entries(source_root, &include, &mut entries)?;
96    }
97    entries.sort_by(|left, right| left.0.cmp(&right.0));
98    let mut outer = Sha256::new();
99    for (canonical_path, digest) in entries {
100        outer.update(digest.as_bytes());
101        outer.update(b"  ");
102        outer.update(canonical_path.as_bytes());
103        outer.update(b"\n");
104    }
105    Ok(hex_lower(&outer.finalize()))
106}
107
108fn collect_digest_entries(
109    source_root: &Path,
110    relative: &Path,
111    entries: &mut Vec<(String, String)>,
112) -> Result<(), SourcePackageError> {
113    let source = source_root.join(relative);
114    let metadata = std::fs::symlink_metadata(&source).map_err(|source_error| SourcePackageError::Io {
115        action: "stat lean-rs interop shim payload path",
116        path: source.clone(),
117        source: source_error,
118    })?;
119    if metadata.is_dir() && !metadata.file_type().is_symlink() {
120        let dir_entries = std::fs::read_dir(&source).map_err(|source_error| SourcePackageError::Io {
121            action: "read lean-rs interop shim payload directory",
122            path: source.clone(),
123            source: source_error,
124        })?;
125        for entry in dir_entries {
126            let entry = entry.map_err(|source_error| SourcePackageError::Io {
127                action: "read lean-rs interop shim payload directory entry",
128                path: source.clone(),
129                source: source_error,
130            })?;
131            collect_digest_entries(source_root, &relative.join(entry.file_name()), entries)?;
132        }
133    } else if metadata.is_file() {
134        let bytes = std::fs::read(&source).map_err(|source_error| SourcePackageError::Io {
135            action: "read lean-rs interop shim payload file for digest",
136            path: source,
137            source: source_error,
138        })?;
139        let mut hasher = Sha256::new();
140        hasher.update(bytes);
141        entries.push((relative.to_string_lossy().into_owned(), hex_lower(&hasher.finalize())));
142    }
143    Ok(())
144}
145
146#[allow(
147    clippy::arithmetic_side_effects,
148    clippy::indexing_slicing,
149    reason = "hex encoding indexes a fixed 16-byte table with masked nibbles"
150)]
151fn hex_lower(bytes: &[u8]) -> String {
152    const HEX: &[u8; 16] = b"0123456789abcdef";
153    let mut out = String::with_capacity(bytes.len() * 2);
154    for byte in bytes {
155        out.push(char::from(HEX[(byte >> 4) as usize]));
156        out.push(char::from(HEX[(byte & 0x0f) as usize]));
157    }
158    out
159}
160
161#[cfg(test)]
162fn unique_nanos() -> u128 {
163    std::time::SystemTime::now()
164        .duration_since(std::time::UNIX_EPOCH)
165        .map_or(0, |duration| duration.as_nanos())
166}
167
168#[cfg(test)]
169mod tests {
170    use std::fs;
171    use std::path::Path;
172    use std::process::Command;
173
174    use super::{LeanRsInteropShimsSourcePackageRequest, materialize_source_package};
175
176    #[test]
177    fn materializes_source_package_with_generated_toolchain() -> Result<(), String> {
178        let temp = std::env::temp_dir().join(format!(
179            "lean-rs-interop-shims-test-{}-{}",
180            std::process::id(),
181            super::unique_nanos()
182        ));
183        drop(remove_path_if_exists(&temp));
184        fs::create_dir_all(&temp).map_err(|error| error.to_string())?;
185        let toolchain = "leanprover/lean4:v4.31.0-rc1".to_owned();
186        let package = materialize_source_package(LeanRsInteropShimsSourcePackageRequest {
187            cache_root: temp.clone(),
188            toolchain_label: toolchain.clone(),
189        })
190        .map_err(|error| error.to_string())?;
191
192        assert_eq!(
193            fs::read_to_string(package.project_root.join("lean-toolchain"))
194                .map_err(|error| error.to_string())?
195                .trim(),
196            toolchain
197        );
198        assert!(package.project_root.join("LeanRsInterop/Worker/Stream.lean").is_file());
199        assert!(package.project_root.join("c/interop_callback.c").is_file());
200        assert!(package.project_root.join("source-package.json").is_file());
201        assert!(!package.project_root.join("Cargo.toml").exists());
202        assert!(!package.project_root.join("src/lib.rs").exists());
203
204        let warm = materialize_source_package(LeanRsInteropShimsSourcePackageRequest {
205            cache_root: temp.clone(),
206            toolchain_label: toolchain,
207        })
208        .map_err(|error| error.to_string())?;
209        assert_eq!(warm.project_root, package.project_root);
210
211        drop(remove_path_if_exists(&temp));
212        Ok(())
213    }
214
215    #[test]
216    fn package_list_contains_runtime_payload_and_license_texts() -> Result<(), String> {
217        let output = Command::new("cargo")
218            .args(["package", "--allow-dirty", "--list"])
219            .current_dir(super::SOURCE_ROOT)
220            .output()
221            .map_err(|error| format!("run cargo package --list: {error}"))?;
222        if !output.status.success() {
223            return Err(format!(
224                "cargo package --list failed with status {}:\nstdout:\n{}\nstderr:\n{}",
225                output.status,
226                String::from_utf8_lossy(&output.stdout),
227                String::from_utf8_lossy(&output.stderr)
228            ));
229        }
230        let stdout = String::from_utf8(output.stdout).map_err(|error| format!("package list is UTF-8: {error}"))?;
231
232        for expected in [
233            "LeanRsInterop.lean",
234            "LeanRsInterop/Worker/Stream.lean",
235            "c/interop_callback.c",
236            "lakefile.lean",
237            "lake-manifest.json",
238            "LICENSE-APACHE",
239            "LICENSE-MIT",
240        ] {
241            if !stdout.lines().any(|line| line == expected) {
242                return Err(format!("package list should include {expected}, got:\n{stdout}"));
243            }
244        }
245        Ok(())
246    }
247
248    fn remove_path_if_exists(path: &Path) -> Result<(), String> {
249        match fs::symlink_metadata(path) {
250            Ok(metadata) if metadata.is_dir() && !metadata.file_type().is_symlink() => {
251                fs::remove_dir_all(path).map_err(|error| error.to_string())
252            }
253            Ok(_) => fs::remove_file(path).map_err(|error| error.to_string()),
254            Err(error) if error.kind() == std::io::ErrorKind::NotFound => Ok(()),
255            Err(error) => Err(error.to_string()),
256        }
257    }
258}
lean_rs_interop_shims/lib.rs

lean_rs_interop_shims/
lib.rs
