lean_toolchain/
fingerprint.rs

1//! Typed composition of the build-baked Lean toolchain identity.
2//!
3//! Every field is a `&'static str` resolved at build time — by
4//! `lean-rs-sys`'s build script (`LEAN_VERSION`, `LEAN_HEADER_DIGEST`) or by
5//! this crate's `build.rs` (`LAKE_FIXTURE_DIGEST`, `HOST_TRIPLE`). Published
6//! crate builds that do not contain the workspace fixture record a zero
7//! `LAKE_FIXTURE_DIGEST`; the value is a workspace regression key, not a
8//! downstream compatibility promise. The
9//! fingerprint is therefore stable across runs for a given build and cheap to
10//! use as a cache key.
11
12// `LAKE_FIXTURE_DIGEST` and `HOST_TRIPLE` are emitted as `pub const` by
13// `build.rs`.
14include!(concat!(env!("OUT_DIR"), "/metadata.rs"));
15
16/// Typed identity of the Lean toolchain this crate was compiled against.
17///
18/// `Eq + Hash` so the fingerprint can serve as a `HashMap` key for caches
19/// keyed by toolchain identity (e.g. compiled module caches, proof caches).
20/// `Clone + Debug` are derived for convenience; every field is `&'static str`
21/// so cloning is a pointer copy.
22#[derive(Clone, Debug, Eq, Hash, PartialEq)]
23pub struct ToolchainFingerprint {
24    /// `LEAN_VERSION_STRING` from the active `lean.h`.
25    pub lean_version: &'static str,
26    /// The version string from the matched
27    /// [`SupportedToolchain`](lean_rs_sys::SupportedToolchain) entry. Equal
28    /// to [`Self::lean_version`] except when several releases share one
29    /// `lean.h` digest, in which case it is the first version listed for
30    /// that entry.
31    pub resolved_version: &'static str,
32    /// SHA-256 of the `lean.h` this build was resolved against.
33    pub header_sha256: &'static str,
34    /// SHA-256 of the workspace Lake fixture artifacts, or zero when the
35    /// crate is built from a published tarball without workspace fixtures.
36    pub fixture_sha256: &'static str,
37    /// Target triple this crate was built for.
38    pub host_triple: &'static str,
39}
40
41impl ToolchainFingerprint {
42    /// Compose the fingerprint from the build-baked constants.
43    #[must_use]
44    pub const fn current() -> Self {
45        Self {
46            lean_version: lean_rs_sys::LEAN_VERSION,
47            resolved_version: lean_rs_sys::LEAN_RESOLVED_VERSION,
48            header_sha256: lean_rs_sys::LEAN_HEADER_DIGEST,
49            fixture_sha256: LAKE_FIXTURE_DIGEST,
50            host_triple: HOST_TRIPLE,
51        }
52    }
53
54    /// Return `true` iff [`Self::lean_version`] is included in the
55    /// [`SUPPORTED_TOOLCHAINS`](lean_rs_sys::SUPPORTED_TOOLCHAINS) window.
56    ///
57    /// The build script already filters at compile time, so this method
58    /// returns `true` for any binary that compiled successfully. It is
59    /// exposed for tooling that constructs a fingerprint from an external
60    /// source (e.g. a remote-worker handshake).
61    #[must_use]
62    pub fn is_supported(&self) -> bool {
63        lean_rs_sys::supported_for(self.lean_version).is_some()
64    }
65}
66
67impl Default for ToolchainFingerprint {
68    fn default() -> Self {
69        Self::current()
70    }
71}
72
73#[cfg(test)]
74mod tests {
75    use super::ToolchainFingerprint;
76    use std::collections::hash_map::DefaultHasher;
77    use std::hash::{Hash as _, Hasher as _};
78
79    #[test]
80    fn current_round_trips_through_clone() {
81        let a = ToolchainFingerprint::current();
82        let b = a.clone();
83        assert_eq!(a, b);
84    }
85
86    #[test]
87    fn fingerprint_hash_is_deterministic() {
88        let a = ToolchainFingerprint::current();
89        let b = ToolchainFingerprint::current();
90        let mut ha = DefaultHasher::new();
91        let mut hb = DefaultHasher::new();
92        a.hash(&mut ha);
93        b.hash(&mut hb);
94        assert_eq!(ha.finish(), hb.finish());
95    }
96
97    #[test]
98    fn distinct_header_digest_changes_fingerprint() {
99        let a = ToolchainFingerprint::current();
100        let b = ToolchainFingerprint {
101            header_sha256: "0000000000000000000000000000000000000000000000000000000000000000",
102            ..a
103        };
104        assert_ne!(a, b);
105    }
106
107    #[test]
108    fn current_is_in_supported_window() {
109        assert!(ToolchainFingerprint::current().is_supported());
110    }
111
112    #[test]
113    fn synthetic_unknown_version_is_not_supported() {
114        let mut fp = ToolchainFingerprint::current();
115        fp.lean_version = "0.0.0-test";
116        assert!(!fp.is_supported());
117    }
118}
lean_toolchain/fingerprint.rs

lean_toolchain/
fingerprint.rs
