Stream: Coq Universe

Topic: Hello World


view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2022 at 15:24):

Hello !

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 16:05):

Is this with dune? :grinning:

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 16:06):

Yes, it is the Coq Universe build

view this post on Zulip 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

view this post on Zulip Rudi Grinberg (Jun 06 2022 at 17:05):

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

view this post on Zulip 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

view this post on Zulip Rudi Grinberg (Jun 06 2022 at 17:13):

Nice. Seems like quite a bit of stuff already

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Rudi Grinberg (Jun 06 2022 at 17:17):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 17:20):

There is CI for each branch

view this post on Zulip Rudi Grinberg (Jun 06 2022 at 17:26):

In any case, it's already impressive.

view this post on Zulip Rudi Grinberg (Jun 06 2022 at 17:26):

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

view this post on Zulip 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

view this post on Zulip Roland Coeurjoly (Jun 06 2022 at 17:37):

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

view this post on Zulip 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

view this post on Zulip Bas Spitters (Jun 06 2022 at 17:49):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 17:53):

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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 17:54):

which should handle Coq's stdlib as a regular library

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 17:54):

so stdlib2 can benefit from this

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 17:54):

but I would expect that to happen with theory spec 2.0

view this post on Zulip Roland Coeurjoly (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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 19:01):

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

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 20:35):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip Roland Coeurjoly (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?

view this post on Zulip 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

view this post on Zulip 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: Feb 06 2023 at 05:03 UTC