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

lean_toolchain/
fingerprint.rs
