Stream: Dune devs & users

Topic: Making PRs to Dune


view this post on Zulip Karl Palmskog (Feb 03 2022 at 13:15):

so let's say I did a PR to actually let (theories X) work with installed projects in contribs [in a hacky way]. Would this have any chance of getting merged? A lot of these things are design issues.

view this post on Zulip Paolo Giarrusso (Feb 03 2022 at 13:28):

"dune rejected Make's build protocol as immature" is both an unfair summary and representative :-).

view this post on Zulip Notification Bot (Feb 03 2022 at 13:29):

This topic was moved here from #Elpi users & devs > elpi and coqdep by Emilio Jesús Gallego Arias

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:30):

Sorry @Karl Palmskog but I get confused, I inferred from your statement that it was an actual problem in getting PRs merged

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:30):

but you mean a hypothetical one, right?

view this post on Zulip Karl Palmskog (Feb 03 2022 at 13:31):

yes, it's a hypothetical one

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:31):

For the case you say, it would me responsibility, so for sure if we chat 10 minutes about the hack

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:31):

and I'm ok with it, it would be merged, I'd be very happy, in fact other devs have submitted already features to Coq + Dune

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:31):

and the process was smooth TTBOMK

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:32):

Actually I don't think we need any hack to make that work fine

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:32):

I already have a tree doing most of the heavy lifting

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:34):

Paolo Giarrusso said:

"dune rejected Make's build protocol as immature" is both an unfair summary and representative :-).

Sorry @Paolo Giarrusso I'm not sure what that means (note I didn't follow that discussion, as people were talking about large distributed builds which I directly have 0 experience with)

view this post on Zulip Karl Palmskog (Feb 03 2022 at 13:35):

I think what he means is that make is a "build free-for-all", which puts few obstacles in your way to running whatever strange commands you want. Dune in contrast aims for an opinionated, strict, build protocol. This means that people have to spend time learning that protocol and its motivations, and they can't shoestring things together.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:36):

I think there is another factor that weights even more to the ones you give

view this post on Zulip Paolo Giarrusso (Feb 03 2022 at 13:37):

in that example, they also had stricter reliability requirements than make and weren't willing to add any interoperability

view this post on Zulip Karl Palmskog (Feb 03 2022 at 13:37):

I'd be happy to chat about the (theories) thing during the hackathon, but if you already have code I need to look at that does things in that direction, that doesn't necessarily make it easier (curse of knowledge, etc.)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:37):

and that Dune is used in a huge industrial codebase, whose challenges are not observed by us, but puts a lot of restrictions on stuff

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:37):

like zero build in our projects can be 0.5 secs, but 2 mins on a codebase of that size

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:38):

Karl Palmskog said:

I'd be happy to chat about the (theories) thing during the hackathon, but if you already have code I need to look at that does things in that direction, that doesn't necessarily make it easier (curse of knowledge, etc.)

Sure let's do it! The code helps as it tells you where are the components you need to touch: basically the library containing all the things in scope, and the rules

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:38):

Note that I fully understand the frustation people is having with many of my projects

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:38):

in the sense most of them are the work of a few days by an overworked, non-permanent researcher

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:39):

you heard the phrase that the last 1% takes 90% of the effort :D

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:39):

indeed

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:39):

for example jsCoq would have never been usable without Shachar doing huge work on his own

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:39):

and work which was extremely hard!

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:40):

So I agree with the all the problems, and I'm very happy to try improve the process

view this post on Zulip Karl Palmskog (Feb 03 2022 at 13:40):

I mean, a lot of us are in similar positions trying to do some paper while making small progress on some general tools. Sometimes we just need to agree on integration points, but this is also hard

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:42):

Yes we need better coordination, the development is very baazarish

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:43):

actually I just started to move the Coq Topic Working Group idea, I wanted a quick internal meeting at Inria first, then all the regular open meetings

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:43):

but it is proving very difficult

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:43):

people just do what they want XD

view this post on Zulip Karl Palmskog (Feb 03 2022 at 13:45):

that's sort of a truism. The crux to me is to set up goals which are aligned with interests and permit distributed work yet have some synergy in the end.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:47):

For that you first need people to come to the meetings :D

view this post on Zulip Karl Palmskog (Feb 03 2022 at 13:50):

I think you're not being Machiavellian enough. There are tricks like using some authority to issue proxied commands/suggestions. To take one example, many people are more willing to review the same paper if asked by a Turing award winner than some rando academic.

I think Lean shows a lot of the weird social effects that don't have much to do with work organization.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:50):

You may be right :D

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:51):

But the good news is that albeit slowly, I think we are moving forward

view this post on Zulip Karl Palmskog (Feb 03 2022 at 13:54):

to give one example: it took maybe a week to get all these projects tagged: https://github.com/coq/platform/issues/193

view this post on Zulip Karl Palmskog (Feb 03 2022 at 13:55):

meanwhile, "please create opam package" issue can remain unanswered for years.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:58):

This is IMHO a tooling problem

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:58):

manual step involved = problem

view this post on Zulip Karl Palmskog (Feb 03 2022 at 13:58):

tooling raises some obstacles, but come on, motivation is a huge part

view this post on Zulip Karl Palmskog (Feb 03 2022 at 13:59):

you have mentioned Rails in the past on convention over configuration, and often the draw in Rails was that cool people were using it, and you got "functionality for free"

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 14:05):

Karl Palmskog said:

tooling raises some obstacles, but come on, motivation is a huge part

It seems so.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 14:06):

I speak of tooling because in my "ideal" world, I would just do ./create_platform_release.sh and a set of bots would check everything is OK, would generate everything that's needed, and do the release / tagging

view this post on Zulip Paolo Giarrusso (Feb 03 2022 at 14:27):

clearly, "X should be automated" decreases motivation for doing X by hand

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 14:50):

Paolo Giarrusso said:

clearly, "X should be automated" decreases motivation for doing X by hand

Oh indeed, you may be right


Last updated: Jun 04 2023 at 23:30 UTC