Coq Platform and Lean comparison

Stream: general

[Karl Palmskog]

Enrico Tassi, Théo Zimmermann and I just published a preprint describing the Coq Platform, the official distribution of Coq together with libraries, plugins, and tools: https://hal.inria.fr/hal-03592675/document

We focus in particular on applying the Coq Platform for reproducing research artifacts, such as formalizations of mathematics, and on preparing specialized distributions for teaching with Coq.

We are interested in any feedback on this from the Lean community, in particular on our comparison of the Platform to Lean/mathlib in section 7.4 on page 9.

[Johan Commelin]

@Karl Palmskog Thanks! I completely agree with what you say about backwards compatibility and upgrade paths concerning Lean and mathlib. However, in an orthogonal direction, mathlib makes a very strong effort for internal compatibility. So that the algebra hierarchy is compatible by design with the topological library, etc... I think this is one benefit of mathlibs approach that deserves to be mentioned.

[Reid Barton]

Do you have an approximate release schedule/frequency in mind?

[Karl Palmskog]

@Reid Barton we follow Coq's approximate cycle of 6-month turnaround for releases (Platform release comes about 1-2 months after a Coq release)

[Karl Palmskog]

@Johan Commelin thanks for the feedback, we will note this for any camera ready or resubmission (the current submission is to RRRR 20222, but we hope it will be invited to a journal)

[Karl Palmskog]

I would argue, though, that MathComp has a similar "internal compatibility" policy as Mathlib, and we do include MathComp itself and many MathComp standalone subprojects in the Platform

[Karl Palmskog]

I suspect there may be a specific "MathComp Platform" for teaching at some point that's a strict subset of the general Platform

[Mario Carneiro]

@Karl Palmskog Regarding the specific wording of "In contrast to Coq, which aims to provide up-
grade paths between versions, Lean 3 and Lean 4 are largely incompatible", these two things are not in opposition. You can be incompatible and also aim to provide an upgrade path, and indeed if upgrading is a thing you need to do to the code then it sounds like it's already not backward compatible. For lean 3 -> lean 4 we are in fact investing heavily in providing an upgrade path, this is the mathport tool.

[Karl Palmskog]

the Coq compatibility policy means, with minor exceptions, that a project that is compatible with Coq version 8.X and has no deprecation warnings on 8.X will be compatible at the source level out-of-the-box with Coq version 8.(X+1) - but possibly with deprecation warnings on 8.(X+1). To me, even in the presence of tool to help with porting, this is a difference in kind and not in degree compared to the Lean approach.

[Karl Palmskog]

but if the paper gets considered for a journal submission, we will be sure to add more specifics about compatibility management in our comparisons.

[Karl Palmskog]

We incorporated feedback from the topic here into a new version of the paper (https://hal.inria.fr/hal-03592675v2). For example, we mention the mathport tool in our Lean comparison.

The new paper version will be the basis of a presentation in the RRRR reproducibility workshop at ETAPS on April 2, 2022. Any feedback on the new paper version is also welcome, since we hope to do a journal version eventually.