Interactions with OCaml features and runtime changes

Developing the Coq system
1

Hi everyone,

I’m creating this topic to centralize references to discussions on the impact (sometimes negative but often positive!) on Coq of the evolution of the OCaml compiler and tools; for example, compatibility issues introduced by new OCaml versions, and improvements in OCaml toolchain that could potentially benefit the Coq system.

Over the years we had discussions about this in many places (including in particular private email threads). Having a public place to centralize discussions, or at least references to discussions, can be beneficial. In particular, it allows people interested on this topic to have a global view of the various efforts going on – even if they don’t participate to everything.

(I’m going to post below with two separate pointers/summaries along these lines.)

2 Likes
2

Compatibility breaking: There are runtime changes in the 4.10 version of the OCaml compiler that break Coq (because Coq is/was relying on unstable internal details of the runtime) – and we expect more such changes in the future, especially as Multicore-OCaml changes are gradually integrated in the upstream runtime. My understanding is that the main issues for 4.10 were runtime changes in signal-handling (coming from the gradual merge of the statistical memory profiler, not Multicore).

(4.10 is not released, but its release process has started. There should be an alpha-release soon.)

Relevant pointers: are:

  • issue coq/coq#10603, " caml_signals_are_pending has been removed from OCaml upstream" by @ejgallego
  • PR coq/coq#11102, “Use the Alloc_small macro from the OCaml runtime rather than our own” by @silene, which is required for 4.10 compatibility but not merged in coq master yet
  • PR coq/coq#11103, " Fix signal polling for OCaml 4.10" by @gadmm

@ejgallego maintains a coq branch that is compatible with the 4.10, which is currently the head of his PR #11131.

Outside Coq maintainers (in particular @ejgallego and @silene), the people who worked most to fix the issues are @jhjourdan and @gadmm .

3

Performance experiment: the 4.10 runtime contains a new experimental allocator for the major heap, developed mainly by Damien Doligez, which was designed to improve performances for memory-hungry OCaml programs.
In issue #11277 I encouraged Coq maintainers to experiment with this (opt-in) allocator, and @ejgallego quickly provided benchmark results. The results are a bit different from my predictions from knowing the new allocator, but they do suggest that using it for Coq programs could result in nice memory savings (reductions of -7% to -13% where observed on test benchmarks consuming up to 3Gio of memory).

1 Like
4

Thanks for the topic @gasche. It is good that there is a public place to discuss this topic in addition to scattered discussions on github. I find it good to try to avoid using private channels for discussions that should be public. I have created an account so that I can follow it and contribute.

1 Like
5

For something positive, I have emitted the idea that Coq could be made robust in the face of memory exhaustion by implementing memory limits using a trick similar to what is described here: https://discuss.ocaml.org/t/todays-trick-memory-limits-with-gc-alarms/4431. The question of memory limits has been asked for Coq there for instance: Memory limit for commands. Unfortunately, this trick does not work in programs that uses systhreads like Coq. To make it compatible with systhreads, I have suggested that one could rely on the upcoming Memprof API (https://github.com/ocaml/ocaml/pull/8920) which offers new ways of asynchronously raising an exception into long-running code. This looks to me like a fun project which could also provide useful feedback to OCaml developers on the experimental API. Unfortunately I do not have time for it. I am leaving this idea here so that if somebody else finds this project fun, then we can have a chat about it.

6

Here is one issue I’ve come across that may fit this thread: deprecation warnings related to Pervasives in extracted OCaml code in OCaml 4.08 and later.

Specifically, when I use:

Require Import ExtrOcamlNatInt.

The extracted code tends to contain a lot of Pervasives.succ and similar function calls, which results in warnings like the following when compiling on OCaml 4.09.0:

File "file.ml", line 23, characters 13-28:
23 | | _ :: l' -> Pervasives.succ (length l')
                  ^^^^^^^^^^^^^^^
Alert deprecated: module Stdlib.Pervasives
Use Stdlib instead.

Maybe the best way would be to not use the Stdlib at all for this functionality?

I opened a Coq issue about this, but fixing things upstream likely leads to more work for extraction project maintainers - e.g., should everyone start to use stdlib shims?