caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Alan Schmitt <alan.schmitt@polytechnique.org>
To: "lwn" <lwn@lwn.net>, "cwn"  <cwn@lists.idyll.org>, caml-list@inria.fr
Subject: [Caml-list] Attn: Development Editor, Latest OCaml Weekly News
Date: Tue, 12 Apr 2022 10:10:47 +0200	[thread overview]
Message-ID: <87lewayb5k.fsf@m4x.org> (raw)


[-- Attachment #1.1: Type: text/plain, Size: 14034 bytes --]

Hello

Here is the latest OCaml Weekly News, for the week of April 05 to 12,
2022.

Table of Contents
─────────────────

LexiFi is hiring!
Développeur principal à plein temps d'Alt-Ergo chez OCamlPro
Using an external JavaScript file in js_of_ocaml
diskuvbox: small set of cross-platform CLI tools
Old CWN


LexiFi is hiring!
═════════════════

  Archive:
  <https://discuss.ocaml.org/t/job-fulltime-internship-paris-lexifi-is-hiring/9648/1>


Alain Frisch announced
──────────────────────

  📢 [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!


[LexiFi] <https://www.lexifi.com>


Développeur principal à plein temps d'Alt-Ergo chez OCamlPro
════════════════════════════════════════════════════════════

  Archive:
  <https://discuss.ocaml.org/t/job-fulltime-paris-developpeur-principal-a-plein-temps-dalt-ergo-chez-ocamlpro/9660/1>


Fabrice Le Fessant announced
────────────────────────────

  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>


Using an external JavaScript file in js_of_ocaml
════════════════════════════════════════════════

  Archive:
  <https://discuss.ocaml.org/t/using-an-external-javascript-file-in-js-of-ocaml/9661/1>


John Whitington asked
─────────────────────

  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.


Nicolás Ojeda Bär replied
─────────────────────────

  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>


diskuvbox: small set of cross-platform CLI tools
════════════════════════════════════════════════

  Archive:
  <https://discuss.ocaml.org/t/ann-diskuvbox-small-set-of-cross-platform-cli-tools/9663/1>


jbeckford announced
───────────────────

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


[shexp] <https://github.com/janestreet/shexp>

[feather] <https://github.com/charlesetc/feather>

[bos - Basic OS interaction]
<https://erratique.ch/software/bos/doc/Bos/index.html>

Acknowledgements
╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌

  The first implementations of Diskuv Box were implemented with the
  assistance of the [OCaml Software Foundation (OCSF)], a sub-foundation
  of the [INRIA Foundation].

  Two OCaml libraries ([bos] and [cmdliner]) are essential to Diskuv
  Box; these libraries were created by [Daniel Bünzli] (@dbuenzli) .


[OCaml Software Foundation (OCSF)] <http://ocaml-sf.org>

[INRIA Foundation] <https://www.inria.fr>

[bos] <https://erratique.ch/software/bos>

[cmdliner] <https://erratique.ch/software/cmdliner>

[Daniel Bünzli] <https://erratique.ch/profile>


Examples
╌╌╌╌╌╌╌╌

  The following are examples that have been condensed from the
  [diskuvbox README.md] …


[diskuvbox README.md] <https://github.com/diskuv/diskuvbox#diskuv-box>

Using in Dune cram tests
┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄

  ┌────
  │ $ install -d a/b/c/d/e/f
  │ $ install -d a/b2/c2/d2/e2/f2
  │ $ install -d a/b2/c3/d3/e3/f3
  │ $ install -d a/b2/c3/d4/e4/f4
  │ $ install -d a/b2/c3/d4/e5/f5
  │ $ install -d a/b2/c3/d4/e5/f6
  │ $ touch a/b/x
  │ $ touch a/b/c/y
  │ $ touch a/b/c/d/z
  │ 
  │ $ diskuvbox tree a --max-depth 10 --encoding UTF-8
  │ a
  │ ├── b/
  │ │   ├── c/
  │ │   │   ├── d/
  │ │   │   │   ├── e/
  │ │   │   │   │   └── f/
  │ │   │   │   └── z
  │ │   │   └── y
  │ │   └── x
  │ └── b2/
  │     ├── c2/
  │     │   └── d2/
  │     │       └── e2/
  │     │           └── f2/
  │     └── c3/
  │         ├── d3/
  │         │   └── e3/
  │         │       └── f3/
  │         └── d4/
  │             ├── e4/
  │             │   └── f4/
  │             └── e5/
  │                 ├── f5/
  │                 └── f6/
  └────


Using in Opam `build' steps
┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄

  ┌────
  │ build: [
  │   ["diskuvbox" "copy-file-into" "assets/icon.png" "assets/public.gpg" "%{_:share}%"]
  │ ]
  └────


Using in Dune rules
┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄

  ┌────
  │ (rule
  │  (targets diskuvbox.corrected.ml diskuvbox.corrected.mli)
  │  (deps
  │   (:license %{project_root}/etc/license-header.txt)
  │   (:conf    %{project_root}/etc/headache.conf))
  │  (action
  │   (progn
  │    (run diskuvbox copy-file -m 644 diskuvbox.ml  diskuvbox.corrected.ml)
  │    (run diskuvbox copy-file -m 644 diskuvbox.mli diskuvbox.corrected.mli)
  │    (run headache -h %{license} -c %{conf} %{targets})
  │    (run ocamlformat --inplace --disable-conf-files --enable-outside-detected-project %{targets}))))
  └────


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]


[send me a message] <mailto:alan.schmitt@polytechnique.org>

[the archive] <https://alan.petitepomme.net/cwn/>

[RSS feed of the archives] <https://alan.petitepomme.net/cwn/cwn.rss>

[online] <http://lists.idyll.org/listinfo/caml-news-weekly/>

[Alan Schmitt] <https://alan.petitepomme.net/>


[-- Attachment #1.2: Type: text/html, Size: 25501 bytes --]

[-- Attachment #2: Type: text/plain, Size: 119 bytes --]

Pour une évaluation indépendante, transparente et rigoureuse !
Je soutiens la Commission d'Évaluation de l'INRIA.

             reply	other threads:[~2022-04-12  8:10 UTC|newest]

Thread overview: 112+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2022-04-12  8:10 Alan Schmitt [this message]
  -- strict thread matches above, loose matches on Subject: below --
2022-07-26 17:54 Alan Schmitt
2022-07-19  8:58 Alan Schmitt
2022-07-12  7:59 Alan Schmitt
2022-07-05  7:42 Alan Schmitt
2022-06-28  7:37 Alan Schmitt
2022-06-21  8:06 Alan Schmitt
2022-06-14  9:29 Alan Schmitt
2022-06-07 10:15 Alan Schmitt
2022-05-31 12:29 Alan Schmitt
2022-05-24  8:04 Alan Schmitt
2022-05-17  7:12 Alan Schmitt
2022-05-10 12:30 Alan Schmitt
2022-05-03  9:11 Alan Schmitt
2022-04-26  6:44 Alan Schmitt
2022-04-19  5:34 Alan Schmitt
2022-04-05 11:50 Alan Schmitt
2022-03-29  7:42 Alan Schmitt
2022-03-22 13:01 Alan Schmitt
2022-03-15  9:59 Alan Schmitt
2022-03-01 13:54 Alan Schmitt
2022-02-22 12:43 Alan Schmitt
2022-02-08 13:16 Alan Schmitt
2022-02-01 13:00 Alan Schmitt
2022-01-25 12:44 Alan Schmitt
2022-01-11  8:20 Alan Schmitt
2022-01-04  7:56 Alan Schmitt
2021-12-28  8:59 Alan Schmitt
2021-12-21  9:11 Alan Schmitt
2021-12-14 11:02 Alan Schmitt
2021-11-30 10:51 Alan Schmitt
2021-11-16  8:41 Alan Schmitt
2021-11-09 10:08 Alan Schmitt
2021-11-02  8:50 Alan Schmitt
2021-10-19  8:23 Alan Schmitt
2021-09-28  6:37 Alan Schmitt
2021-09-21  9:09 Alan Schmitt
2021-09-07 13:23 Alan Schmitt
2021-08-24 13:44 Alan Schmitt
2021-08-17  6:24 Alan Schmitt
2021-08-10 16:47 Alan Schmitt
2021-07-27  8:54 Alan Schmitt
2021-07-20 12:58 Alan Schmitt
2021-07-06 12:33 Alan Schmitt
2021-06-29 12:24 Alan Schmitt
2021-06-22  9:04 Alan Schmitt
2021-06-01  9:23 Alan Schmitt
2021-05-25  7:30 Alan Schmitt
2021-05-11 14:47 Alan Schmitt
2021-05-04  8:57 Alan Schmitt
2021-04-27 14:26 Alan Schmitt
2021-04-20  9:07 Alan Schmitt
2021-04-06  9:42 Alan Schmitt
2021-03-30 14:55 Alan Schmitt
2021-03-23  9:05 Alan Schmitt
2021-03-16 10:31 Alan Schmitt
2021-03-09 10:58 Alan Schmitt
2021-02-23  9:51 Alan Schmitt
2021-02-16 13:53 Alan Schmitt
2021-02-02 13:56 Alan Schmitt
2021-01-26 13:25 Alan Schmitt
2021-01-19 14:28 Alan Schmitt
2021-01-12  9:47 Alan Schmitt
2021-01-05 11:22 Alan Schmitt
2020-12-29  9:59 Alan Schmitt
2020-12-22  8:48 Alan Schmitt
2020-12-15  9:51 Alan Schmitt
2020-12-01  8:54 Alan Schmitt
2020-11-03 15:15 Alan Schmitt
2020-10-27  8:43 Alan Schmitt
2020-10-20  8:15 Alan Schmitt
2020-10-06  7:22 Alan Schmitt
2020-09-29  7:02 Alan Schmitt
2020-09-22  7:27 Alan Schmitt
2020-09-08 13:11 Alan Schmitt
2020-09-01  7:55 Alan Schmitt
2020-08-18  7:25 Alan Schmitt
2020-07-28 16:57 Alan Schmitt
2020-07-21 14:42 Alan Schmitt
2020-07-14  9:54 Alan Schmitt
2020-07-07 10:04 Alan Schmitt
2020-06-30  7:00 Alan Schmitt
2020-06-16  8:36 Alan Schmitt
2020-06-09  8:28 Alan Schmitt
2020-05-19  9:52 Alan Schmitt
2020-05-12  7:45 Alan Schmitt
2020-05-05  7:45 Alan Schmitt
2020-04-28 12:44 Alan Schmitt
2020-04-21  8:58 Alan Schmitt
2020-04-14  7:28 Alan Schmitt
2020-04-07  7:51 Alan Schmitt
2020-03-31  9:54 Alan Schmitt
2020-03-24  9:31 Alan Schmitt
2020-03-17 11:04 Alan Schmitt
2020-03-10 14:28 Alan Schmitt
2020-03-03  8:00 Alan Schmitt
2020-02-25  8:51 Alan Schmitt
2020-02-18  8:18 Alan Schmitt
2020-02-04  8:47 Alan Schmitt
2020-01-28 10:53 Alan Schmitt
2020-01-21 14:08 Alan Schmitt
2020-01-14 14:16 Alan Schmitt
2020-01-07 13:43 Alan Schmitt
2019-12-31  9:18 Alan Schmitt
2019-12-17  8:52 Alan Schmitt
2019-12-10  8:21 Alan Schmitt
2019-12-03 15:42 Alan Schmitt
2019-11-26  8:33 Alan Schmitt
2019-11-12 13:21 Alan Schmitt
2019-11-05  6:55 Alan Schmitt
2019-10-15  7:28 Alan Schmitt
2019-09-03  7:35 Alan Schmitt

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=87lewayb5k.fsf@m4x.org \
    --to=alan.schmitt@polytechnique.org \
    --cc=caml-list@inria.fr \
    --cc=cwn@lists.idyll.org \
    --cc=lwn@lwn.net \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).