Extraction to OCaml + OCaml wrapper code #18
Conversation
|
Thanks for doing all this work. This looks pretty reasonable, and should be a nice improvement for the Ocaml code for anyone that wants to use that. I'd be happy to merge this into the repo, in some form. Let me know if you think this is more-or-less the final state for these changes, or if you want to clean it up further before merging. |
This is mostly functional, but performance is an issue - mkfs and the fuse wrapper work - we vendor ocamlfuse, with patches to add support for an extra `mknod` argument and the `destroy` callback. These should be upstreamed at some point. - TODO: add support for the `create` callback in fuse - TODO: support for timings (the Rdtsc operation) (but the main TODO to make this usable is improving performance)
Armael
force-pushed
the
ocaml_extraction
branch
from
867f13d to
4ee8310
Compare
Armael
changed the title
|
Thanks! I've just squashed the intermediate commits; this should be in a mergeable state now. |
|
|
||
| Set Implicit Arguments. | ||
|
|
||
| (* Disk value and address types *) | ||
|
|
||
| Notation "'valubytes_real'" := (4 * 1024)%nat. (* 4KB *) | ||
| Notation "'valubytes_real'" := (HexString.to_nat "0x1000"). (* 4KB *) |
There was a problem hiding this comment.
Just curious: what's the rationale for using HexString.to_nat instead of doing the computation directly in nat as before? Does this help avoid some kind of degenerate nat performance issue with Ocaml extraction? I have to admit I've never even known about HexString.to_nat before seeing this.
There was a problem hiding this comment.
Yes, otherwise (AFAIR) the generated OCaml code would be building a nat by piling up 1024 S constructors, and that would make compiling (!) the ocaml code quite slow.
|
Thanks for the review and the merge! |
(This PR is based on top of #17.)
I marked this PR as WIP as it could need some work (and the history needs squashing/rebasing), cf also #16 .
The current status is that the PR adds OCaml code that should be on-par with the Haskell code functionality wise; the mkfs and fuse binaries seem to work, but performance is currently not good.
I thought it would nevertheless be a useful datapoint. I'm interested to know whether you think this would be worth merging into the repo (now or after some more work), or whether I should rather work on it on the side.