Re: [MirageOS-devel] Can one use malfunction with mirageos?

[Apostolis Xekoukoulotakis <apostolis.xekoukoulotakis@xxxxxxxxx>]

Yesterday, I managed to export an agda function to Ocaml. Let me tell you how I did, so that you could help me doing the same with mirageos.

Initially , there are two files in the directory :

-- Import.agda 

```

module Import where

open import Prelude.String

bob : String
bob = "bob"

wew : String
wew = "wew"

{-# COMPILE OCaml bob as val bold : string #-}
```

and

-- test.ml

```
let _ = print_string Import.bold
```

when I compile Import.agda into a library , I get these files into the directory :

-- ForeignCode.cmi  ForeignCode.cmx  ForeignCode.ml  ForeignCode.o  Import.agda  Import.agdai  Import.cmi  Import.cmx  Import.mlf  Import.mli  Import.o  test.ml

ForeignCode.ml is OCaml code that is imported into Agda.

The Import.mli file contains :

```

val bold : string

```

In order to compile test.ml I execute this command :

```

ocamlfind ocamlopt -linkpkg -package zarith,uucp,uutf,uunf,uunf.string ForeignCode.cmx Import.cmx test.ml

```

How would I perform the last step with mirage?

On Wed, Oct 3, 2018 at 6:52 PM Anil Madhavapeddy <anil@xxxxxxxxxx> wrote:

Haven’t directly tried it, bit it should work fine.  Let us know if you run into any linking issues with the cmx.

Anil

On 3 Oct 2018, at 15:47, Apostolis Xekoukoulotakis <apostolis.xekoukoulotakis@xxxxxxxxx> wrote:

Hello, everyone, has anyone used malfunction (https://github.com/stedolan/malfunction)

to create a mirage unikernel?

malfunction creates either an executable or a ".cmx" file. (or possibly code in flambda, but this will require to fork malfunction.)

(I am trying to compile agda to malfunction and OCaml to eventually create a mirage unikernel.)

_______________________________________________
MirageOS-devel mailing list
MirageOS-devel@xxxxxxxxxxxxxxxxxxxx
https://lists.xenproject.org/mailman/listinfo/mirageos-devel

_______________________________________________
MirageOS-devel mailing list
MirageOS-devel@xxxxxxxxxxxxxxxxxxxx
https://lists.xenproject.org/mailman/listinfo/mirageos-devel