Karl Palmskog (Feb 03 2022 at 13:15): 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.
Paolo Giarrusso (Feb 03 2022 at 13:28):"dune rejected Make's build protocol as immature" is both an unfair summary and representative :-).
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
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
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:30):but you mean a hypothetical one, right?
Karl Palmskog (Feb 03 2022 at 13:31):yes, it's a hypothetical one
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
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
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:31):and the process was smooth TTBOMK
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
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:32):I already have a tree doing most of the heavy lifting
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)
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.
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
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
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.)
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
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
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
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
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
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
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:39):indeed
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
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:39):and work which was extremely hard!
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
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
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:42):Yes we need better coordination, the development is very baazarish
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
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:43):but it is proving very difficult
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:43):people just do what they want XD
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.
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:47):For that you first need people to come to the meetings :D
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.
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:50):You may be right :D
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
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
Karl Palmskog (Feb 03 2022 at 13:55):meanwhile, "please create opam package" issue can remain unanswered for years.
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:58):This is IMHO a tooling problem
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:58):manual step involved = problem
Karl Palmskog (Feb 03 2022 at 13:58):tooling raises some obstacles, but come on, motivation is a huge part
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"
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.
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
Paolo Giarrusso (Feb 03 2022 at 14:27):clearly, "X should be automated" decreases motivation for doing X by hand
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: Apr 18 2024 at 04:02 UTC