Xen project Mailing List

It worked!! I performed these steps for it to work.

```

mirage configure -t ukvm

agda-ocaml --mlf --cmx Import.agda

```

Then I move the compiled output inside _build.

The generated Import.mli , I keep inside the initial directory because it seems that it is needed there.

then I execute :

```

make depend

make

```

and it works.

Do you have any suggestions on the placement of files? or the workflow?

(For example, It would be nice if packages set at config.ml were also passed to agda-ocaml.)

Other than that, let's have some fun writing a server in Agda.

On another note , I think that I need to compile Agda' IO monad into Lwt.

On Thu, Oct 25, 2018 at 1:56 PM Thomas Gazagnaire <thomas@xxxxxxxxxxxxxx> wrote:

>
> 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?

The easiest way is to start to adapt the hello world example[1]

You can add zarith and unicode dependencies in config.ml like that:

```

let packages = [
package "zarith";
package "uucp";
package "uutf";
package ~sublibs:["string"] "uunf";
]

let () =
register ~packages "hello" [main $ default_time]
```

And then modify unikernel.ml to call Import.bold: ocamlbuild will automatically detect the dependency and build things in the right order:

```
Logs.info (fun f -> f Import.bold)
```

Hope that helps,
Thomas

[1]: https://github.com/mirage/mirage-skeleton/tree/master/tutorial/hello

>
>
>
> 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

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