Multithreaded example

Callee/Callee.lean

@@ -1,3 +1,5 @@
+import Lean
+
 @[export my_function]
 def my_function (s: String): String :=
   s ++ s!" at callee"

Callee/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:nightly-2024-03-27

build.rs

@@ -8,7 +8,6 @@ fn main() {
 	let input = format!("{lean_root}/include/lean/lean.h");
 	println!("cargo:rustc-link-search={callee_root}");
 	println!("cargo:rustc-link-search={lean_root}/lib/lean");
-	println!("cargo:rustc-link-lib=Init_shared");
 
 	let bindgen_dir = env::temp_dir().join("bindgen");
 	let extern_src_path = bindgen_dir.join("leanextern.c");

flake.lock

@@ -38,19 +38,20 @@
         "flake-utils": "flake-utils",
         "lean4-mode": "lean4-mode",
         "nix": "nix",
-        "nixpkgs": "nixpkgs_2"
+        "nixpkgs": "nixpkgs_2",
+        "nixpkgs-old": "nixpkgs-old"
       },
       "locked": {
-        "lastModified": 1709691092,
+        "lastModified": 1711508550,
-        "narHash": "sha256-jHY8BhDotfGcMS0Xzl5iawqCaug3dDEKuD5Y1WcM06I=",
+        "narHash": "sha256-UK4DnYmwXLcqHA316Zkn0cnujdYlxqUf+b6S4l56Q3s=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "6fce8f7d5cd18a4419bca7fd51780c71c9b1cc5a",
+        "rev": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
         "type": "github"
       },
       "original": {
         "owner": "leanprover",
-        "ref": "v4.7.0-rc2",
+        "ref": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
         "repo": "lean4",
         "type": "github"
       }
@@ -141,6 +142,23 @@
         "type": "github"
       }
     },
+    "nixpkgs-old": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1581379743,
+        "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-19.03",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
     "nixpkgs-regression": {
       "locked": {
         "lastModified": 1643052045,

flake.nix

@@ -4,7 +4,7 @@
   inputs = {
     nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean.url = "github:leanprover/lean4?ref=v4.7.0-rc2";
+    lean.url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2";
     rust-crate2nix = {
       url = "github:kolloch/crate2nix";
       flake = false;

src/main.rs

@@ -6,10 +6,16 @@ mod lean {
 	include!(concat!(env!("OUT_DIR"), "/lean.rs"));
 
 	#[link(name = "leanshared")]
+	#[link(name = "Init_shared")]
+	#[link(name = "leanrt")]
 	extern "C" {
 		pub fn lean_initialize_runtime_module();
 		pub fn lean_initialize();
 		// lean_io_mark_end_initialization is already defined.
+		#[link_name = "lean_initialize_thread"]
+		pub fn initialize_thread();
+		#[link_name = "lean_finalize_thread"]
+		pub fn finalize_thread();
 	}
 }
 
@@ -119,8 +125,7 @@ fn call_think(s: &str) -> Result<String, usize> {
 	}
 }
 
-fn call_print_in_upper()
+fn call_print_in_upper() {
-{
 	let c_str = std::ffi::CString::new("caller").unwrap();
 	unsafe {
 		let native_str = lean::lean_mk_string(c_str.as_ptr());
@@ -139,10 +144,27 @@ fn main() {
 	initialize();
 	println!("Lean initialization complete!");
 
-	call_my_function();
+	use std::{
-	call_stylize();
+		sync::{Arc, Barrier},
+		thread,
+	};
 
-	assert_eq!(call_think("Stanford"), Ok("tanford".to_string()));
+	let threads: usize = 10;
-	assert_eq!(call_think("Else"), Err(4));
+
-	call_print_in_upper();
+	let mut handles = Vec::with_capacity(threads);
+	let barrier = Arc::new(Barrier::new(threads));
+	for _ in 0..threads {
+		let barrier = barrier.clone();
+		handles.push(thread::spawn(move || {
+			unsafe { lean::initialize_thread() };
+			barrier.wait();
+			call_my_function();
+			call_stylize();
+			call_print_in_upper();
+			unsafe { lean::finalize_thread() };
+		}))
+	}
+	for handle in handles {
+		handle.join().unwrap();
+	}
 }