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.
"dune rejected Make's build protocol as immature" is both an unfair summary and representative :-).
This topic was moved here from #Elpi users & devs > elpi and coqdep by Emilio Jesús Gallego Arias
Sorry @Karl Palmskog but I get confused, I inferred from your statement that it was an actual problem in getting PRs merged
but you mean a hypothetical one, right?
yes, it's a hypothetical one
For the case you say, it would me responsibility, so for sure if we chat 10 minutes about the hack
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
and the process was smooth TTBOMK
Actually I don't think we need any hack to make that work fine
I already have a tree doing most of the heavy lifting
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)
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.
I think there is another factor that weights even more to the ones you give
in that example, they also had stricter reliability requirements than make
and weren't willing to add any interoperability
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.)
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
like zero build in our projects can be 0.5 secs, but 2 mins on a codebase of that size
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
Note that I fully understand the frustation people is having with many of my projects
in the sense most of them are the work of a few days by an overworked, non-permanent researcher
you heard the phrase that the last 1% takes 90% of the effort :D
indeed
for example jsCoq would have never been usable without Shachar doing huge work on his own
and work which was extremely hard!
So I agree with the all the problems, and I'm very happy to try improve the process
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
Yes we need better coordination, the development is very baazarish
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
but it is proving very difficult
people just do what they want XD
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.
For that you first need people to come to the meetings :D
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.
You may be right :D
But the good news is that albeit slowly, I think we are moving forward
to give one example: it took maybe a week to get all these projects tagged: https://github.com/coq/platform/issues/193
meanwhile, "please create opam package" issue can remain unanswered for years.
This is IMHO a tooling problem
manual step involved = problem
tooling raises some obstacles, but come on, motivation is a huge part
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"
Karl Palmskog said:
tooling raises some obstacles, but come on, motivation is a huge part
It seems so.
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
clearly, "X should be automated" decreases motivation for doing X by hand
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