From b53d26b7ecc599c9a517e9c940298e69d11bb7d0 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 4 Mar 2024 21:08:55 -0800 Subject: [PATCH] Stub --- .gitignore | 2 + Callee/Callee.lean | 3 + Callee/lake-manifest.json | 5 + Callee/lakefile.lean | 8 ++ Cargo.lock | 7 ++ Cargo.toml | 11 +++ README.md | 9 ++ flake.lock | 202 ++++++++++++++++++++++++++++++++++++++ flake.nix | 45 +++++++++ src/.gitignore | 2 + src/main.rs | 3 + 11 files changed, 297 insertions(+) create mode 100644 .gitignore create mode 100644 Callee/Callee.lean create mode 100644 Callee/lake-manifest.json create mode 100644 Callee/lakefile.lean create mode 100644 Cargo.lock create mode 100644 Cargo.toml create mode 100644 README.md create mode 100644 flake.lock create mode 100644 flake.nix create mode 100644 src/.gitignore create mode 100644 src/main.rs diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..9ea0f13 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +.* +!.gitignore diff --git a/Callee/Callee.lean b/Callee/Callee.lean new file mode 100644 index 0000000..46723c3 --- /dev/null +++ b/Callee/Callee.lean @@ -0,0 +1,3 @@ +@[export my_function] +def my_function (s: String): String := + s ++ s!"abc" diff --git a/Callee/lake-manifest.json b/Callee/lake-manifest.json new file mode 100644 index 0000000..351580c --- /dev/null +++ b/Callee/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": 7, + "packagesDir": ".lake/packages", + "packages": [], + "name": "callee", + "lakeDir": ".lake"} diff --git a/Callee/lakefile.lean b/Callee/lakefile.lean new file mode 100644 index 0000000..cb0c4d0 --- /dev/null +++ b/Callee/lakefile.lean @@ -0,0 +1,8 @@ +import Lake +open System Lake DSL + +package callee + +@[default_target] +lean_lib Callee where + defaultFacets := #[LeanLib.sharedFacet] diff --git a/Cargo.lock b/Cargo.lock new file mode 100644 index 0000000..770c440 --- /dev/null +++ b/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "rustcalllean" +version = "0.1.0" diff --git a/Cargo.toml b/Cargo.toml new file mode 100644 index 0000000..d2190a6 --- /dev/null +++ b/Cargo.toml @@ -0,0 +1,11 @@ +[package] +name = "rustcalllean" +description = "Rust calls Lean" +authors = ["Leni Aniva"] +publish = false + +version = "0.1.0" +edition = "2021" +rust-version = "1.73" + +[dependencies] diff --git a/README.md b/README.md new file mode 100644 index 0000000..fc2fa99 --- /dev/null +++ b/README.md @@ -0,0 +1,9 @@ +# Rust Call Lean + +A tiny example of calling Lean's FFI from Rust with Nix. + +This is based on: +* [Lean4 Reverse FFI](https://github.com/leanprover/lean4/tree/master/src/lake/examples/reverse-ffi) +* [Lean4 FFI](https://lean-lang.org/lean4/doc/dev/ffi.html#initialization) +* [Rustonomicon FFI](https://doc.rust-lang.org/nomicon/ffi.html) +* [Rust Bindgen](https://rust-lang.github.io/rust-bindgen/introduction.html) diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..0475ae7 --- /dev/null +++ b/flake.lock @@ -0,0 +1,202 @@ +{ + "nodes": { + "flake-parts": { + "inputs": { + "nixpkgs-lib": "nixpkgs-lib" + }, + "locked": { + "lastModified": 1709336216, + "narHash": "sha256-Dt/wOWeW6Sqm11Yh+2+t0dfEWxoMxGBvv3JpIocFl9E=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "f7b3c975cf067e56e7cda6cb098ebe3fb4d74ca2", + "type": "github" + }, + "original": { + "owner": "hercules-ci", + "repo": "flake-parts", + "type": "github" + } + }, + "flake-utils": { + "locked": { + "lastModified": 1656928814, + "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "lean": { + "inputs": { + "flake-utils": "flake-utils", + "lean4-mode": "lean4-mode", + "nix": "nix", + "nixpkgs": "nixpkgs_2" + }, + "locked": { + "lastModified": 1695693562, + "narHash": "sha256-6qbCafG0bL5KxQt2gL6hV4PFDsEMM0UXfldeOOqxsaE=", + "owner": "leanprover", + "repo": "lean4", + "rev": "a832f398b80a5ebb820d27b9e55ec949759043ff", + "type": "github" + }, + "original": { + "owner": "leanprover", + "ref": "v4.1.0", + "repo": "lean4", + "type": "github" + } + }, + "lean4-mode": { + "flake": false, + "locked": { + "lastModified": 1676498134, + "narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=", + "owner": "leanprover", + "repo": "lean4-mode", + "rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440", + "type": "github" + }, + "original": { + "owner": "leanprover", + "repo": "lean4-mode", + "type": "github" + } + }, + "lowdown-src": { + "flake": false, + "locked": { + "lastModified": 1633514407, + "narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=", + "owner": "kristapsdz", + "repo": "lowdown", + "rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8", + "type": "github" + }, + "original": { + "owner": "kristapsdz", + "repo": "lowdown", + "type": "github" + } + }, + "nix": { + "inputs": { + "lowdown-src": "lowdown-src", + "nixpkgs": "nixpkgs", + "nixpkgs-regression": "nixpkgs-regression" + }, + "locked": { + "lastModified": 1657097207, + "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=", + "owner": "NixOS", + "repo": "nix", + "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f", + "type": "github" + }, + "original": { + "owner": "NixOS", + "repo": "nix", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1653988320, + "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-22.05-small", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs-lib": { + "locked": { + "dir": "lib", + "lastModified": 1709237383, + "narHash": "sha256-cy6ArO4k5qTx+l5o+0mL9f5fa86tYUX3ozE1S+Txlds=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "1536926ef5621b09bba54035ae2bb6d806d72ac8", + "type": "github" + }, + "original": { + "dir": "lib", + "owner": "NixOS", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs-regression": { + "locked": { + "lastModified": 1643052045, + "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", + "type": "github" + }, + "original": { + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", + "type": "github" + } + }, + "nixpkgs_2": { + "locked": { + "lastModified": 1686089707, + "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixpkgs-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs_3": { + "locked": { + "lastModified": 1709479366, + "narHash": "sha256-n6F0n8UV6lnTZbYPl1A9q1BS0p4hduAv1mGAP17CVd0=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "b8697e57f10292a6165a20f03d2f42920dfaf973", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-parts": "flake-parts", + "lean": "lean", + "nixpkgs": "nixpkgs_3" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..4b6a37e --- /dev/null +++ b/flake.nix @@ -0,0 +1,45 @@ +{ + description = "RustCallLean"; + + inputs = { + nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; + flake-parts.url = "github:hercules-ci/flake-parts"; + lean.url = "github:leanprover/lean4?ref=v4.1.0"; + }; + + outputs = inputs @ { + self, + nixpkgs, + flake-parts, + lean, + ... + } : flake-parts.lib.mkFlake { inherit inputs; } { + flake = { + }; + systems = [ + "x86_64-linux" + "x86_64-darwin" + ]; + perSystem = { system, pkgs, ... }: let + leanPkgs = lean.packages.${system}; + callee = leanPkgs.buildLeanPackage { + name = "Callee"; + roots = [ "Callee" ]; + src = ./Callee; + }; + in rec { + packages = { + inherit (leanPkgs) lean iTree stage1 lean-all; + callee = callee.sharedLib; + }; + devShells.default = pkgs.mkShell { + CALLEE_PATH = callee.sharedLib; + LEAN_INCLUDE_PATH = leanPkgs.lean-all; + buildInputs = [ + leanPkgs.lean-all + pkgs.rustc + ]; + }; + }; + }; +} diff --git a/src/.gitignore b/src/.gitignore new file mode 100644 index 0000000..9ea0f13 --- /dev/null +++ b/src/.gitignore @@ -0,0 +1,2 @@ +.* +!.gitignore diff --git a/src/main.rs b/src/main.rs new file mode 100644 index 0000000..89dc87a --- /dev/null +++ b/src/main.rs @@ -0,0 +1,3 @@ +fn main() { + println!("Testing!"); +}