We shall finish the semester with a "Every proof assistant" talk by William Bowman. Note that we start an hour later than usual, at 17:00 UTC+2.

Cur: Designing a less devious proof assistant

Time: Thursday, June 25, 2020 from 17:00 to 18:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: William J. Bowman (University of British Columbia)
Proof assistant: Cur

Abstract:

Dijkstra said that our tools can have a profound and devious influence on o…

We shall finish the semester with a "Every proof assistant" talk by William Bowman. Note that we start an hour later than usual, at 17:00 UTC+2.

Cur: Designing a less devious proof assistant

Time: Thursday, June 25, 2020 from 17:00 to 18:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: William J. Bowman (University of British Columbia)
Proof assistant: Cur

Abstract:

Dijkstra said that our tools can have a profound and devious influence on our thinking. I find this especially true of modern proof assistants, with "devious" out-weighing "profound". Cur is an experiment in design that aims to be less devious. The design emphasizes language extension, syntax manipulation, and DSL construction and integration. This enables the user to be in charge of how they think, rather than requiring the user to contort their thinking to that of the proof assistant. In this talk, my goal is to convince you that you want similar capabilities in a proof assistant, and explain and demonstrate Cur's attempt at solving the problem.

The talk video recording and slides with notes and demo code are available.

Upcoming talks: Anders Mörtberg's talk on Cubical Agda will take place in September 2020.

This week shall witness a performance by Conor McBride.

Epigram 2: Autopsy, Obituary, Apology

Time: Thursday, June 11, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Conor McBride (University of Strathclyde)
Proof assistant: Epigram 2

Abstract: "A good pilot is one with the same number of take-offs and landings." runs the old joke, which makes me a very bad pilot indeed. The Epigram 2 project was repeatedly restarted se…

This week shall witness a performance by Conor McBride.

Epigram 2: Autopsy, Obituary, Apology

Time: Thursday, June 11, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Conor McBride (University of Strathclyde)
Proof assistant: Epigram 2

Abstract: "A good pilot is one with the same number of take-offs and landings." runs the old joke, which makes me a very bad pilot indeed. The Epigram 2 project was repeatedly restarted several times in the late 2000s and never even reached cruising altitude. This talk is absolutely not an attempt to persuade you to start using it. Rather, it is an exploration of the ideas which drove it: proof irrelevant observational equality, first class datatype descriptions, nontrivial equational theories for neutral terms. We may yet live to see such things. Although the programming language elaborator never happened, the underlying proof engine was accessible via an imperative interface called "Cochon": we did manage some interesting constructions, at least one of which I can walk through. I'll also explore the reasons, human and technological, why the thing did not survive the long dark.

The video recording of the talk.

Upcoming talks:

• June 25, 2020: William J. Bowman, Cur
• July 2, 2020: Anders Mörtberg - Cubical Agda

This week the speaker will be Jon Sterling, and we are getting two proof assistants for the price of one!

redtt and the future of Cartesian cubical type theory

Time: Thursday, June 4, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Jon Sterling (Carnegie Mellon University)
Proof assistant: redtt and cooltt

Abstract: redtt is an interactive proof assistant for Cartesian cubical type theory, a version of Martin-Löf type t…

This week the speaker will be Jon Sterling, and we are getting two proof assistants for the price of one!

redtt and the future of Cartesian cubical type theory

Time: Thursday, June 4, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Jon Sterling (Carnegie Mellon University)
Proof assistant: redtt and cooltt

Abstract: redtt is an interactive proof assistant for Cartesian cubical type theory, a version of Martin-Löf type theory featuring computational versions of function extensionality, higher inductive types, and univalence. Building on ideas from Epigram, Agda, and Idris, redtt introduces a new cubical take on interactive proof development with holes. We will first introduce the basics of cubical type theory and then dive into an interactive demonstration of redtt’s features and its mathematical library.

After this we will catch a first public glimpse of the future of redtt, a new prototype that our team is building currently code-named “cooltt”: cooltt introduces syntax to split on disjunctions of cofibrations in arbitrary positions, implementing the full definitional eta law for disjunction. While cooltt is still in the early stages, it already has full support for univalence and cubical interactive proof development.

The video recording of the talk.

Upcoming talks:

• June 11, 2020: Conor McBride - Epigram 2
• June 25, 2020: William J. Bowman, Cur
• July 2, 2020: Anders Mörtberg - Cubical Agda

We are marching on with the Every proof assistant series!

Mechanizing Meta-Theory in Beluga

Time: Thursday, May 28, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Brigitte Pientka (McGill University)
Proof assistant: Beluga

Abstract: Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. In this talk, I will …

We are marching on with the Every proof assistant series!

Mechanizing Meta-Theory in Beluga

Time: Thursday, May 28, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Brigitte Pientka (McGill University)
Proof assistant: Beluga

Abstract: Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. In this talk, I will survey the proof environment Beluga. To specify formal systems and represent derivations within them, Beluga relies on the logical framework LF; to reason about formal systems, Beluga provides a dependently typed functional language for implementing (co)inductive proofs about derivation trees as (co)recursive functions following the Curry-Howard isomorphism. Key to this approach is the ability to model derivation trees that depend on a context of assumptions using a generalization of the logical framework LF, i.e. contextual LF which supports first-class contexts and simultaneous substitutions.

Our experience demonstrated that Beluga enables direct and compact mechanizations of the meta-theory of formal systems, in particular programming languages and logics.

The video recording of the talk.

Upcoming talks:

• June 4, 2020: Jon Sterling - redtt
• June 11, 2020: Conor McBride - Epigram 2
• June 25, 2020: William J. Bowman, Cur
• July 2, 2020: Anders Mörtberg - Cubical Agda

We are pleased to announce that TLS 1.3 support for MirageOS is available. With mirage 3.7.7 and tls 0.12 the Transport Layer Security (TLS) Protocol Version 1.3 is available in all MirageOS unikernels, including on our main website. If you're reading this, you've likely established a TLS 1.3 connection already :)

Getting there was some effort: we now embed the Coq-verified fiat library (from fiat-crypto) for the P-256 elliptic curve, and the F*-verified hacl library (from Project Everest) for t…

We are pleased to announce that TLS 1.3 support for MirageOS is available. With mirage 3.7.7 and tls 0.12 the Transport Layer Security (TLS) Protocol Version 1.3 is available in all MirageOS unikernels, including on our main website. If you're reading this, you've likely established a TLS 1.3 connection already :)

Getting there was some effort: we now embed the Coq-verified fiat library (from fiat-crypto) for the P-256 elliptic curve, and the F*-verified hacl library (from Project Everest) for the X25519 elliptic curve to establish 1.3 handshakes with ECDHE.

Part of our TLS 1.3 stack is support for pre-shared keys, and 0 RTT. If you're keen to try these features, please do so and report any issues you encounter to our issue tracker.

We are still lacking support for RSA-PSS certificates and EC certificates, post-handshake authentication, and the chacha20-poly1305 ciphersuite. There is also a minor symbol clash with the upstream F* C bindings which we are aware of. We will continue to work on these, and patches are welcome.

I am happy to announce the next seminar in the "Every proof assistant" series.

MMT: A Foundation-Independent Logical System

Time: Thursday, May 21, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Florian Rabe (University of Erlangen)
Proof assistant: The MMT Language and System

Abstract: Logical frameworks are meta-logics for defining other logics. MMT follows this approach but abstracts even further: it avoids committin…

I am happy to announce the next seminar in the "Every proof assistant" series.

MMT: A Foundation-Independent Logical System

Time: Thursday, May 21, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Florian Rabe (University of Erlangen)
Proof assistant: The MMT Language and System

Abstract: Logical frameworks are meta-logics for defining other logics. MMT follows this approach but abstracts even further: it avoids committing to any foundational features like function types or propositions. All MMT algorithms are parametric in a set of rules, which are self-contained objects plugged in by the language designer. That results in a framework general enough to develop many formal systems including other logical frameworks in it, enabling the rapidly prototyping of new language features.

Despite this high level of generality, it is possible to develop sophisticated results in MMT. The current release includes, e.g., parsing, type reconstruction, module system, IDE-style editor, and interactive library browser. MMT is systematically designed to be extensible, providing multiple APIs and plugin interfaces, and thus provides a versatile infrastructure for system development and integration.

This talk gives an overview of the current state of MMT and its future challenges. Examples are drawn from the LATIN project, a long-running project of building a modular, highly inter-related suite of formalizations of logics and related formal systems.

The video recording of the talk.

The spring schedule of talks is planned as follows:

• May 28, 2020: Brigitte Pientka - Beluga
• June 4, 2020: Jon Sterling - redtt (to be confirmed)
• June 11, 2020: Conor McBride - Epigram 2
• June 25, 2020: William J. Bowman, Cur
• July 2, 2020: Anders Mörtberg - Cubical Agda

New release: Ocsigen Start 2.18

Ocsigen Start is a template for client-server Web and/or mobile app in OCaml or ReasonML. It contains many standard features like user management, notifications, and many code examples. Use it to learn Web/mobile development in OCaml or as a basis for your app.

Last features include:

• Demo of new Ot_tongue widget

See live examples here:

• See an online demo of the default template
• The same, as a mobile app for Android
• Be Sport is based on Ocsigen Start

New release: Ocsigen Start 2.18

Ocsigen Start is a template for client-server Web and/or mobile app in OCaml or ReasonML. It contains many standard features like user management, notifications, and many code examples. Use it to learn Web/mobile development in OCaml or as a basis for your app.

Last features include:

• Demo of new Ot_tongue widget

See live examples here:

• See an online demo of the default template
• The same, as a mobile app for Android
• Be Sport is based on Ocsigen Start Web / Android / iOS

New release: Ocsigen Start 2.18

Ocsigen Start is a template for client-server Web and/or mobile app in OCaml or ReasonML. It contains many standard features like user management, notifications, and many code examples. Use it to learn Web/mobile development in OCaml or as a basis for your app.

Last features include:

• Demo of new Ot_tongue widget

See live examples here:

• See an online demo of the default template
• The same, as a mobile app for Android
• Be Sport is based on Ocsigen Start

New release: Ocsigen Start 2.18

Ocsigen Start is a template for client-server Web and/or mobile app in OCaml or ReasonML. It contains many standard features like user management, notifications, and many code examples. Use it to learn Web/mobile development in OCaml or as a basis for your app.

Last features include:

• Demo of new Ot_tongue widget

See live examples here:

• See an online demo of the default template
• The same, as a mobile app for Android
• Be Sport is based on Ocsigen Start Web / Android / iOS

New release: Ocsigen Toolkit 2.7

Ocsigen Toolkit is a widget toolkit for developing mobile and Web apps with js_of_ocaml. It is designed to take advantage of Eliom’s multi-tier programming paradigm. All widgets can be created either on server or client side.

This version introduces a new widget: Ot_tongue. It is a swipable panel, coming from the bottom of the screen (or from another side). Try it online with a mobile phone in Ocsigen Start’s demo or on the app Mon club près de chez moi.

New release: Ocsigen Toolkit 2.7

Ocsigen Toolkit is a widget toolkit for developing mobile and Web apps with js_of_ocaml. It is designed to take advantage of Eliom’s multi-tier programming paradigm. All widgets can be created either on server or client side.

This version introduces a new widget: Ot_tongue. It is a swipable panel, coming from the bottom of the screen (or from another side). Try it online with a mobile phone in Ocsigen Start’s demo or on the app Mon club près de chez moi.

You can also test it on mobile apps:

• Ocsigen Start demo
• Be Sport Android / iOS

New release: Ocsigen Toolkit 2.7

Ocsigen Toolkit is a widget toolkit for developing mobile and Web apps with js_of_ocaml. It is designed to take advantage of Eliom’s multi-tier programming paradigm. All widgets can be created either on server or client side.

This version introduces a new widget: Ot_tongue. It is a swipable panel, coming from the bottom of the screen (or from another side). Try it online with a mobile phone in Ocsigen Start’s demo or on the app Mon club près de chez moi.

New release: Ocsigen Toolkit 2.7

Ocsigen Toolkit is a widget toolkit for developing mobile and Web apps with js_of_ocaml. It is designed to take advantage of Eliom’s multi-tier programming paradigm. All widgets can be created either on server or client side.

This version introduces a new widget: Ot_tongue. It is a swipable panel, coming from the bottom of the screen (or from another side). Try it online with a mobile phone in Ocsigen Start’s demo or on the app Mon club près de chez moi.

You can also test it on mobile apps:

• Ocsigen Start demo
• Be Sport Android / iOS

For a while now I have been contemplating a series of seminars titled "Every proof assistant" that would be devoted to all the different proof assistants out there. Apart from the established ones (Isabelle/HOL, Coq, Agda, Lean), there are other interesting experimental proof assistants, and some that are still under development, or just proofs of concept. I would like to know more about them, and I suspect I am not the only one.

Getting the authors of proof assistants to travel to Ljubljana …

For a while now I have been contemplating a series of seminars titled "Every proof assistant" that would be devoted to all the different proof assistants out there. Apart from the established ones (Isabelle/HOL, Coq, Agda, Lean), there are other interesting experimental proof assistants, and some that are still under development, or just proofs of concept. I would like to know more about them, and I suspect I am not the only one.

Getting the authors of proof assistants to travel to Ljubljana and giving talks at our Foundations of mathematics and theoretical computer science seminar has largely become impossible. But luckily research seminars world-wide are rapidly moving online, and so is our Foundations seminar. I am therefore delighted to announce the first "Every proof assistant" seminar:

Arend proof assistant

Time: Thursday, April 30, 2020 from 18:00 to 19:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 965 4439 5816
Speaker: Valery Isaev (JetBrains research) Proof assistant: Arend proof assistant

Abstract: I will discuss Arend, a proof assistant developed at JetBrains Research. The aim of Arend is to provide a powerful system for formalization results in homotopy type theory and in ordinary mathematics. To achieve the latter goal, we prove a flexible class system with subtyping, universe polymorphism with a powerful level inference mechanism, quotient sets with a convenient pattern matching principles for them. We also recently implemented a tactic framework which can be used to automate routine proofs and implement various EDSLs. Homotopic features of Arend include built-in universes of finite homotopy level, higher inductive types, univalence, and path types in the style of cubical type theories. I will talk about these features and also about our plans to implement language extensions that can be used to simplify reasoning about various higher structures.

Video recording of the talk is available.

I have a couple more in the pipeline, so follow this blog, the Foundations seminar announcements or my Twitter account @andrejbauer.

We are pleased to announce the minor release of opam 2.0.7.

This new version contains backported small fixes:

• Escape Windows paths on manpages [#4129 @AltGr @rjbou]
• Fix opam installer opam file [#4058 @rjbou]
• Fix various warnings [#4132 @rjbou @AltGr - fix #4100]
• Fix dune 2.5.0 promote-install-files duplication [#4132 @rjbou]

Note: To homogenise macOS name on system detection, we decided to keep macos, and convert darwin to macos in opam. For the moment, in order to avoid breaking jobs & CIs…

We are pleased to announce the minor release of opam 2.0.7.

This new version contains backported small fixes:

• Escape Windows paths on manpages [#4129 @AltGr @rjbou]
• Fix opam installer opam file [#4058 @rjbou]
• Fix various warnings [#4132 @rjbou @AltGr - fix #4100]
• Fix dune 2.5.0 promote-install-files duplication [#4132 @rjbou]

Note: To homogenise macOS name on system detection, we decided to keep macos, and convert darwin to macos in opam. For the moment, in order to avoid breaking jobs & CIs, we keep uploading darwin & macos binaries, but from the 2.1.0 release, only macos ones will be kept.

1. From binaries: run

   sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)

   or download manually from the Github "Releases" page to your PATH. In this case, don't forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update you sandbox script.

2. From source, using opam:

   opam update; opam install opam-devel

   (then copy the opam binary to your PATH as explained, and don't forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update you sandbox script)

3. From source, manually: see the instructions in the README.

We hope you enjoy this new minor version, and remain open to bug reports and suggestions.

NOTE: this article is cross-posted on opam.ocaml.org and ocamlpro.com. Please head to the latter for the comments!

We are happy to announce a alpha for opam 2.1.0, one year and a half in the making after the release of 2.0.0.

Many new features made it in (see the complete changelog or release note for the details), but here are a few highlights of this release.

Release highlights

The two following features have been around for a while as plugins and are now completely integrated in the core of opam. No extra installs needed anymore, and a more smooth experience.

Seamless integration of System dependenci…

We are happy to announce a alpha for opam 2.1.0, one year and a half in the making after the release of 2.0.0.

Many new features made it in (see the complete changelog or release note for the details), but here are a few highlights of this release.

Release highlights

The two following features have been around for a while as plugins and are now completely integrated in the core of opam. No extra installs needed anymore, and a more smooth experience.

Seamless integration of System dependencies handling (a.k.a. "depexts")

A number of opam packages depend on tools or libraries installed on the system, which are out of the scope of opam itself. Previous versions of opam added a specification format, and opam 2.0 already handled checking the OS and extracting the required system package names.

However, the workflow generally involved letting opam fail once, then installing the dependencies and retrying, or explicitely using the opam-depext plugin, which was invaluable for CI but still incurred extra steps.

With opam 2.1.0, depexts are seamlessly integrated, and you basically won't have to worry about them ahead of time:

• Before applying its course of actions, opam 2.1.0 checks that external dependencies are present, and will prompt you to install them. You are free to let it do it using sudo, or just run the provided commands yourself.
• It is resilient to depexts getting removed or out of sync.
• Opam 2.1.0 detects packages that depend on stuff that is not available on your OS version, and automatically avoids them.

This is all fully configurable, and can be bypassed without tricky commands when you need it (e.g. when you compiled a dependency yourself).

Dependency locking

To share a project for development, it is often necessary to be able to reproduce the exact same environment and dependencies setting — as opposed to allowing a range of versions as opam encourages you to do for releases.

For some reason, most other package managers call this feature "lock files". Opam can handle those in the form of [foo.]opam.locked files, and the --locked option.

With 2.1.0, you no longer need a plugin to generate these files: just running opam lock will create them for existing opam files, enforcing the exact version of all dependencies (including locally pinned packages).

If you check-in these files, new users would just have run opam switch create . --locked on a fresh clone to get a local switch ready to build the project.

Pinning sub-directories

This one is completely new: fans of the Monorepo rejoice, opam is now able to handle projects in subtrees of a repository.

• Using opam pin PROJECT_ROOT --subpath SUB_PROJECT, opam will look for PROJECT_ROOT/SUB_PROJECT/foo.opam. This will behave as a pinning to PROJECT_ROOT/SUB_PROJECT, except that the version-control handling is done in PROJECT_ROOT.
• Use opam pin PROJECT_ROOT --recursive to automatically lookup all sub-trees with opam files and pin them.

Opam switches are now defined by invariants

Previous versions of opam defined switches based on base packages, which typically included a compiler, and were immutable. Opam 2.1.0 instead defines them in terms of an invariant, which is a generic dependency formula.

This removes a lot of the rigidity opam switch commands had, with little changes on the existing commands. For example, opam upgrade ocaml commands are now possible; you could also define the invariant as ocaml-system and have its version change along with the version of the OCaml compiler installed system-wide.

Configuring opam from the command-line

The new opam option command allows to configure several options, without requiring manual edition of the configuration files.

For example:

• opam option jobs=6 --global will set the number of parallel build jobs opam is allowed to run (along with the associated jobs variable)
• opam option depext-run-commands=false disables the use of sudo for handling system dependencies; it will be replaced by a prompt to run the installation commands.

The command opam var is extended with the same format, acting on switch and global variables.

Try it!

In case you plan a possible rollback, you may want to first backup your ~/.opam directory.

The upgrade instructions are unchanged:

1. Either from binaries: run

   sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) --dev

   or download manually from the Github "Releases" page to your PATH.

2. Or from source, manually: see the instructions in the README.

You should then run:

opam init --reinit -ni

This is still a alpha, so a few glitches or regressions are to be expected. Please report them to the bug-tracker. Thanks for trying it out, and hoping you enjoy!

NOTE: this article is cross-posted on opam.ocaml.org and ocamlpro.com. Please head to the latter for the comments!

I just finished coding up another webapp in OCaml. I thought it would be cool to publish the sources of a small, completely self-contained app. It’s a sliding tile puzzle coded entirely in OCaml, using a few of the BuckleScript extensions. There are no dependencies on any frameworks or the like aside from the Js modules of BuckleScript. The app itself consists of just one JavaScript file—no images, nothing else.

You can try out the puzzle or get the sources a…

I just finished coding up another webapp in OCaml. I thought it would be cool to publish the sources of a small, completely self-contained app. It’s a sliding tile puzzle coded entirely in OCaml, using a few of the BuckleScript extensions. There are no dependencies on any frameworks or the like aside from the Js modules of BuckleScript. The app itself consists of just one JavaScript file—no images, nothing else.

You can try out the puzzle or get the sources at the Slide24 page.

I also tried to make a clean DOM interface based on experience with the Cassino and Schnapsen apps. I think it came out well, at least for these self-contained webapps.

The idea for the DOM interface is that it should expose only abstract types, but that there should be a subtype relation based on the JavaScript DOM. It turns out that you can do this pretty easily using private declarations. Types for contents of a document look like this:

type node
type text = private node
type element = private node
type canvas = private element
type box = private element
type div = private box
type span = private box
type button = private box

So, the interface reveals nothing whatsoever about the types except that they participate in a subtype relation. text and element are subtypes of node, canvas is a subtype of element, and so on. node is the supertype of all the document content types.

What this means is that you can pass a canvas or a button to a function that expects an element, and so on. I don’t find the necessity to use explicit supertype coercion to be too much trouble when working with non-parameterized types.

let style = Pseldom.(element_style (mybutton :> element)) in
. . .

It seems to me this captures pretty much everything that I want from the object-oriented approach without the usual complicated baggage. I think inheritance is more often a hindrance than a help. It’s too dependent on implementation details, and is associated with too many informal (unenforceable) descriptions of how to write subclasses of each class without messing up the semantics.

I’ve never used private declarations before, but they seem to have created exactly the structure I was hoping for.

Posted by: Jeffrey

Something like ten years ago we produced two iOS card game apps written in OCaml, partly as a proof of concept for compiling OCaml to iOS and partly because we enjoy card games. Unfortunately we weren’t able to spark a worldwide craze for writing iOS apps in OCaml or for playing Schnapsen, as we had hoped. Consequently there was very little financial return and we all had to move on to other projects.

Both apps play a very good two-player card game. The apps are essenti…

Something like ten years ago we produced two iOS card game apps written in OCaml, partly as a proof of concept for compiling OCaml to iOS and partly because we enjoy card games. Unfortunately we weren’t able to spark a worldwide craze for writing iOS apps in OCaml or for playing Schnapsen, as we had hoped. Consequently there was very little financial return and we all had to move on to other projects.

Both apps play a very good two-player card game. The apps are essentially a kind of solitaire where you play against the app as your opponent. The games are:

• Cassino, a classic fishing game said without substantiation to be of Italian origin (per Wikipedia).

• Schnapsen, a kind of miniature Pinochle very popular in the territories of the former Austro-Hungarian Empire (again per Wikipedia).

The Schnapsen app also plays a closely related game called Sixty-Six, named after this number in many different languages.

The images and layout algorithms for the apps quickly fell behind the formats and display capabilities of later iOS devices, so I was thinking we might just as well release the apps as is, for free. However there is a lot of rigamarole (and some cost) associated with the App Store if all you want to do is release some free apps.

Cassino

Master Schnapsen/66

Recently I wondered if it wouldn’t be possible to revive the apps in a browser environment. These days you can compile OCaml to JavaScript using BuckleScript or Js_of_ocaml. The HTML 5 canvas element has an interface a lot like the two-dimensional graphics used by the apps. It seems like it should be possible.

So, in fact, that’s what I did. I ported the two card game apps to run as webapps. Visually they run in a smallish rectangle exactly the size of the original iPhone screen. I was able to retain the iPhone behavior almost unchanged. Computationally they run completely in the browser, and make no further contact with psellos.com (unless you want to access the game pages at psellos.com).

The OCaml code is compiled to JavaScript using the BuckleScript compiler. Because the target language is JavaScript, there’s no need for any stubs or supporting code (as there was in iOS). All of the code for the apps is in OCaml.

Once the basic graphics primitives were in place, a lot of the code worked without any change. The part of the code that actually plays the game (the “engine”) didn’t change at all.

As an unexpected and very welcome side effect, two of the old iOS app team members got interested in the project again. They’re working on making the Schnapsen app into an even better player. I added some extra features to the Schnapsen GUI to make it easier to keep track of what’s happened in a hand.

Neither of the webapps is quite finished yet. But they both are already playable and in fact quite enjoyable. You can try them by clicking on the icons above. You can also read about the apps and the games they play on their own separate pages.

• Cassino Page
• Schnapsen Page

If you have any comments, suggestions, or encouragement, leave them below or email me at jeffsco@psellos.com.

Posted by: Jeffrey