OCaml Weekly News

📢 LexiFi is hiring!

✔️ Software Engineer (full-time): https://lnkd.in/evhkxTg

✔️ Software Development Internship: https://lnkd.in/gb-bdDA9

LexiFi is a software editor, based in Paris. We have been happily using OCaml 🐪 for more than 20 years in our entire software stack, from backend components to UI (web & native) front-end, and we contribute back to the OCaml community (check out our blog post : https://www.lexifi.com/blog/ocaml/ocaml-open-source/)

Don't hesitate to contact me directly if you want to learn more about the positions before applying!

Alt-Ergo est l'un des solveurs SMT les plus efficaces pour la vérification formelle de code. Il est ainsi utilisé derrière des ateliers tels que Why3, Frama-C et Spark. Initialement développé par Sylvain Conchon au LRI, il est aujourd'hui maintenu par OCamlPro, grâce aux financements du Club Alt-Ergo (AdaCore, Trust-in-Soft, Thalès, MERCE, CEA List), à des contrats bilatéraux d'évolution et à des projets collaboratifs.

OCamlPro souhaite aujourd'hui recruter un développeur principal à temps plein pour Alt-Ergo, pour compléter son équipe méthodes formelles et accélérer l'évolution d'Alt-Ergo. Disposant d'une expérience dans les méthodes formelles, ses missions seront :

• de découvrir le projet Alt-Ergo et tous ses composants (prouveur, interface graphique, etc.) et d'en comprendre le fonctionnement à travers l'exploration du code et la lecture d'articles scientifiques;
• d'élaborer la roadmap de maintenance évolutive d'Alt-Ergo, en collaboration avec les membres du Club Alt-Ergo, et de proposer des améliorations qui pourront être financées au travers de contrats bilatéraux ou de projets collaboratifs;
• de participer avec l'équipe à la maintenance corrective d'Alt-Ergo et de fournir du support aux membres du Club Alt-Ergo;
• de participer à l'encadrement de stages et de thèses CIFRE autour d'Alt-Ergo et des solveurs SMT en général;
• de suivre l'actualité des solveurs SMTs et des travaux scientifiques connexes, et de maintenir des collaborations avec les experts académiques du domaine;

Intégré au sein de l'équipe Méthodes Formelles d'OCamlPro, il bénéficiera de leur expérience et leur fera bénéficier de son expertise croissante dans l'utilisation d'Alt-Ergo. Outre la maintenance d'Alt-Ergo, l'équipe Méthodes Formelles d'OCamlPro participe à diverses activités:

• Développement d'outils open-source pour les méthodes formelles, tels que Dolmen, Matla, etc.
• Expertises sur WhyML, TLA, Coq, et autres langages de spécification et de vérification;
• Certification de logiciels pour les Critères Communs (EAL6 et plus)
• Spécification et vérification formelle de smart contracts (Solidity, etc.)

Les bureaux d'OCamlPro sont dans le 14ème arrondissement de Paris (Alésia). L'entreprise est connue pour son équipe sympathique, son excellence technique, sa productivité, ses valeurs et son éthique.

Si ce poste vous intéresse, n'hésitez pas à envoyer votre CV à:

contact@ocamlpro.com

Pour plus d'informations sur OCamlPro:

https://www.ocamlpro.com/

Pour plus d'informations sur Alt-Ergo:

https://alt-ergo.ocamlpro.com/

Pour plus d'informations sur le Club Alt-Ergo:

https://www.ocamlpro.com/club-alt-ergo

I am a beginner at both Javascript and js_of_ocaml, so I may be mixing up all sorts of mistakes and misconceptions here.

I have compiled up an existing project, my command line PDF tools, using js_of_ocaml, and all is well:

$ node cpdf.js -info hello.pdf
Encryption: Not encrypted
Permissions:
Linearized: false
Version: 1.1
Pages: 1

Like magic! But I had to comment out the parts of my code which use external C code of course - that is zlib and some encryption primitives. So now I wish to bind javascript libraries for those. I am experimenting with a simple library of my own, first, which is given on the command line to js_of_ocaml as foomod.js:

foo = 42;

I can get to this global variable easily from OCaml:

let foo = Js.Unsafe.global##.foo

But now I want to do things better, and I change foomod.js to:

exports.foo = 42;

How can I get to that? Giving foomod.js on the js_of_ocaml command line includes the contents of foomod.js in some way, but does not contain the string foomod, so I'm not sure how to get to the foomod's variables and functions. How to I access them? In the node REPL, I can simply do:

> foomod = require('./foomod.js');
{ foo; 42 }
> foomod.foo;
42

I have read the js_of_ocaml help page on how to bind JS modules:

https://ocsigen.org/js_of_ocaml/latest/manual/bindings

I imagine if I could get over this hump, all the rest of the information I need will be there.

Not exactly what you asked, but if you just want to provide a JS version of some C primitive

external foo : unit -> int = "caml_foo"

you can do this by writing the following in your .js file:

//Provides: caml_foo
function caml_foo() {
  return 42;
}

Then js_of_ocaml will automatically replace calls to the external function by a call to its JS implementation.

This is the same mechanism used by js_of_ocaml to implement its own JS version of the OCaml runtime, see eg

https://github.com/ocsigen/js_of_ocaml/blob/3850a67b1cb00cfd2ee4399cf1e2948062884b92/runtime/bigarray.js#L328-L335

TLDR:

$ opam update
$ opam install diskuvbox

$ diskuvbox copy-dir --mode 755 src1/ src2/ dest/
$ diskuvbox copy-file --mode 400 src/a dest/b
$ diskuvbox copy-file-into src1/a src2/b dest/
$ diskuvbox touch-file x/y/z

$ diskuvbox find-up . _build
Z:/source/_build

$ diskuvbox tree --max-depth 2 --encoding=UTF-8 .
.
├── CHANGES.md
├── README.md
├── _build/
│   ├── default/
│   ├── install/
│   └── log

Problem: When writing cram tests, Dune rules and Opam build steps, often we default to using GNU binaries (/usr/bin/*) available on Linux (ex. /usr/bin/cp -R). Unfortunately these commands rarely work on Windows, and as a consequence Windows OCaml developers are forced to maintain Cygwin or MSYS2 installations to get GNU tooling.

Solution: Provide some of the same functionality for Windows and macOS that the GNU binaries in /usr/bin/* do in Linux.

diskuvbox is a single binary that today provides an analog for a very small number of binaries that I have needed in the Diskuv Windows OCaml distribution. It is liberally licensed under Apache v2.0. With your PRs it could emulate much more!

diskuvbox has CI testing for Windows, macOS and Linux. Usage and help are available in the diskuvbox README: https://github.com/diskuv/diskuvbox#diskuv-box

diskuvbox also has a OCaml library, but consider the API unstable until version 1.0.

Alternatives:

• There are some shell scripting tools like shexp and feather that give you POSIX pipes in OCaml-friendly syntax. I feel these complement Diskuv Box.
• Dune exposes (copy) to copy a file in Dune rules; theoretically more operations could be added.

Internally diskuvbox is a wrapper on the excellent bos - Basic OS interaction library.