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 #-}
```
and the unikernel.ml is
```
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
```
On Sat, Oct 27, 2018 at 5:52 AM Apostolis Xekoukoulotakis <
[email protected]> wrote:
> 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?
>
>
> On Thu, Oct 25, 2018 at 9:29 PM Apostolis Xekoukoulotakis <
> [email protected]> wrote:
>
>> 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
