Skip to content

Commit

Permalink
chore: add lib var for macos usage (#1)
Browse files Browse the repository at this point in the history
  • Loading branch information
nilslice authored Jun 19, 2024
1 parent 13e5908 commit 4f8c307
Showing 1 changed file with 24 additions and 12 deletions.
36 changes: 24 additions & 12 deletions README.md
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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`

0 comments on commit 4f8c307

Please sign in to comment.