Previous week Up Next week

Hello

Here is the latest OCaml Weekly News, for the week of January 10 to 17, 2017.

  1. Prof. Spacetime 0.1.0
  2. BuckleScript New Year release
  3. Deprecating the Forge in 2017 (forge.ocamlcore.org)
  4. Postdoc position in Applied Semantics for Production Architectures
  5. Beginners Question for js_of_ocaml
  6. BER MetaOCaml N104, for OCaml 4.04.0
  7. A question about Ocaml logging

Prof. Spacetime 0.1.0

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00050.html

Leo 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.
      

BuckleScript New Year release

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00051.html

Hongbo Zhang announced:
Dear OCaml developers:
BuckleScript is an optimizing compiler for OCaml to generate readable
JavaScript, it is open sourced by Bloomberg [1].
We are glad to announce a new release for 2017(1.4.1), this release comes with
even better experience for Windows users, it is self contained on Windows
platform(no dependency on C toolchain anymore)
It also comes with a number of bug fixes and performance improvement(some
performant critical code is rewritten in C)
Documentation is available here:
http://bloomberg.github.io/bucklescript/Manual.html
To install:
npm install -g bs-platform
Happy hacking in OCaml! -- Hongbo
[1]: https://github.com/bloomberg/bucklescript/ 
      

Deprecating the Forge in 2017 (forge.ocamlcore.org)

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00054.html

Sylvain 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
      

Postdoc position in Applied Semantics for Production Architectures

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00062.html

Peter 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.
      

Beginners Question for js_of_ocaml

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00069.html

Helmut Brandl asked and Nicolás Ojeda Bär replied:
> I am trying to use js_of_ocaml to compile my ocaml project for the nodejs
> ecosystem. Since js_of_ocaml does not compile calls to the 'unix' library I
> have to call some javascript functions directly from ocaml. All I need is to be
> able to call the javascript functions
>
> - readdirSync
> - mkdirSync
> - rmdirSync
> - statSync
>
> and receive the results in ocaml.
>
> I have looked into the documentation and into the examples, but I have not
> found a way on how to do this. All examples are for use in the browser. Maybe
> its a stupid question and it is so simple that I, as a beginner in js_of_ocaml,
> just don't see it.
>
> Can anybody give me a hint? Thanks in advance.

I am a js_of_ocaml beginner, but it sounds like you could do it using :

Js.Unsafe.fun_call (Js.Unsafe.js_expr "readdirSync") [| .. args , wrapped with
Js.Unsafe.inject .. |]

You can look at the docs at
https://ocsigen.org/js_of_ocaml/2.8.3/manual/bindings, especially under
"Binding a JS function", where there is an example with the function
"decodeURI".
      
Philippe Veber then added:
Also note there are bindings to nodejs for js_of_ocaml [1] 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.

[1] https://github.com/fxfactorial/ocaml-nodejs
      

BER MetaOCaml N104, for OCaml 4.04.0

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00076.html

Continuing 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
      

A question about Ocaml logging

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00044.html

Chet 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.
      

Old cwn

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.


Alan Schmitt