Here is the latest OCaml Weekly News, for the week of January 10 to 17, 2017.
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00050.htmlLeo White announced:
I'm pleased to announce the initial release of the Prof. Spacetime viewer for Spacetime memory profiles. It is available on opam as "prof_spacetime". Documentation for both the viewer and for generating Spacetime profiles is still pretty sparse, but I've written a blog post to get people started: https://blogs.janestreet.com/a-brief-trip-through-spacetime/ An initial version of the spacetime_lib library, on which Prof. Spacetime depends, has also been released. This includes some basic high-level functionality for reading Spacetime profiles. Both the spacetime_lib library and prof_spacetime viewer are developed on GitHub: https://github.com/lpw25/prof_spacetime https://github.com/lpw25/spacetime_lib So please report any issues there.
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00051.htmlHongbo Zhang announced:
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00054.htmlSylvain Le Gall announced:
The OCaml Forge was launched 9 years ago. Today, the OCaml community will probably benefit to switch to a more popular hosting option, like Github. Over the course of 2017, the content of the current forge will be transferred to a static website or given back to its author for a migration to another hosting provider. The detailed plan for the deprecation is available in this post: http://forge.ocamlcore.org/forum/forum.php?forum_id=958
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00062.htmlPeter Sewell announced:
Updating this: the likellihood of new funding means we may be able to make several appointments, to build a really strong team. Closing date 24 Jan, as before. University of Cambridge Computer Laboratory Research Associate £29,301 - £38,183 or Senior Research Associate £39,324 - 49,772 Fixed-term: until February 28, 2019, when the grant funding the post currently ends. Details: http://www.jobs.cam.ac.uk/job/12397/ Do you want to help build mathematically rigorous foundations for real-world computing, to make it more robust and secure? We have an ongoing project to establish rigorous semantic models for production multiprocessors, to provide a clear basis for programming, software verification, and hardware verification. This involves long-term close collaborations with ARM and IBM, and we have an agreement with ARM to take their internal ISA description, build a mathematical model based on it, integrate it with the concurrency semantics we are developing, and release the whole in a form usable for verification. This will provide the first strongly validated public model for a production multiprocessor architecture. We also have a close collaboration with the CHERI research project, developing processors with hardware-accelerated in-process memory protection and sandboxing, together with an open-source operating system and toolchain based on FreeBSD and Clang/LLVM; formal modelling is at the heart of the CHERI design process. For more details, see some of our previous papers: POPL17 (http://www.cl.cam.ac.uk/~pes20/popl17/mixed-size.pdf), POPL16 (http://www.cl.cam.ac.uk/~pes20/popl16-armv8/top.pdf), MICRO 2015 (http://www.cl.cam.ac.uk/~pes20/micro-48-2015.pdf), PLDI11 (http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/pldi105-sarkar.pdf), CHERI ISA spec (http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-891.html), CHERI (https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/), REMS (http://rems.io). We have a position available to work on: - the development of our Sail metalanguage for ISA description: a language with a lightweight dependent type system, designed to capture ARM, IBM POWER, and CHERI instruction semantics in an engineer-friendly way; - translation from Sail to generate efficient emulators and usable theorem-prover definitions; - mechanised proof about the architecture definitions, e.g. of security properties, relationships between concurrency models, and correctness results for high-level language concurrency compilation; and/or - development of reasoning, symbolic execution, debugging, and/or model-checking tools above the architecture definitions - the initial work should generate many opportunities along these lines. The successful candidate must have a PhD (or equivalent experience), a track-record of publication in relevant areas of Computer Science, good knowledge of English and communication skills, and the expertise and commitment to apply rigorous semantics to real systems. We're looking for people with the skills to make solid models and tools, well-engineered and widely usable. You should have expertise in one or more of: - functional programming (e.g. OCaml) - programming language semantics and type systems - theorem provers, especially Isabelle and/or Coq - symbolic execution - model-checking For senior applicants, e.g. who will be able to contribute substantially to future grant applications, it may be possible to appoint at the Senior Research Associate level. This is part of the broader REMS (Rigorous Engineering for Mainstream Systems) programme grant: a lively collaboration between systems and semantics researchers in Cambridge, Imperial, and Edinburgh to scale up and apply mathematically rigorous semantics to mainstream systems. Informal enquiries should be directed to Peter Sewell (Peter.Sewell@cl.cam.ac.uk). To apply online for this vacancy, please click on the 'Apply' button below. This will route you to the University's Web Recruitment System, where you will need to register an account (if you have not already) and log in before completing the online application form. Please ensure you upload your Curriculum Vitae (CV) and a cover letter explaining your potential contribution to the project, as pdf documents. Include the names of 2 or 3 referees at the appropriate point in the online application. Your referees should be prepared to send references within a week of the closing date, if asked by the University. If you upload any additional documents which have not been requested, we will not be able to consider these as part of your application. Please quote reference NR10978 on your application and in any correspondence about this vacancy. The University values diversity and is committed to equality of opportunity. The University has a responsibility to ensure that all employees are eligible to live and work in the UK.
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00069.htmlHelmut Brandl asked and Nicolás Ojeda Bär replied:
Also note there are bindings to nodejs for js_of_ocaml  developped by Edgar Aroutiounian. I have not checked if the functions you need are in there, but if they're not, you could contribute them to this project. Hope that helps, Philippe.  https://github.com/fxfactorial/ocaml-nodejs
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00076.htmlContinuing this old thread, Eray Ozkural asked and Gabriel Scherer replied:
> I have a question. Have you ever designed at length how to implement a super > fast *interpreted* version of metaocaml, or let me put it this way: do you > think if that is possible at all? For fast just-in-time compilation of OCaml code, you may be interested in Benedikt Meurer's work on OCamlJit2 (the article is well-written and easy to read): Just-In-Time compilation of OCaml byte-code Benedikt Meurer, 2010 https://arxiv.org/abs/1011.6223
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00044.htmlChet Murthy asked:
I hope this is the right place to ask this question. I've been writing a nontrivial distributed system (well, a number of them over the last few years) and have had need of a robust and flexible logging framework. Specifically, I've been using "bolt" and its descendant, "volt", which provide camlp4 syntax extensions. These extensions make the syntax of the logging statements significantly less verbose, and that in itself ia a valuable thing. With the arrival of ppx rewriters, I realize that the camlp4/camlp5 method of adding syntax to ocaml is deprecated. So I wonder: is there some really good logging toolkit out there, that I've overlooked. I'm aware of a number of different packages, but only bolt/volt have syntax extensions, and it's my belief that they're essential to making effortless pervasive log-line instrumentation. But perhaps I just haven't looked hard enough .... So .... before I go write my own, I figured I'd ask the list if there were such a thing. For concreteness, the basic thing I'm looking for, is a syntax extension that somewhat resembles LOG "%s" appid LEVEL DEBUG ; which expands out to code something like begin if log_enabled <current-module/function-path-as-string> DEBUG then log (Printf.sprintf "%s" appid) end I hate writing "slight variations on somebody else's good idea", so would much prefer to "improve" somebody else's library/tool, than come up with my own.Daniil Baturin replied:
Have you looked into the logging modules from Lwt? While they work best for those who already use Lwt, and they definitely have their shortcoming, on the plus side the log statements are very concise, you can set the log level and add logging rules at runtime, and it has file and syslog logging out of the box.Hugo Herbelin remarked:
> With the arrival of ppx rewriters, I realize that the camlp4/camlp5 > method of adding syntax to ocaml is deprecated. So I wonder: is there > some really good logging toolkit out there, that I've overlooked. I don't know if OCaml developers recommend a deprecation of camlp4, but as far as camlp5 is concerned, I don't believe there is an intention from his current main developer (who actually works in the office next door to mine) to deprecate camlp5. My understanding is even the opposite, that he would be happy that campl5 continues to exist after him. What is not exclusive at all of using ppx of course! There is a room for different approaches and different objectives!Anil Madhavapeddy suggested:
In MirageOS, we've been moving away from syntax extensions and towards placing the logging directives as closures directly within the code. This is slightly slower in the case of debug logging, but in practise for distributed systems we are finding that having "permanent" logging at different levels is more valuable than the "recompile with debug logging" that we used to use. The basis library for this that our libraries are mostly using now in the forthcoming MirageOS3 is Daniel Buenzli's Logs library: http://erratique.ch/software/logs It does not have a syntax extension out of the box, but it does provide flexible support for multiple backends, and has an Lwt module included.
If you happen to miss a CWN, you can send me a message and I'll mail it to you, or go take a look at the archive or the RSS feed of the archives.
If you also wish to receive it every week by mail, you may subscribe online.