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 <[email protected]> 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 <
> [email protected]> 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
> [email protected]
> https://lists.xenproject.org/mailman/listinfo/mirageos-devel
>
>
>
_______________________________________________
MirageOS-devel mailing list
[email protected]
https://lists.xenproject.org/mailman/listinfo/mirageos-devel
