Stream: Coq Universe

Topic: Hello World

Emilio Jesús Gallego Arias (Jun 05 2022 at 15:24):

Hello !

Emilio Jesús Gallego Arias (Jun 06 2022 at 15:56):

Some numbers for build times in a 16-core, 32-threads machine (2 x Intel(R) Xeon(R) CPU E5-2660 0 @ 2.20GHz):

real    34m33,477s
user    322m46,797s
sys     19m2,853s

job count stays usually around 10-30 , averaging at 20. Many parts of the stdlib come up pretty late in the build as they are seldom used. The last part of the build is odd-order with a totally linear build setup (1 job)

Paolo Giarrusso (Jun 06 2022 at 16:05):

Is this with dune? :grinning:

Emilio Jesús Gallego Arias (Jun 06 2022 at 16:06):

Yes, it is the Coq Universe build

Emilio Jesús Gallego Arias (Jun 06 2022 at 16:29):

In my laptop, 8-core, 16-threads i7-10875H:

real    24m38,502s
user    218m5,828s
sys     9m11,441s

Rudi Grinberg (Jun 06 2022 at 17:05):

Could you summarize what's a part of this hello world universe?

Emilio Jesús Gallego Arias (Jun 06 2022 at 17:12):

@Rudi Grinberg basically what you can see here https://github.com/ejgallego/coq-universe

Rudi Grinberg (Jun 06 2022 at 17:13):

Nice. Seems like quite a bit of stuff already

Rudi Grinberg (Jun 06 2022 at 17:14):

I don't know if you're familiar with stackage, but this could be a whipped up stackage for coq projects. Quite a useful thing for making sure things are mutually compatible and avoids the constraint solving hell on opam.

Emilio Jesús Gallego Arias (Jun 06 2022 at 17:14):

That's an interesting idea! Coq's CI kinda already checks that, but nobody is using that informaton

Rudi Grinberg (Jun 06 2022 at 17:17):

Coq's CI uses coq in master, right? So it's slightly different.

Emilio Jesús Gallego Arias (Jun 06 2022 at 17:20):

There is CI for each branch

Rudi Grinberg (Jun 06 2022 at 17:26):

In any case, it's already impressive.

Rudi Grinberg (Jun 06 2022 at 17:26):

There's no auto update mechanism for the various packages yet, right?

Emilio Jesús Gallego Arias (Jun 06 2022 at 17:27):

Rudi Grinberg said:

There's no auto update mechanism for the various packages yet, right?

See https://github.com/ejgallego/coq-universe/issues/9

Roland Coeurjoly Lechuga (Jun 06 2022 at 17:37):

What does it mean for a project to be present in Coq's CI system?

Emilio Jesús Gallego Arias (Jun 06 2022 at 17:45):

Roland Coeurjoly said:

What does it mean for a project to be present in Coq's CI system?

https://github.com/coq/coq/blob/master/dev/ci/README.md

Bas Spitters (Jun 06 2022 at 17:49):

Exciting! What are the differences/overlaps in goals with coq-platform, stdlib2, ...

Emilio Jesús Gallego Arias (Jun 06 2022 at 17:52):

@Bas Spitters this is how I envisioned the platform done at first, but we didn't have the tech

Emilio Jesús Gallego Arias (Jun 06 2022 at 17:52):

for now the main difference is that build is using dune, so it is truly incremental and supports caching

Emilio Jesús Gallego Arias (Jun 06 2022 at 17:53):

so from a dev point of view this is practical to do refactoring in multiple projects

Emilio Jesús Gallego Arias (Jun 06 2022 at 17:53):

also for dataset processing, doc generation, etc...

Emilio Jesús Gallego Arias (Jun 06 2022 at 17:53):

this should also be the base for what we call "dune theory specification" 2.0

Emilio Jesús Gallego Arias (Jun 06 2022 at 17:54):

which should handle Coq's stdlib as a regular library

Emilio Jesús Gallego Arias (Jun 06 2022 at 17:54):

so stdlib2 can benefit from this

Emilio Jesús Gallego Arias (Jun 06 2022 at 17:54):

but I would expect that to happen with theory spec 2.0

Roland Coeurjoly Lechuga (Jun 06 2022 at 18:41):

I tried building coq-universe but failed.
Among others, I get the following error:

Error: The implementation coq-master/clib/cMap.ml
does not match the interface coq-master/clib/.clib.objs/byte/cMap.cmi:

Maybe to improve reproducibility, a nix shell should be provided? I could volunteer

Emilio Jesús Gallego Arias (Jun 06 2022 at 19:01):

Hi @Roland Coeurjoly , sure a Nix build would be awesome

Emilio Jesús Gallego Arias (Jun 06 2022 at 19:01):

can you open a new topic with the precise problem and how to reproduce?

Théo Zimmermann (Jun 06 2022 at 19:07):

@Rudi Grinberg The closest thing we have to Stackage (and release coordination) is the Coq Platform. See https://hal.inria.fr/hal-03592675 for some details on the vision (and why it shares similarities with Stackage).

Rudi Grinberg (Jun 06 2022 at 19:18):

Cool. Seems like doing it with the coq-universe is a lightweight way to get some of the same benefits

Théo Zimmermann (Jun 06 2022 at 19:23):

Yes and no. Technology matters and stuff like coq-universe is definitely going to contribute to facilitating this kind of release coordination goals, but social aspects matter as well, and for this, having a process by which we ask authors to produce releases and incentivize them to do so is important as well.

Emilio Jesús Gallego Arias (Jun 06 2022 at 20:30):

@Théo Zimmermann actually one point of Coq Universe is to provide a unified tooling for that

Emilio Jesús Gallego Arias (Jun 06 2022 at 20:30):

once Coq's CI can run on that (which could make things go much faster actually, as it seems the Dune cache works inside the CI)

Paolo Giarrusso (Jun 06 2022 at 20:35):

the “platform” is needed for releases, but the universe could help a lot for fast iteration :-)

Paolo Giarrusso (Jun 06 2022 at 20:38):

most users do not just want to use some ecosystem snapshot that builds (which you would get from the universe), but also a snapshot made of stable releases — even in Coq there are kinds of quality control that are not enforced by coqc.

Rudi Grinberg (Jun 06 2022 at 20:40):

@Paolo Giarrusso have you dunified your projects yet? Seems like you understand the benefits of using dune. If not, what's blocking you?

Paolo Giarrusso (Jun 06 2022 at 20:42):

mine was a general comment — dune caching is enough of a killer app that I use dune wherever I can

Emilio Jesús Gallego Arias (Jun 06 2022 at 20:45):

I think @Paolo Giarrusso was mostly blocked on inter-scope composition right @Paolo Giarrusso ?

Roland Coeurjoly Lechuga (Jun 06 2022 at 20:54):

Rudi Grinberg said:

Paolo Giarrusso have you dunified your projects yet? Seems like you understand the benefits of using dune. If not, what's blocking you?

Apart from caching, what are the benefits of using dune?

Emilio Jesús Gallego Arias (Jun 06 2022 at 20:58):

Roland Coeurjoly said:

Rudi Grinberg said:

Paolo Giarrusso have you dunified your projects yet? Seems like you understand the benefits of using dune. If not, what's blocking you?

Apart from caching, what are the benefits of using dune?

@Roland Coeurjoly we should write this properly when we do a beta call, but Dune has quite a few more features than make. For example, it can track and delete stale targets, has exec / top functionality, for OCaml has a lot of goodies for people doing plugins, can compose theories, and handles generated files much better, including promotion

Rudi Grinberg (Jun 06 2022 at 21:02):

@Roland Coeurjoly in addition to those, it has proper windows support, sandboxing of rules, a fast watch mode, rpc for editor integration

Last updated: Sep 28 2023 at 11:01 UTC