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