Pierre-Marie Pédrot (May 11 2020 at 12:57): Pierre-Marie Pédrot (May 11 2020 at 12:57):At the risk of repeating myself, I hate the ocamlformat hook. Apart from breaking randomly from time to time, not being stable across versions and similar other horror stories, my grief today is diff size.
Pierre-Marie Pédrot (May 11 2020 at 12:58):I am trying to port funind to the new tactic engine, and it is horrible.
Pierre-Marie Pédrot (May 11 2020 at 12:58):It's virtually impossible to rebase any commit.
Pierre-Marie Pédrot (May 11 2020 at 12:59):Merely adding one line somewhere changes the format of 1000+ lines of code. I know that funind has a tendency to have too big functions, but still.
Pierre-Marie Pédrot (May 11 2020 at 12:59):Therefore, I am calling for a poll to see whether I am the only one facing this alienating piece of crap that abuses the name of "tool", and should be called instead a "torture rack".
Pierre-Marie Pédrot (May 11 2020 at 13:01):/poll should we get rid of the automatic ocamlformat hook?
Pierre-Marie Pédrot (May 11 2020 at 13:04):You're allowed to give arguments btw. For now I haven't seen any that would convince me so far apart from pure ideology.
Emilio Jesús Gallego Arias (May 11 2020 at 13:42):Indeed I was originally opposed to applying ocamlformat automatically; indeed ocamlformat is still experimental, and while I think we all appreciate the better formatting on funind [before was really bad], applying it automatically is a bit of a stretch.
On the other hand the point raised about formatting getting out of sync was valid; the idea was to use a couple of plugins to see how things go. I still feel that it would be better for developers to apply ocamlformat manually, but I dunno, there were quite strong opinions in both senses in that thread.
Regarding your concrete use case Pierre-Marie, it is indeed worst-case. I would just disable the automatic formatting and ignore the linter for now.
Pierre-Marie Pédrot (May 11 2020 at 13:44):I don't know how to deactivate this, so net result is that I'll have to start from scratch.
Emilio Jesús Gallego Arias (May 11 2020 at 13:45):Umm, you should not have to start from scratch; tweak dev/tools/pre-commit
Emilio Jesús Gallego Arias (May 11 2020 at 13:45):Or you can just uninstall ocamlformat
Enrico Tassi (May 11 2020 at 13:45):I think that the feeling about these tools is also related to the kind of coding you do. From time to time I move code around and end up copy/pasting code in a single function from different sources and indeed the code needs a lot of indenting work in order to become readable again. There I'd love to have a indent-selection feature in VScode (which I don't have for OCaml...). When I write new code, on the contrary, I much prefer to chose how the code is indented.
Bottom line: "indenting" a too long line is not a dumb task about putting enough \n\t, it is about picking a good name for an intermediate expression, something no tool can do for me.
Emilio Jesús Gallego Arias (May 11 2020 at 13:47):The discussion is about the hook I understand.
Emilio Jesús Gallego Arias (May 11 2020 at 13:49):For me @Pierre-Marie Pédrot it is ok to remove the hook temporarily; but yeah, that implies you need to push some indentation commits from time to time. By the way, git can understand ocamlformat changes for rebase and diff , this is another way to remove the pain
Emilio Jesús Gallego Arias (May 11 2020 at 13:49):But yeah, you need to configure your tooling
Emilio Jesús Gallego Arias (May 11 2020 at 13:50):But definitively you should not have to start from scratch; it would take a couple of minutes to have git understand the ocamlformat changes so your rebase / diff goes clean
Pierre-Marie Pédrot (May 11 2020 at 13:53):Emilio Jesús Gallego Arias: The discussion is about the hook I understand.
The hook and the linter check, actually.
Pierre-Marie Pédrot (May 11 2020 at 13:53):The first one is required by the second one.
Emilio Jesús Gallego Arias (May 11 2020 at 13:54):The linter check is less painful IMHO but it could be relaxed I think.
Emilio Jesús Gallego Arias (May 11 2020 at 13:54):or just turn it into a warning
Emilio Jesús Gallego Arias (May 11 2020 at 13:54):regarding the tool itself, I'm in favor of its (soft) application. After seeing the state of the codebase w.r.t. indent I prefer to delegate that choices than to have to think about indenting all the time.
Pierre-Marie Pédrot (May 11 2020 at 13:54):Also, even locally deactivating ocamlformat means that after a PR touching funind, I'll still get random diffs.
Pierre-Marie Pédrot (May 11 2020 at 13:55):Automatically applying a formatter to a pile of crap is not going to magically fix it.
Emilio Jesús Gallego Arias (May 11 2020 at 13:55):Yes, that's a problem Pierre-Marie, only solution there is to teach git about it
Pierre-Marie Pédrot (May 11 2020 at 13:55):The root of the problem is that funind and micromega are in a horrible state.
Pierre-Marie Pédrot (May 11 2020 at 13:56):Teaching git is not going to teach me to read through the diff, unfortunately.
Emilio Jesús Gallego Arias (May 11 2020 at 13:56):the point is not to fix the code, but to liberate the developers from having to think about that. I spent too much time worrying about indentation so in other projects, even if it doesn't fully follow my preferences, it is kind of liberating that I just write the code in the way I want, apply the formatted, and don't care about it.
Pierre-Marie Pédrot (May 11 2020 at 13:56):liberating
That's very strange, because it's precisely one of the most alienating things we added to the Coq dev tools.
Janno (May 11 2020 at 13:57):Do you mean reading through the diff on your computer on on github?
Emilio Jesús Gallego Arias (May 11 2020 at 13:57):Pierre-Marie Pédrot said:
Teaching git is not going to teach me to read through the diff, unfortunately.
What do you mean, if you teach git you should get the diff modulo indentation changes
Pierre-Marie Pédrot (May 11 2020 at 13:57):I love the linter in the absolute, e.g. auto correcting spacing and the like.
Emilio Jesús Gallego Arias (May 11 2020 at 13:57):Freedom is Slavery Pierre-Marie
Emilio Jesús Gallego Arias (May 11 2020 at 13:57):In your computer / git GUI
Pierre-Marie Pédrot (May 11 2020 at 13:57):@Jan-Oliver Kaiser reading on github.
Janno (May 11 2020 at 13:58):Could this help at all?
Pierre-Marie Pédrot (May 11 2020 at 13:58):It's not whitespace, unfortunately.
Emilio Jesús Gallego Arias (May 11 2020 at 13:58):yeah on github that's a bit more tricky for now, it will happen soon tho, so that's I preferred to use it softly , this auto-formatting tooling is experimental and indeed creates some churn here and there
Pierre-Marie Pédrot (May 11 2020 at 13:58):given a block of code, ocamlformat can reorder it in arbitrary ways
Janno (May 11 2020 at 13:59):Oh, I see. Sorry, I haven't yet had the pleasure of non-whitespace ocamlformat horror..
Emilio Jesús Gallego Arias (May 11 2020 at 13:59):Anyways my point of view Pierre-Marie is that we should not lose a lot of time on this; if you got his problem, making it soft for now is OK IMO
Pierre-Marie Pédrot (May 11 2020 at 13:59):e.g. I added two lines to a funind function and magically I ended up with 700 lines of code modified
Pierre-Marie Pédrot (May 11 2020 at 13:59):yes, but what bothers me is that it took so long to reach this conclusion
Pierre-Marie Pédrot (May 11 2020 at 13:59):I was not the only one complaining
Pierre-Marie Pédrot (May 11 2020 at 13:59):@Maxime Dénès also ranted at some point
Emilio Jesús Gallego Arias (May 11 2020 at 14:00):Pierre-Marie Pédrot said:
e.g. I added two lines to a funind function and magically I ended up with 700 lines of code modified
That actually signals a different problem IMO in terms of how the API is supposed to work
Emilio Jesús Gallego Arias (May 11 2020 at 14:00):@Pierre-Marie Pédrot this doesn't seem accurate to me
Pierre-Marie Pédrot (May 11 2020 at 14:00):what?
Emilio Jesús Gallego Arias (May 11 2020 at 14:00):your point about who ranted
Pierre-Marie Pédrot (May 11 2020 at 14:01):what's the accurate formulation then?
Pierre-Marie Pédrot (May 11 2020 at 14:01):My personal stance is that I don't like the method of shoving broken tools up the throat of our dev team
Emilio Jesús Gallego Arias (May 11 2020 at 14:01):I am moving on, I already wrote a long post on gitter explaining what happened with microomega [which was actually a confusion] I cannot afford to spend so many cycles on this sorry.
Pierre-Marie Pédrot (May 11 2020 at 14:01):ok, so let's stop losing time
Emilio Jesús Gallego Arias (May 11 2020 at 14:02):I already explained to you what happened last time you did that comment, which it is not fair
Emilio Jesús Gallego Arias (May 11 2020 at 14:02):if you don't want to read the actual discussion and history about what happened what can I do?
Emilio Jesús Gallego Arias (May 11 2020 at 14:02):the comment is not fair I mean
Pierre-Marie Pédrot (May 11 2020 at 14:02):anyways
Pierre-Marie Pédrot (May 11 2020 at 14:03):I'll submit a PR deactivating this format + check
Pierre-Marie Pédrot (May 11 2020 at 14:03):problem solved
Théo Zimmermann (May 11 2020 at 14:29):I am seriously annoyed by your way of starting discussions @Pierre-Marie Pédrot :frown:
Théo Zimmermann (May 11 2020 at 14:36):And in addition to repeating false claims from the last time this discussion happened, you are completely overlooking all the efforts that was made (by myself in particular) to accommodate the feedback.
Théo Zimmermann (May 11 2020 at 14:37):So even after this ocamlformat is still not working out, OK, maybe time to reconsider it, but do not pretend that the complaints so far were ignored.
Théo Zimmermann (May 11 2020 at 14:38):So yeah, do whatever you want to ocamlformat but change your attitude too. This is hitting my nerves.
Théo Zimmermann (May 11 2020 at 14:40):And a poll is certainly not the right way of taking this decision. What if a majority is in favor of keeping it because they never touch this part of the codebase? We can remove ocamlformat if it bothers just a couple of devs, that's not a problem.
Théo Zimmermann (May 11 2020 at 14:42):I don't feel so much concerned for instance. I almost never touch this code (funind and micromega). I touch other parts of the codebase for which I wish I had ocamlformat activated but that's not such a big deal. I have ocamlformat activated in the codebase of coqbot and I'm already happy with this.
Enrico Tassi (May 11 2020 at 15:15):@Théo Zimmermann what I don't understand is how it is possible that we have weekly calls and a change in the process/toolchain is not discussed before being implemented. As these endless discussions show, this ocamlformat thing is absolutely not consensual.
Théo Zimmermann (May 11 2020 at 15:18):@Enrico Tassi What I don't understand is that a developer can rant here about this being done against the will of other developers when it was actually discussed a number of time in Coq Calls...
Théo Zimmermann (May 11 2020 at 15:19):So do whatever the heck you want to ocamlformat but stop pretending that complaints are getting ignored and so forth.
Enrico Tassi (May 11 2020 at 15:20):Hum, I don't miss many of these calls...
Théo Zimmermann (May 11 2020 at 15:21):Let's not pretend that the introduction of ocamlformat in the pre-commit hook toolchain was not discussed because it was done because devs asked for it.
Théo Zimmermann (May 11 2020 at 15:23):I spent way too much time (during a week-end) working on this (coq/coq#11874) and the PR received 39 comments!
Enrico Tassi (May 11 2020 at 15:23):the pre-commit hook was a patch to alleviate the pain. that is welcome. sorry if I ranted again about the root/original problem.
Enrico Tassi (May 11 2020 at 15:29):Pierre-Marie Pédrot said:
Emilio Jesús Gallego Arias: The discussion is about the hook I understand.
The hook and the linter check, actually.
Anyway, the discussion was about both things, not just the git hook, since, as the message after the one I quote says, one requires the other.
Théo Zimmermann (May 11 2020 at 15:30):Let's repeat again the story of how it was introduced then: ocamlformat got applied a bit too eagerly by a micromega maintainer who did not want to have to think of formatting (typical use-case of using an automatic code formatter BTW). But the problem of ocamlformat is that it formats a whole file, so if you apply it only from time to time (e.g. when this maintainer works on the code), then you will have massive noise in your diffs. Therefore, at that time, I thought it would make sense to enforce formatting and suggested adding it in the linter. My mistake. Mea maxima culpa. But after this introduction which was certainly done too fast (but that's because nobody anticipated it), nothing was done without discussion.
Emilio Jesús Gallego Arias (May 11 2020 at 16:39):Indeed I do agree with Théo 's remark about the form of the discussion; I see a couple of points that I personally don't like and that do hurt the project and create great damage to Coq's public image:
Emilio Jesús Gallego Arias (May 11 2020 at 16:49):so in short folks, let's try to be kind to each other and if problems with stuff arise, let's just go and solve them instead of ranting. Example this thread could have gone better is something like "Hi ocamlformat people, I am having a lot of trouble with my funind refactoring, when I try to do X I get an unwieldy diff. Is this normal, is there some workaround I can use? Maybe we should modify the current setup?"
Pierre-Marie Pédrot (May 11 2020 at 19:21):You're right, I am sorry for the tone.
Pierre-Marie Pédrot (May 11 2020 at 19:22):In particular, I wrongly aimed my wrath at the hook, which is not the actual thing I had in mind.
Pierre-Marie Pédrot (May 11 2020 at 19:22):As @Enrico Tassi said, the root issue is the ocamlformat lint.
Pierre-Marie Pédrot (May 11 2020 at 19:24):So, let's act in good faith:
Pierre-Marie Pédrot (May 11 2020 at 19:24): Pierre-Marie Pédrot (May 11 2020 at 19:25): Pierre-Marie Pédrot (May 11 2020 at 19:26):What do?
Emilio Jesús Gallego Arias (May 11 2020 at 23:04):No worries @Pierre-Marie Pédrot , I understand how frustrating this stuff is. Indeed there is a tricky point here about requiring advanced tooling, as I said I propose we address the attempts to change the tooling with a bit of patiente.
Now, regarding your question, my opinion is that if the tooling [in this case ocamlformat] is making your life harder, you should immediate override it and don't lose any time on that, much less put yourself thru a hellish rebase; specially for stuff like ocamlformat we can easily re-apply it any time in the future. If you are adventurous you could also try the git support for it, but that effectively means that you'd become a beta/alpha tester of ocamlformat so IMHO this should only be done by those curious about it.
So I'd say that in your particular case, ocamlformat should be disabled; what to do in the medium term is more open. My personal opinion here is to use this kind of tooling in a "soft" way, as for example is done in Dune. That means that ocamlformat is mostly applied manually, only when the developers feel it is needed. That introduces some extra commits but on the other hand the pain is minimal. On the other hand the lint check is indeed useful as to avoid the "going out of sync" problem [and thus formatting-only commits that are for example OK in Dune], but it does indeed require a special git setup so seems quite hard.
My "soft" point of view didn't unfortunately got a lot of support so we went for the lint check; I dunno, I still feel the lint check is an interesting experiment as long as it is clear it shouldn't interfere with regular development practice, but we can make it into a warning or an allow-failure job [so people may run make fmt if they feel like it]
On the topic of general ocamlformat use, I am 51% in favor / 49% against; it is very good in projects where I'm not the main contributor [so I can entirely forget about how I'm supposed to lay the code out], on my personal projects I do indent as I want so it mostly interferes.
For Coq, I find the wildly different code layouts a bit distressing [and as for funind for example, impossible to read / modify] so I would personally prefer the tradeoff of using it [even if not perfect] to the current mess. But yeah, I have to admit that for me this kind of tooling setup is mostly painless, in the sense that I'm able to quickly fix my editor / git system to accommodate to this without a lot of problems.
Pierre-Marie Pédrot (Jun 10 2020 at 16:36):vernac/.ocamlformat-enable:comHints.ml
Pierre-Marie Pédrot (Jun 10 2020 at 16:36):this is a joke, right?
Théo Zimmermann (Jun 10 2020 at 16:41):Ah ah! I'm assuming that @Emilio Jesús Gallego Arias accidentally committed it. But note that you are the one who merged the PR that introduced it (coq/coq#12130).
Pierre-Marie Pédrot (Jun 10 2020 at 16:43):Oh, the irony...
Emilio Jesús Gallego Arias (Jun 10 2020 at 19:53):Pierre-Marie Pédrot said:
this is a joke, right?
@Pierre-Marie Pédrot can you stop talking in derogatory terms please?
Théo Zimmermann (Jun 11 2020 at 08:44):But was this inserted and left in the PR on purpose? I personally wouldn't be opposed to enforce ocamlformat on new files but we would have to first:
Théo Zimmermann (Jun 11 2020 at 08:44): Théo Zimmermann (Jun 11 2020 at 08:44): Pierre-Marie Pédrot (Jun 11 2020 at 09:04):convince our fellow developers that this is useful
I think you don't realize the level of annoyance ocamlformat constitutes: there are PR I currently cannot rebase because I am waiting to get rid of ocamlformat on funind.
Pierre-Marie Pédrot (Jun 11 2020 at 09:05):And it's not just some stray whitespace, ocamlformat gladly rewrites chunks of hundreds of lines
Pierre-Marie Pédrot (Jun 11 2020 at 09:05):So I don't think there is any way to make the diff understandable to git
Théo Zimmermann (Jun 11 2020 at 09:07):Why didn't you prepare the PR removing ocamlformat from the linter yet, BTW? I told you I would merge it.
Théo Zimmermann (Jun 11 2020 at 09:08):Pierre-Marie Pédrot said:
So I don't think there is any way to make the diff understandable to git
I haven't tested it but it is supposed to be possible to configure the diff algorithm that git uses.
Pierre-Marie Pédrot (Jun 11 2020 at 09:08):To be honest, because I am sadistic.
Pierre-Marie Pédrot (Jun 11 2020 at 09:08):I secretly hope you'll have to backport a change to funind that triggers this kind of behaviours
Pierre-Marie Pédrot (Jun 11 2020 at 09:09):So that I end up not being the only one complaining
Pierre-Marie Pédrot (Jun 11 2020 at 09:09):(my personal theory is that very few people touch funind / micromega which is why the problem went unnoticed)
Pierre-Marie Pédrot (Jun 11 2020 at 09:10):but since I perform in-depth cleanups of e.g. tactics, I am on the front line
Pierre-Marie Pédrot (Jun 11 2020 at 09:11):Also, I wonder why this kind of problem does not appear with formatters in other languages ?
Pierre-Marie Pédrot (Jun 11 2020 at 09:11):do they respect more the line structure or what?
Pierre-Marie Pédrot (Jun 11 2020 at 09:11):from my painful experience ocamlformat is fundamentally incompatible with line-based CVS
Maxime Dénès (Jun 11 2020 at 09:14):@Pierre-Marie Pédrot IIRC, the current status quo is that you can call @Emilio Jesús Gallego Arias for help each time a rebase is made difficult by ocamlformat.
Enrico Tassi (Jun 11 2020 at 09:19):Pierre-Marie Pédrot said:
from my painful experience ocamlformat is fundamentally incompatible with line-based CVS
Not all projects check that a file round trips wrt automatic indentation. This is what makes it hard to read the diff of a change that triggers some indentation (if you don't reindent after your change, I see no problem)
Pierre-Marie Pédrot (Jun 11 2020 at 09:19):ocamlformat is not automatic indentation
Maxime Dénès (Jun 11 2020 at 09:20):yeah the problems I usually have are in the part far beyond automatic indentation indeed
Pierre-Marie Pédrot (Jun 11 2020 at 09:20):it can rewrite your code in fancy ways
Pierre-Marie Pédrot (Jun 11 2020 at 09:20):including replacing begin / end with parentheses and random stylistic choices of the same kind
Maxime Dénès (Jun 11 2020 at 09:20):this one we disabled, no?
Maxime Dénès (Jun 11 2020 at 09:20):but yeah, this kind of changes
Pierre-Marie Pédrot (Jun 11 2020 at 09:21):I think I remember at some point it was on, I don't know whether it was disabled since
Pierre-Marie Pédrot (Jun 11 2020 at 09:21):seems to be off judging from funind
Enrico Tassi (Jun 11 2020 at 09:22):Again, this is not the problem. If you don't have to run it, it leaves your begin/end alone.
Enrico Tassi (Jun 11 2020 at 09:22):But since you have to...
Théo Zimmermann (Jun 11 2020 at 09:49):Pierre-Marie Pédrot said:
do they respect more the line structure or what?
elm-format does respect the line structure much more: it won't break your line because it has become too long: for instance, you can keep adding items to a list and keep it on a single line, but as soon as you put a single new line inside a list it will put all of your list items on different lines.
Théo Zimmermann (Jun 11 2020 at 09:49):Pierre-Marie Pédrot said:
Also, I wonder why this kind of problem does not appear with formatters in other languages ?
But maybe the answer is also: because not many projects rebase as much as we do.
Théo Zimmermann (Jun 11 2020 at 09:49):git was invented first and foremost for the ability to merge, not rebase.
Enrico Tassi (Jun 11 2020 at 10:19):Théo Zimmermann said:
But maybe the answer is also: because not many projects rebase as much as we do.
You get the same problem with merge as well when there is a conflict. The conflict is not just going to be about the change but also the reformatting accompaining that change. I see no link with git or our workflow (other than forcing the reformatting).
Théo Zimmermann (Jun 11 2020 at 10:27):In any case, if you have reasonably sized functions you cannot have horrible diffs resulting from an automatic reformatting, maybe most projects that use a code formatter have less such cases of huge functions that get highly impacted by the formatter.
Théo Zimmermann (Jun 11 2020 at 10:29):The question then becomes: was micromega and funind really the good candidates to show the point of ocamlformat?
Enrico Tassi (Jun 11 2020 at 12:05):Théo Zimmermann said:
The question then becomes: was micromega and funind really the good candidates to show the point of
ocamlformat?
IMO yes they were good candidate to be indented once and no they were not good candidates to be kept indented with the current technology/workflow.
I've no idea what is the "ocamlformat point to be shown". To me it's just a tool, and we are misusing it, hence it backfires.
Emilio Jesús Gallego Arias (Sep 21 2020 at 21:51):For those interested in ocamlformat there will be a seminar this Jeudi at Jussieu; I plan to be in person there.
Emilio Jesús Gallego Arias (Sep 21 2020 at 21:51):http://www-apr.lip6.fr/~chaillou/Public/programmation/index.html
Emilio Jesús Gallego Arias (Sep 21 2020 at 21:51):I wonder if there will be an online option
Last updated: Nov 29 2023 at 21:01 UTC