Skip to content

chore: Native decide dynlib - #43

Merged
samuelburnham merged 2 commits into
mainfrom
native-decide-dynlib
Aug 19, 2026
Merged

chore: Native decide dynlib#43
samuelburnham merged 2 commits into
mainfrom
native-decide-dynlib

Conversation

@samuelburnham

Copy link
Copy Markdown
Member

No description provided.

Add a cdylib output alongside the staticlib so the raw rs_blake3_* FFI
symbols can be loaded as a position-independent shared object at runtime.
This lets downstream tooling supply the BLAKE3 backend to Lean's native
evaluator for native_decide proofs, which are elaborated before any final
executable (and thus the usual static link of these symbols) exists.
Expose the shared-library (cdylib) build product as its own target so
downstream packages can fetch it directly, rather than reaching into this
package's rust/target directory to build and locate it themselves. Used to
supply the raw rs_blake3_* symbols to Lean's native evaluator at
elaboration time (native_decide).
@samuelburnham
samuelburnham merged commit db25a8a into main Aug 19, 2026
3 checks passed
@samuelburnham
samuelburnham deleted the native-decide-dynlib branch August 19, 2026 21:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants