[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [MirageOS-devel] Can one use malfunction with mirageos?
With some trickery , I made it to work. (I also had to install zarith-freestanding.)
Here is the hello program in Agda :
```
module UniK where
open import Prelude.IO
open import Prelude.Monad
open import Prelude.Unit
open import Prelude.Nat
open import Prelude.String
postulate
info : String -> IO Unit
{-# FOREIGN OCaml
let info s world = Logs_lwt.info (fun f -> f (Scanf.format_from_string s ""))
#-}
{-# COMPILE OCaml info = info #-}
loop : IO Unit → Nat → IO Unit
loop sleep zero = return unit
loop sleep (suc n) = do
info "hello"
sleep
loop sleep n
start : IO Unit → IO Unit
start sleep = loop sleep 4
{-# COMPILE OCaml start as val start : (unit -> unit Lwt.t) -> unit -> unit Lwt.t #-}
```
``` module DD = ForeignCode
module Hello (Time : Mirage_time_lwt.S) = struct
let start _time = UniK.start (fun _ -> Time.sleep_ns (Duration.of_sec 1)) ()
end
```
The previous example worked because ```Import``` didn't use any code from the ForeignCode module. Unfortunately, mirage cannot detect the dependency to ForeignCode, so when It tries to create the file ```main.native``` , it does not include it and the compilation/linking fails.
```
+ ocamlfind ocamlopt -g -linkpkg -g -thread -package zarith -package uutf -package uunf.string -package uunf -package uucp -package mirage-unix -package mirage-types-lwt -package mirage-types -package mirage-runtime -package mirage-logs -package mirage-clock-unix -package lwt -package logs.lwt -package logs -package functoria-runtime -package duration -predicates mirage_unix UniK.cmx key_gen.cmx unikernel.cmx main.cmx -o main.native
File "_none_", line 1:
Error: No implementations provided for the following modules:
ForeignCode referenced from UniK.cmx, unikernel.cmx, main.cmx
Command exited with code 2.
run ['ocamlbuild' '-use-ocamlfind' '-classic-display' '-tags'
'predicate(mirage_unix),warn(A-4-41-42-44),debug,bin_annot,strict_sequence,principal,safe_string,thread,color(always)'
'-pkgs'
'duration,functoria-runtime,logs,logs.lwt,lwt,mirage-clock-unix,mirage-logs,mirage-runtime,mirage-types,mirage-types-lwt,mirage-unix,uucp,uunf,uunf.string,uutf,zarith'
'-cflags' '-g' '-lflags' '-g' '-tag-line' '<static*.*>: warn(-32-34)'
'-X' '_build-solo5-hvt' '-X' '_build-ukvm' 'main.native']: exited with 10
Makefile:18: recipe for target 'build' failed
make: *** [build] Error 1 ```
If I execute the last command manually and add the file (ForeignCode.cmx) , it works for the ```unix``` target. For the other targets, there is more work to be done after that command.
Is there a way to resolve this issue?
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.
>
> 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
_______________________________________________
MirageOS-devel mailing list
MirageOS-devel@xxxxxxxxxxxxxxxxxxxx
https://lists.xenproject.org/mailman/listinfo/mirageos-devel
|
