Stub
This commit is contained in:
commit
b53d26b7ec
GPG Key ID:
4D9B1C8D10EA4C50
|
|
@ -0,0 +1,2 @@
|
|||
.*
|
||||
!.gitignore
|
||||
|
|
@ -0,0 +1,3 @@
|
|||
@[export my_function]
|
||||
def my_function (s: String): String :=
|
||||
s ++ s!"abc"
|
||||
|
|
@ -0,0 +1,5 @@
|
|||
{"version": 7,
|
||||
"packagesDir": ".lake/packages",
|
||||
"packages": [],
|
||||
"name": "callee",
|
||||
"lakeDir": ".lake"}
|
||||
|
|
@ -0,0 +1,8 @@
|
|||
import Lake
|
||||
open System Lake DSL
|
||||
|
||||
package callee
|
||||
|
||||
@[default_target]
|
||||
lean_lib Callee where
|
||||
defaultFacets := #[LeanLib.sharedFacet]
|
||||
|
|
@ -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"
|
||||
|
|
@ -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]
|
||||
|
|
@ -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)
|
||||
|
|
@ -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
|
||||
}
|
||||
|
|
@ -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
|
||||
];
|
||||
};
|
||||
};
|
||||
};
|
||||
}
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
.*
|
||||
!.gitignore
|
||||
|
|
@ -0,0 +1,3 @@
|
|||
fn main() {
|
||||
println!("Testing!");
|
||||
}
|
||||
Loading…
Reference in New Issue