diff --git a/README.md b/README.md index 069f478..fadff20 100644 --- a/README.md +++ b/README.md @@ -1,23 +1,32 @@ # Extism Lean 4 Host SDK -This repo contains the [Lean 4](https://github.com/leanprover/lean4) package for integrating with [Extism](https://github.com/extism/extism) +This repo contains the [Lean 4](https://github.com/leanprover/lean4) package for +integrating with [Extism](https://github.com/extism/extism) -Note: These bindings are under active development and the public API is unstable. +Note: These bindings are under active development and the public API is +unstable. ## Building -The Extism shared object is required for these bindings to work, see our [installation instructions](https://extism.org/docs/install/). +The Extism shared object is required for these bindings to work, see our +[installation instructions](https://extism.org/docs/install/). From the root of the repository run: ```sh lake build + +# on macos +# DYLD_LIBRARY_PATH=/usr/local/lib lake build ``` To run the tests: ```sh lake exe test + +# on macos +# DYLD_LIBRARY_PATH=/usr/local/lib lake exe test ``` ## Getting started @@ -30,11 +39,13 @@ require extism from git "https://github.com/extism/lean4-sdk" @ "main" ### Loading a Plug-in +The primary concept in Extism is the +[plug-in](https://extism.org/docs/concepts/plug-in). A plug-in is a code module +stored in a `.wasm` file. -The primary concept in Extism is the [plug-in](https://extism.org/docs/concepts/plug-in). A plug-in is a code module stored in a `.wasm` file. - -Plug-in code can come from a file on disk, object storage or any number of places. Since you may not have one handy, let's load a demo plug-in from the web. Let's -start by creating a main function that loads a plug-in: +Plug-in code can come from a file on disk, object storage or any number of +places. Since you may not have one handy, let's load a demo plug-in from the +web. Let's start by creating a main function that loads a plug-in: ``` import Extism @@ -48,8 +59,9 @@ def main : IO Unit := do ### Calling A Plug-in's Exports -This plug-in was written in Rust and it does one thing, it counts vowels in a string. It exposes one "export" function: `count_vowels`. We can call exports using `Plugin::call`. -Let's add code to call `count_vowels` to our main func: +This plug-in was written in Rust and it does one thing, it counts vowels in a +string. It exposes one "export" function: `count_vowels`. We can call exports +using `Plugin::call`. Let's add code to call `count_vowels` to our main func: ``` import Extism @@ -63,6 +75,6 @@ def main : IO Unit := do // => {"count":3,"total":3,"vowels":"aeiouAEIOU"} ``` -Note: `call` accepts any type that implements `Extism.ToBytes` as input, and returns any type that implements -`Extism.FromBytes`, these are implemented for `ByteArray`, `String` and `Lean.Json a` - +Note: `call` accepts any type that implements `Extism.ToBytes` as input, and +returns any type that implements `Extism.FromBytes`, these are implemented for +`ByteArray`, `String` and `Lean.Json a`