Callee/Callee.lean

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

Callee/lean-toolchain

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

flake.lock

@@ -38,20 +38,19 @@
         "flake-utils": "flake-utils",
         "lean4-mode": "lean4-mode",
         "nix": "nix",
-        "nixpkgs": "nixpkgs_2",
-        "nixpkgs-old": "nixpkgs-old"
+        "nixpkgs": "nixpkgs_2"
       },
       "locked": {
-        "lastModified": 1711508550,
-        "narHash": "sha256-UK4DnYmwXLcqHA316Zkn0cnujdYlxqUf+b6S4l56Q3s=",
+        "lastModified": 1695693562,
+        "narHash": "sha256-6qbCafG0bL5KxQt2gL6hV4PFDsEMM0UXfldeOOqxsaE=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
+        "rev": "a832f398b80a5ebb820d27b9e55ec949759043ff",
         "type": "github"
       },
       "original": {
         "owner": "leanprover",
-        "ref": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
+        "ref": "v4.1.0",
         "repo": "lean4",
         "type": "github"
       }
@@ -142,23 +141,6 @@
         "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=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2";
+    lean.url = "github:leanprover/lean4?ref=v4.1.0";
     rust-crate2nix = {
       url = "github:kolloch/crate2nix";
       flake = false;

src/main.rs

@@ -6,16 +6,10 @@ 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();
 	}
 }
 
@@ -125,7 +119,8 @@ 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());
@@ -144,27 +139,10 @@ fn main() {
 	initialize();
 	println!("Lean initialization complete!");
 
-	use std::{
-		sync::{Arc, Barrier},
-		thread,
-	};
+	call_my_function();
+	call_stylize();
 
-	let threads: usize = 10;
-
-	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();
-	}
+	assert_eq!(call_think("Stanford"), Ok("tanford".to_string()));
+	assert_eq!(call_think("Else"), Err(4));
+	call_print_in_upper();
 }