From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id 946985D5 for ; Tue, 6 Jul 2021 12:34:03 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.83,328,1616454000"; d="scan'208,217";a="518576128" Received: from prod-listesu18.inria.fr (HELO sympa.inria.fr) ([128.93.162.160]) by mail2-relais-roc.national.inria.fr with ESMTP; 06 Jul 2021 14:33:59 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 676B9E0C59; Tue, 6 Jul 2021 14:33:59 +0200 (CEST) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 67EAAE0035 for ; Tue, 6 Jul 2021 14:33:54 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=Pass smtp.pra=alan.schmitt@polytechnique.org; spf=Pass smtp.mailfrom=SRS0=/xfW=L6=polytechnique.org=alan.schmitt@bounces.m4x.org; spf=Pass smtp.helo=postmaster@mx1.polytechnique.org IronPort-PHdr: =?us-ascii?q?A9a23=3A1jgrVx1CqchMmF1NsmDOGwIyDhhOgF0UFjAc5pd?= =?us-ascii?q?vsb9SaKPrp82kYBaHo601xweXFcWDsrQY0ruQ6/ihEUU7or+5+EgYd5JNUxJXw?= =?us-ascii?q?e43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgR?= =?us-ascii?q?pOOv1BpTSj8Oq3Oyu5pHfeQpFiCShbb9oMBm6sQrdutUXjIB/Lqo91gbFrmFHd?= =?us-ascii?q?uhLwW5kP06fkwr56syt4JNt7iNctu47+cVdS6v6ZaM4TbJZDDQiLW844dDguAf?= =?us-ascii?q?AQwWS+HYSS30anRVUDQfL6hH6RYrxvTDhtuVhwimaPNb5Qq4yVD+/8qpkUh7oi?= =?us-ascii?q?CMANz4k7GHaj9F7gaxHrB69oRF03onbbpyINPplZqPSY88VRXZCUMZUWCxPDIS?= =?us-ascii?q?8b44VAOoAO+ZTso3xqlUSoRe7AwSgBODhyjlWhn/3xq060v8uEQXY0wc9EdMOt?= =?us-ascii?q?27Uo8juNKwPVey4wrXEwTDFYvhL2zny9ZLIfwghr/+SQLx+f8nfxkYzGA7elFq?= =?us-ascii?q?ctZboMimJ2ugRsWWW6fdrW+K1i24grgF8uiSixsM2hYnPm4kb10zL9SV8wIY0O?= =?us-ascii?q?d24VFNwbNm+H5tUrS6aMZF6Qtg+TGFovSY6y6EGuYKgcSgSz5Qnwx7ea+CZfIe?= =?us-ascii?q?U4hLjUueRIS5lhH17Yr6/gAyy8Ue5x+D6S8K730pEoDBfndnQqnACyQbT6s6fR?= =?us-ascii?q?/dj8Uqs1zaC2h7O5+xLLk45lKjWJpEuzLMsipYeslrPEjH4lkj1kaObeUUp9+u?= =?us-ascii?q?s5urpbbvquJ+SOpJ3hw3gMqkjnNG0D+o/MggLRWeb+OK82aX7/ULnXLVKj+E2n?= =?us-ascii?q?bfBsJDdIMQbo7C2DxVT0ok99xazFzCm38gCknkCKFJJYhWHj5LmO13WL/D4DOu?= =?us-ascii?q?/g1C2nzhw3fzJIrrhApDVInjMkbfhYbZ961NHxwYp0d9f4JdUBqkbIPL0QUDxq?= =?us-ascii?q?cbYAgUlPAyzxObnEM1x1pkZWW2UH6+ZKrnesV6P5u43JemMa44VtCzjJPg4//L?= =?us-ascii?q?ugn45mUMdfam0xpQbcmq0EehhI0WceXbjnskOEX0QsQo7TezllF2CXiRPaHaxQ?= =?us-ascii?q?a08/Cs3B56hDYfGXoytm72B3Ci9HpJMYmBGEUqDEXH1eIWYW/cMcjydLdV8nTw?= =?us-ascii?q?fT7SuV4gh1RS2uADg0bpmIevU+jMCuZLkzth16PXflRAv+j10C8Sd13uBT2Zun?= =?us-ascii?q?mMHQTI9waNxoVRlx1uez6R1h+ZUGcFP6/5GSAs3O4LQw/Z0Bt39Qg7NY9mEREu?= =?us-ascii?q?8Ttm4ATw8Qcg9z8ISb0pnBtmvjAzP0iy3CLEPjbOLHoY78qfE0njxOcl9z3HG2?= =?us-ascii?q?bEkj1gpX8dDL3Wmhql79wnTG47GjVmWl6asdaQdxS7N6XmMwXCJvEFCXw58SaT?= =?us-ascii?q?FXXYBaUvKtdn1+13OQru0Bbg6LgdMxtSOJ6VWZtHzg1hLS+/vONHEbGKwn2ewC?= =?us-ascii?q?wyIxrSJbIfyZmsTwDjTBFQcngwI8neGOwgxCz+nrW/fFDFuDVXvY0fs8Olitny?= =?us-ascii?q?0Uk80zweLb014yrq65AQZhfuGS/Mcxr8LoiMhpC9yHFqnxNLZF9qApw9gfKVAf?= =?us-ascii?q?dMw+0xI1WXEtwx7IpOvMbtiikQbcwl4sELizRJ3Cp9PkcQytnMl0BJyKb6E0FN?= =?us-ascii?q?Gbz6XwYr/OrjTKmXr+BCvarXW2k3F3daN+qYP7ew4pE/5sAGoEEoi6XRn3MNP3?= =?us-ascii?q?3uS/JWZRDYVBNj1TUB9v0x+uLfyZjY7oYXZySsoeeO/rTmIk5p9D/Qj4hKhZMt?= =?us-ascii?q?EdqKIBQv2VcoACJ7qYOcjnlzsahMfIMhT8rQ1NoWobaiowqmuac9klTTutm9H5?= =?us-ascii?q?YFhzgrY/i51TKjT1JYAwu2E9hOAUybggVyhtMHuhI0CYisdSDnsgRP4DZJcM/U?= =?us-ascii?q?hNb0ADn2jdpPvrj2br4bqX29E+VWjAVIfxcLvfgCdPQWVNeJ430MKp3eqgm29k?= =?us-ascii?q?ywylCsm/PP3NM3mxvS7MgIAPn9XSWJii1b1PIXyiMoVDhHAUg=3D=3D?= IronPort-HdrOrdr: =?us-ascii?q?A9a23=3AEitPMa4Rzs9RXJVXbgPXwM/XdLJyesId70hD?= =?us-ascii?q?6qkRc3xom6Oj+PxG8M5w6faWslcssRMb9+xoUZPoKRjhHPVOjbX5U43OYCDW/E?= =?us-ascii?q?OWaKti4YHhzzCIIVycysdtkYF6fexbAN30ZGIK6PoSDTPIceod/A=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CAAgByTORgfSIeaIFahAVTRwFkVzoxh?= =?us-ascii?q?EiBX4cliFGBE4IUhW6GUod1hBCBEQNPEAEDAQ0qAQ4FAQIEAQGDHoQnAh4GAQU?= =?us-ascii?q?zEwIEFQEBBQEBAQIBAwMEARMBAQ8UCEOFaA2COAwMA4N3AwEYAQgKQAceIwMUA?= =?us-ascii?q?QYDAhEBFwEUChcBEhqCITeDBwUKinucCoEygQGDTAGETYFjDQIUgQAXhWxTOg4?= =?us-ascii?q?BgmgIg3ACJxCBVUSBFYIkSgduggNfAQEBAQGBIwQUAQEIgy8Xgk0Egh0vDjgIL?= =?us-ascii?q?B8LAgEGBxsMARMIDwEEEAwCNiMIDQEHAxkZBA0KFgYuCwsCLQORHA8li2+KK5Q?= =?us-ascii?q?yLAeDJIEsBguHFAU6gRWHN4MugVGHdoEXgkuBRooAlwMhlVeCGoZPCH0FCYIvh?= =?us-ascii?q?DiOZycEHBGEfoIUKoFqDAczGjBDgmkJYA6IIIYLFoNOEHGBY4F1O4Ijgyk/MgI?= =?us-ascii?q?BATQCBgEJAQEDCXUBAQUTCwGIJV4BAQ?= X-IPAS-Result: =?us-ascii?q?A0CAAgByTORgfSIeaIFahAVTRwFkVzoxhEiBX4cliFGBE4I?= =?us-ascii?q?UhW6GUod1hBCBEQNPEAEDAQ0qAQ4FAQIEAQGDHoQnAh4GAQUzEwIEFQEBBQEBA?= =?us-ascii?q?QIBAwMEARMBAQ8UCEOFaA2COAwMA4N3AwEYAQgKQAceIwMUAQYDAhEBFwEUChc?= =?us-ascii?q?BEhqCITeDBwUKinucCoEygQGDTAGETYFjDQIUgQAXhWxTOg4BgmgIg3ACJxCBV?= =?us-ascii?q?USBFYIkSgduggNfAQEBAQGBIwQUAQEIgy8Xgk0Egh0vDjgILB8LAgEGBxsMARM?= =?us-ascii?q?IDwEEEAwCNiMIDQEHAxkZBA0KFgYuCwsCLQORHA8li2+KK5QyLAeDJIEsBguHF?= =?us-ascii?q?AU6gRWHN4MugVGHdoEXgkuBRooAlwMhlVeCGoZPCH0FCYIvhDiOZycEHBGEfoI?= =?us-ascii?q?UKoFqDAczGjBDgmkJYA6IIIYLFoNOEHGBY4F1O4Ijgyk/MgIBATQCBgEJAQEDC?= =?us-ascii?q?XUBAQUTCwGIJV4BAQ?= X-IronPort-AV: E=Sophos;i="5.83,328,1616454000"; d="scan'208,217";a="387260667" X-MGA-submission: =?us-ascii?q?MDGyf/dGTL4rwcxW5+OFEfnD1qbab46DFQ7Gde?= =?us-ascii?q?Ej7YQQZkbJDYwkqzDR7IKf7045YGv3Lc3Y2CRKg3nUFLs1HimJf7XNZi?= =?us-ascii?q?bwLZD7hT+7KHusA7e8vwaQfyU6R+XHPo6z5gyr6e9fNvSeASmiZz6r/Q?= =?us-ascii?q?2azNf0D1XPrkMDJnl4bhNVnA=3D=3D?= Received: from mx1.polytechnique.org ([129.104.30.34]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 06 Jul 2021 14:33:50 +0200 Received: from set (set.irisa.fr [131.254.10.170]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ssl.polytechnique.org (Postfix) with ESMTPSA id D652556482D; Tue, 6 Jul 2021 14:33:48 +0200 (CEST) From: Alan Schmitt To: "lwn" , "cwn" , caml-list@inria.fr Date: Tue, 06 Jul 2021 14:33:43 +0200 Message-ID: <878s2j8vvc.fsf@m4x.org> MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="=-=-=" X-AV-Checked: ClamAV using ClamSMTP at svoboda.polytechnique.org (Tue Jul 6 14:33:49 2021 +0200 (CEST)) X-Spam-Flag: No, tests=bogofilter, spamicity=0.003375, queueID=3BBA956482E X-Org-Mail: alan.schmitt.1995@polytechnique.org Subject: [Caml-list] Attn: Development Editor, Latest OCaml Weekly News Reply-To: Alan Schmitt X-Loop: caml-list@inria.fr X-Sequence: 18538 Errors-To: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Help: List-Subscribe: List-Unsubscribe: List-Post: List-Owner: List-Archive: Archived-At: --=-=-= Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Hello Here is the latest OCaml Weekly News, for the week of June 29 to July 06, 2021. Table of Contents =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80 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 Old CWN LibreRef - LablGtk-based Digital Reference Tool Application =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95= =90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90= =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95= =90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90= =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90 Archive: Kiran Gopinathan announced =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80= =E2=94=80 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 established. [gitlab] [github mirror] u2f - universal second factor =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95= =90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90= =E2=95=90=E2=95=90=E2=95=90=E2=95=90 Archive: Hannes Mehnert announced =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80 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 =E2=80=93 please let us know if you run into any trouble, or open an issu= e on the GitHub repository. One question though: we're unable to generate the documentation from the mli =E2=80=93 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 skolem.tech. Reproducible OPAM packages / MirageOS =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95= =90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90= =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90 Archive: Hannes Mehnert announced =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80 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 =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90 Archive: Emilio Jes=C3=BAs Gallego Arias announced =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80= =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80 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: =E2=80=A2 Add `(enabled_if ...)' to `(mdx ...)' (, @emillon) =E2=80=A2 Add support for instrumentation dependencies (, fixes , @nojb) =E2=80=A2 Add the possibility to use `locks' with the cram tests stanza (, @voodoos) =E2=80=A2 Allow to set up merlin in a variant of the default context (, @TheLortex, @voodoos) =E2=80=A2 Add `(package ...)' to `(mdx ...)' (, fixes , @emillon) =E2=80=A2 Handle renaming of `coq.kernel' library to `coq-core.kernel' in= Coq 8.14 (, @proux01) =E2=80=A2 Fix generation of merlin configuration when using `(include_sub= dirs unqualified)' on Windows (, @nojb) =E2=80=A2 Fix bug for the install of Coq native files when using `(include_subdirs qualified)' (, @ejgallego) =E2=80=A2 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) =E2=80=A2 Fix issue where Dune would ignore `(env ... (coq (flags ...)))' declarations appearing in `dune' files (, fixes , @ejgallego @rgrinberg) =E2=80=A2 Disable some warnings on Coq 8.14 and `(lang coq (>=3D 0.3))' d= ue to the rework of the Coq "native" compilation system (, @ejgallego) =E2=80=A2 Fix a bug where instrumentation flags would be added even if the instrumentatation was disabled (@nojb, ) =E2=80=A2 Fix : option `-p' ta= kes now precedence on environement variable `DUNE_PROFILE' (, , @bobot, reported by @dra27 ) =E2=80=A2 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 ) =E2=80=A2 Fix multiple issues in the sites feature (, @bobot, reported by @Lelio-Brun , by @Kakadu , by @toots ) Hardcaml MIPS CPU Learning Project and Blog =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95= =90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90= =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95= =90=E2=95=90 Archive: "Alexander (Sasha) Skvortsov announced =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80= =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80 Tl;dr: I=E2=80=99m [writing a blog] about making a MIPS CPU in Hardcaml. Hi! My name is Sasha, and I=E2=80=99m 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=E2=80=99ve 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=E2=80=99re still working on the pro= ject, 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=E2=80= =99s [up on GitHub]. We=E2=80=99ve written some blog posts about our project: 1. [Some more background on what we=E2=80=99re 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 generation] 5. [How to split Hardcaml circuits into multiple modules] There=E2=80=99s also a few more that we=E2=80=99ve written code for, but = are still drafting blog posts about: =E2=80=A2 How to work with memory in Hardcaml =E2=80=A2 How to design stateful, sequential circuits in Hardcaml =E2=80=A2 A safer design pattern for Hardcaml circuits I=E2=80=99m 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=E2=80=99re doing and why] [An ELI5 overview of how hardware, and pipelined CPUs in particular, work] [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 generation] [How to split Hardcaml circuits into multiple modules] dune-release 1.5.0 =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95= =90=E2=95=90 Archive: Nathan Rebours announced =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80 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: =E2=80=A2 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. =E2=80=A2 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 this. 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 =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90 Archive: Namdak Tonpa announced =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80 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=C3=B6f 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, Sattler]. 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]. =E2=94=8C=E2=94=80=E2=94=80=E2=94=80=E2=94=80 =E2=94=82 $ opam install anders =E2=94=82 $ anders =E2=94=82 Anders theorem prover [PTS][MLTT][CCHM-4][HTS]. =E2=94=82=20 =E2=94=82 invoke =3D anders | anders list =E2=94=82 list =3D [] | command list =E2=94=82 command =3D check filename | lex filename =E2=94=82 | parse filename | help =E2=94=82 | cubicaltt filename | girard =E2=94=82 | trace =E2=94=94=E2=94=80=E2=94=80=E2=94=80=E2=94=80 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] Old CWN =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90 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] [the archive] [RSS feed of the archives] [online] [Alan Schmitt] --=-=-= Content-Type: text/html; charset=utf-8 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable OCaml Weekly News

OCaml Weekly News

Previous Week<= /a> Up Next Week

Hello

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

LibreRef - LablGtk-based Digital Reference Tool Application

Archive: https://discuss.ocaml.org/t/ann-= libreref-lablgtk-based-digital-reference-tool-application/8077/1

Kiran Gopinathan announced

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

3D"b=

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 e= xamples of it in action:

3D"126997c61b83=

3D"49b11ef943e4=

Overall, getting LablGtk to work was fairly straightforward, although the d= ocumentation 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 r= elying 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 & LinuxDepl= oy toolchain to work well with the resulting binary (admittedly I've only tested it with two devices so fa= r), and it meant that I could publish the program without having to ask people to setup the full OC= aml & Opam toolchain, which would probably be a large ask.

As for the implementation, I think it was fairly elegant (if I say so mysel= f :slight_smile:), although I may have gone overboard with functors (see this higher-order functor in t= he GUI interface: https://gitlab.com/gopiandcode/libre-ref/-/blob/master/gui.mli#L175) and some aspects of the separation of concerns weren't so well established.

u2f - universal second factor

Archive: https://discuss.ocaml.org/t/ann-u2f-universal-second-factor/80= 78/1

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 s= pecial device (yubikey etc.). The device does challenge-response authentication with the server us= ing 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 auth= orization requests with responses thereof. Please have a look at https://github.com/roburio/u2f 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 https://u2f-demo.robur.co= op – 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 ml= i – 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 skolem.tech.

Reproducible OPAM packages / MirageOS

Archive: https://discuss.ocaml.org/t/reproducible-opam-packages-mir= ageos/8079/1

Hannes Mehnert announced

we are pleased to announce reproducible binary images for MirageOS unikerne= ls (see the blog post at https://hannes.robur.coo= p/Posts/Deploy). The binaries are located at https://builds.robur.coop (all components are open source and linked from the page).

Additionally, the required tools to achieve reproducible builds are release= d as binary packages for various operating systems as well on the same site. They are used by the in= frastructure to run daily builds (always with the HEAD of opam-repository to not loose any updates / = new releases). The custom overlay https://git.r= obur.io/robur/unikernel-repo is used that adds some development package= s.

Happy to hear your thoughts and feedback here. (Earlier post https://discuss.ocaml.org/t/reproducible-builds-with-oca= ml-opam-and-mirageos/4877)

This work was funded by the NGI Pointer<= /a> project "Funding The Next Generation Ecosystem of Internet Architects".

Dune 2.9.0

Archive: http= s://discuss.ocaml.org/t/ann-dune-2-9-0/8087/1

Emilio Jes=C3=BAs 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 r= elease 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:

Hardcaml MIPS CPU Learning Project and Blog

Archive: https://discuss.ocaml.org/t/hardcaml-mips-cpu-lear= ning-project-and-blog/8088/1

"Alexander (Sasha) Skvortsov announced

Tl;dr: I=E2=80=99m writing a blog about making a MIPS CPU in Hardcaml.

Hi! My name is Sasha, and I=E2=80=99m a student at Penn State majoring in C= S and Math. Last semester, I took a computer engineering class where we built a pipelined MIPS CPU in Verilog a= s 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=E2=80=99ve been wanting to learn OCaml for a while.

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

We=E2=80=99ve written some blog posts about our project:

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

There=E2=80=99s also a few more that we=E2=80=99ve written code for, but ar= e 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=E2=80=99m new to both OCaml and blogging, and this has definitely been a = fun experience so far! Would love to hear any feedback / comments.

dune-release 1.5.0

Archive: https://discuss.ocaml.org/t/ann-dune-release-1-5-0/8095/1

Nathan Rebours announced

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

It has been quite a while since the last release so there are numerous chan= ges 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 wil= l undraft both and update the opam file's url.src field accord= ingly. We believe this feature will prove helpful to maintainers of tools s= uch as dune which releases are often watched by distribution m= aintainers. Draft releases allow you to wait until you have opam-repository= 's CI approval to actually create a GH release that will notify anyone watc= hing the repository. This feature is still a bit experimental, we have idea= s 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 kno= w 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 buildi= ng 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 th= is 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 anno= unced 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 seeml= ess 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 conf= igurable 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 repositori= es. 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 s= uch as handling gitlab hosted repositories but we want to make sure our main user base is happy wi= th the tool before adding this.

We'll communicate a bit more on our plans for 2.0 in the next few months. O= ur 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 h= appy releases!

anders 0.7.1

Archive: ht= tps://discuss.ocaml.org/t/ann-anders-0-7-1/8098/1

Namdak Tonpa announced

The HTS language proposed by Voevodsky exposes two different presheaf model= s of type theory: the inner one is homotopy type system presheaf that models HoTT and the outer one is = traditional Martin-L=C3=B6f 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-t= heoretical and homotopical languages was continued in 2LTT [Anenkov, Capriotti, Kraus, Sattler].

While we are on our road to HTS with Lean-like tactic language, currently w= e are at the stage of regular cubical (HoTT) type checker with CHM-style primitives, or more gene= ral CCHM type checker. You may try it at Github: groupo= id/anders. 

$ opam install anders
$ anders
Anders theorem prover [PTS][MLTT][CCHM-4][HTS].

   invoke =3D anders | anders list
     list =3D [] | command list
  command =3D check filename     | lex filename
          | parse filename     | help
          | cubicaltt filename | girard
          | trace

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

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 loo= k at the archive or the <= a href=3D"https://alan.petitepomme.net/cwn/cwn.rss">RSS feed of the archive= s.

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

--=-=-=--