caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Alan Schmitt <>
To: "lwn" <>, "cwn"  <>,
Subject: [Caml-list] Attn: Development Editor, Latest OCaml Weekly News
Date: Tue, 06 Jul 2021 14:33:43 +0200	[thread overview]
Message-ID: <> (raw)

[-- Attachment #1: Type: text/plain, Size: 18790 bytes --]


Here is the latest OCaml Weekly News, for the week of June 29 to July
06, 2021.

Table of Contents

LibreRef - LablGtk-based Digital Reference Tool Application
u2f - universal second factor
Reproducible OPAM packages / MirageOS
Dune 2.9.0
Hardcaml MIPS CPU Learning Project and Blog
dune-release 1.5.0
anders 0.7.1

LibreRef - LablGtk-based Digital Reference Tool Application


Kiran Gopinathan announced

  I'm not sure if this is that close to the typical uses of OCaml, but
  posting this here just in case anyone was interested in another
  end-user facing application using LablGtk.


        LibreRef is a free as in freedom digital referencing tool
        for artists.

  It's written in OCaml using LablGtk and Cairo to implement the GUI.

  You can find the source code at: [gitlab] ([github mirror])

  A picture is worth a thousand words, so before I continue, here are a
  few examples of it in action:



  Overall, getting LablGtk to work was fairly straightforward, although
  the documentation was a bit lacking (although the same might be said
  of Gtk itself).

  I was able to piece together the correct uses of most of the API calls
  by relying on either the examples from the repository or by
  translating snippets of code from online back into LablGtk.

  As for deploying it as an application, I found the AppImage &
  LinuxDeploy toolchain to work well with the resulting binary
  (admittedly I've only tested it with two devices so far), and it meant
  that I could publish the program without having to ask people to setup
  the full OCaml & Opam toolchain, which would probably be a large ask.

  As for the implementation, I think it was fairly elegant (if I say so
  myself :slight_smile:), although I may have gone overboard with
  functors (see this higher-order functor in the GUI interface:
  and some aspects of the separation of concerns weren't so well

[gitlab] <>

[github mirror] <>

u2f - universal second factor


Hannes Mehnert announced

  it is our pleasure to announce the just released opam package u2f,
  which is a server side implementation of the FIDO standard for
  two-factor authentication using a special device (yubikey etc.). The
  device does challenge-response authentication with the server using
  public key cryptography.

  The implementation is stateless and does not use a specific IO
  library, but only achieves the logic for constructing a registration
  request, verifying a response thereof, and authorization requests with
  responses thereof. Please have a look at
  <> if you're interested. It is licensed
  under the permissive 2-clause BSD license.

  We use this library in an example server (in the `bin' directory) that
  uses dream. The live server is online at <>
  – please let us know if you run into any trouble, or open an issue on
  the GitHub repository.

  One question though: we're unable to generate the documentation from
  the mli – already asked on discord with no result. Anyone with a
  better understanding of odoc etc. can take a look why `dune build
  @doc' outputs a nearly empty file? Thanks a lot :)

  The development was sponsored by

Reproducible OPAM packages / MirageOS


Hannes Mehnert announced

  we are pleased to announce reproducible binary images for MirageOS
  unikernels (see the blog post at
  <>). The binaries are located at
  <> (all components are open source and linked
  from the page).

  Additionally, the required tools to achieve reproducible builds are
  released as binary packages for various operating systems as well on
  the same site. They are used by the infrastructure to run daily builds
  (always with the HEAD of opam-repository to not loose any updates /
  new releases). The custom overlay
  <> is used that adds some
  development packages.

  Happy to hear your thoughts and feedback here. (Earlier post

  This work was funded by the [NGI Pointer] project "Funding The Next
  Generation Ecosystem of Internet Architects".

[NGI Pointer] <>

Dune 2.9.0

  Archive: <>

Emilio Jesús Gallego Arias announced

  Dear all, on behalf of the Dune team I'm pleased to announce the
  release of Dune 2.9.0. This is the last release on the Dune 2.x series
  and could be considered a maintenance release as it mostly consists on
  bug fixes and miscellaneous tweaks and features for sites,
  instrumentation, and mdx support.

  Please find the full list of changes below:
  • Add `(enabled_if ...)' to `(mdx ...)'
    (<>, @emillon)

  • Add support for instrumentation dependencies
    (<>, fixes
    <>, @nojb)

  • Add the possibility to use `locks' with the cram tests stanza
    (<>, @voodoos)

  • Allow to set up merlin in a variant of the default context
    (<>, @TheLortex, @voodoos)

  • Add `(package ...)' to `(mdx ...)'
    (<>, fixes
    <>, @emillon)

  • Handle renaming of `coq.kernel' library to `coq-core.kernel' in Coq
    8.14 (<>, @proux01)

  • Fix generation of merlin configuration when using `(include_subdirs
    unqualified)' on Windows (<>,

  • Fix bug for the install of Coq native files when using
    `(include_subdirs qualified)'
    (<>, @ejgallego)

  • Allow users to specify install target directories for `doc' and
    `etc' sections. We add new options `--docdir' and `--etcdir' to both
    Dune's configure and `dune install'
    command. (<>, fixes
    <>, @ejgallego, thanks to
    @JasonGross for reporting this issue)

  • Fix issue where Dune would ignore `(env ... (coq (flags ...)))'
    declarations appearing in `dune' files
    (<>, fixes
    <>, @ejgallego @rgrinberg)

  • Disable some warnings on Coq 8.14 and `(lang coq (>= 0.3))' due to
    the rework of the Coq "native" compilation system
    (<>, @ejgallego)

  • Fix a bug where instrumentation flags would be added even if the
    instrumentatation was disabled (@nojb,

  • Fix <>: option `-p' takes
    now precedence on environement variable `DUNE_PROFILE'
    <>, @bobot, reported by
    @dra27 <>)

  • Fix installation with opam of package with dune sites. The
    `.install' file is now produced by a local `dune install' during the
    build phase (<>,
    <>, @bobot, reported by
    @kit-ty-kate <>)

  • Fix multiple issues in the sites feature
    <> @bobot, reported by
    @Lelio-Brun <>, by @Kakadu
    <>, by @toots

Hardcaml MIPS CPU Learning Project and Blog


"Alexander (Sasha) Skvortsov announced

  Tl;dr: I’m [writing a blog] about making a MIPS CPU in Hardcaml.

  Hi! My name is Sasha, and I’m a student at Penn State majoring in CS
  and Math. Last semester, I took a computer engineering class where we
  built a pipelined MIPS CPU in Verilog as a semester-long project. I
  enjoyed the class, but a lot of frustration came from Verilog itself.

  A few months ago, I came across the [Signals and Threads Programmable
  Hardware episode]. I really liked the idea of [Hardcaml]: a library to
  write and test hardware designs in OCaml. Representing circuits as
  functions felt like a good abstraction, and I’ve been wanting to learn
  OCaml for a while.

  So this summer, a friend and I are rewriting the Verilog MIPS CPU we
  made last semester into Hardcaml.  We’re still working on the project,
  but have made some good progress and wanted to share it in case anyone
  finds it interesting / useful. If anyone wants to take a look, it’s
  [up on GitHub].

  We’ve written some blog posts about our project:

  1. [Some more background on what we’re doing and why]
  2. [An ELI5 overview of how hardware, and pipelined CPUs in
     particular, work]
  3. [Another high-level overview of Verilog, hardware design, FPGAs,
     and why I think OCaml might be a great fit for hardware design]
  4. [How to set up a Hardcaml project, including testing and Verilog
  5. [How to split Hardcaml circuits into multiple modules]

  There’s also a few more that we’ve written code for, but are still
  drafting blog posts about:

  • How to work with memory in Hardcaml
  • How to design stateful, sequential circuits in Hardcaml
  • A safer design pattern for Hardcaml circuits

  I’m new to both OCaml and blogging, and this has definitely been a fun
  experience so far! Would love to hear any feedback / comments.

[writing a blog] <>

[Signals and Threads Programmable Hardware episode]

[Hardcaml] <>

[up on GitHub] <>

[Some more background on what we’re doing and why]

[An ELI5 overview of how hardware, and pipelined CPUs in particular,

[Another high-level overview of Verilog, hardware design, FPGAs, and why
I think OCaml might be a great fit for hardware design]

[How to set up a Hardcaml project, including testing and Verilog

[How to split Hardcaml circuits into multiple modules]

dune-release 1.5.0

  Archive: <>

Nathan Rebours announced

  On behalf of the dune-release team I'm pleased to announce that we're
  releasing dune-release.1.5.0.

  It has been quite a while since the last release so there are numerous
  changes and improvements in this one, along with a lot of bug fixes.

  The two main new features in 1.5.0 are:
  • A draft release mode that creates a draft Github release and a draft
    PR to opam-repository. It comes with an `undraft' command that will
    undraft both and update the opam file's `url.src' field
    accordingly. We believe this feature will prove helpful to
    maintainers of tools such as `dune' which releases are often watched
    by distribution maintainers. Draft releases allow you to wait until
    you have opam-repository's CI approval to actually create a GH
    release that will notify anyone watching the repository. This
    feature is still a bit experimental, we have ideas on how to improve
    it but we wanted to get a first version out to collect feedback on
    how it is used and what you folks expect from it.
  • A `check' command that you can run ahead of a release to know if
    dune-release has all the information it needs in the repository,
    along with running the lint, build and test checks it normally runs
    after building the tarball. We're aware that it can be frustrating
    to see dune-release fail right in the middle of the release
    process. We're trying to improve this situation and this is a first
    step in that direction.

  You can see the full changelog [here]

  You'll note we also deprecated a few features such as delegates (as we
  announced in [this post]), opam 1.x and the `--user' option and
  corresponding config file field.  This release is likely to be the
  last 1.x release of `dune-release' except for important bug fixes as
  we'll start working on 2.0 soon.

  Our main goals for 2.0 are to make the experience for github users as
  seemless as possible. We want the tool to do the right thing for those
  users without them having to configure anything. Delegates got in the
  way there and that's why we're removing them.  We do care about our
  non github users and we've worked on making it as configurable as
  possible so that you can integrate it in your release workflow. The
  situation should already have improved quite a bit with this release
  as we fixed several bugs for non github hosted repositories. We want
  to make sure that these users will be happy with dune-release 2.0 as
  well.  Hopefully in the future dune-release will support other release
  workflows such as handling gitlab hosted repositories but we want to
  make sure our main user base is happy with the tool before adding

  We'll communicate a bit more on our plans for 2.0 in the next few
  months. Our hope is that it will hit opam before the end of this year.

  We hope that you'll like this new version and wish you all successful
  and happy releases!

[here] <>

[this post]

anders 0.7.1

  Archive: <>

Namdak Tonpa announced

  The HTS language proposed by Voevodsky exposes two different presheaf
  models of type theory: the inner one is homotopy type system presheaf
  that models HoTT and the outer one is traditional Martin-Löf type
  system presheaf that models set theory with UIP. The motivation behind
  this doubling is to have an ability to express semisemplicial
  types. Theoretical work on merging meta-theoretical and homotopical
  languages was continued in [2LTT] [Anenkov, Capriotti, Kraus,

  While we are on our road to HTS with Lean-like tactic language,
  currently we are at the stage of regular cubical (HoTT) type checker
  with CHM-style primitives, or more general CCHM type checker. You may
  try it at Github: [groupoid/anders].

  │ $ opam install anders
  │ $ anders
  │ Anders theorem prover [PTS][MLTT][CCHM-4][HTS].
  │    invoke = anders | anders list
  │      list = [] | command list
  │   command = check filename     | lex filename
  │           | parse filename     | help
  │           | cubicaltt filename | girard
  │           | trace

  Anders is idiomatic and educational. We carefully draw the favourite
  Lean-compatible syntax to fit 130 LOC in Menhir, the MLTT core (based
  on Mini-TT) is 500 LOC and pretypes presheaf is another 500 LOC.

[2LTT] <>

[groupoid/anders] <>


  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

  If you also wish to receive it every week by mail, you may subscribe

  [Alan Schmitt]

[send me a message] <>

[the archive] <>

[RSS feed of the archives] <>

[online] <>

[Alan Schmitt] <>

[-- Attachment #2: Type: text/html, Size: 31723 bytes --]

             reply	other threads:[~2021-07-06 12:34 UTC|newest]

Thread overview: 112+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2021-07-06 12:33 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-12  8:10 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-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:

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

  git send-email \ \ \ \ \ \

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