Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

chore: add lib var for macos usage #1

Merged
merged 1 commit into from
Jun 19, 2024
Merged

chore: add lib var for macos usage #1

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 24 additions & 12 deletions README.md
View file
Open in desktop
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`
Loading