Zulip Chat Archive

Stream: general

Topic: Coq Platform and Lean comparison


Karl Palmskog (Mar 01 2022 at 15:26):

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 (Mar 01 2022 at 16:35):

@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 (Mar 01 2022 at 16:39):

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

Karl Palmskog (Mar 01 2022 at 16:39):

@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 (Mar 01 2022 at 16:40):

@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 (Mar 01 2022 at 16:42):

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 (Mar 01 2022 at 16:43):

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 (Mar 01 2022 at 23:06):

@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 (Mar 02 2022 at 08:14):

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 (Mar 02 2022 at 08:16):

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 (Mar 18 2022 at 13:43):

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.


Last updated: Dec 20 2023 at 11:08 UTC