Mukesh Tiwari (Oct 28 2021 at 04:13): Mukesh Tiwari (Oct 28 2021 at 04:13):I am trying to install coq-prime that depends on coq-bignums, but it fails to install coq-bignums. Any idea to solve this?
➜ Crypto_Voting git:(main) ✗ opam install coq-coqprime
The following actions will be performed:
∗ install coq-bignums 8.14.0 [required by coq-coqprime]
∗ install coq-coqprime 1.1.0
===== ∗ 2 =====
Do you want to continue? [Y/n] Y
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
⬇ retrieved coq-bignums.8.14.0 (https://github.com/coq/bignums/archive/V8.14.0.tar.gz)
⬇ retrieved coq-coqprime.1.1.0 (https://github.com/thery/coqprime/archive/v8.14.zip)
[ERROR] The compilation of coq-bignums.8.14.0 failed at "make -j9".
#=== ERROR while compiling coq-bignums.8.14.0 =================================#
# context 2.1.0 | macos/arm64 | ocaml.4.13.1 | https://coq.inria.fr/opam/released#2021-10-26 17:40
# path ~/.opam/default/.opam-switch/build/coq-bignums.8.14.0
# command ~/.opam/opam-init/hooks/sandbox.sh build make -j9
# exit-code 2
# env-file ~/.opam/log/coq-bignums-13879-027796.env
# output-file ~/.opam/log/coq-bignums-13879-027796.out
### output ###
# [...]
# #[global] and #[export] depending on your choice. For example: "#[export]
# Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
# File "./SpecViaQ/QSig.v", line 150, characters 0-4:
# Warning: The default value for instance locality is currently "local" in a
# section and "global" otherwise, but is scheduled to change in a future
# release. For the time being, adding instances outside of sections without
# specifying an explicit locality attribute is therefore deprecated. It is
# recommended to use "export" whenever possible. Use the attributes #[local],
# #[global] and #[export] depending on your choice. For example: "#[export]
# Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
# make[1]: *** [all] Error 2
# make: *** [all] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
┌─ The following actions failed
│ λ build coq-bignums 8.14.0
└─
╶─ No changes have been performed
➜ Crypto_Voting git:(main) ✗ opam --version
2.1.0
➜ Crypto_Voting git:(main) ✗ coqtop --version
The Coq Proof Assistant, version 8.14.0
compiled with OCaml 4.13.1
One could downgrade coq to 8.13.2, investigate what coqprime supports, or fix the error
Guillaume Melquiond (Oct 28 2021 at 06:41):Unfortunately, the log does not show what the actual error is. You need to open the "output-file" and show us the relevant part. (Either that or use opam install -j1 coq-bignums=8.14.0 to disable parallel compilation.)
Mukesh Tiwari (Oct 28 2021 at 06:49):Content of the ~/.opam/log/coq-bignums-18025-d2684f.out file:
coq_makefile -f _CoqProject -o Makefile.coq
make -f Makefile.coq Makefile
ocaml BigN/gen/NMake_gen.ml > BigN/NMake_gen.v || (RV=$?; rm -f BigN/NMake_gen.v; exit ${RV})
COQDEP VFILES
OCAMLLIBDEP plugin/bignums_syntax_plugin.mlpack
CAMLDEP plugin/bignums_syntax.ml
make[1]: Nothing to be done for `Makefile'.
make -f Makefile.coq all
CAMLOPT -c -for-pack Bignums_syntax_plugin plugin/bignums_syntax.ml
File "plugin/bignums_syntax.ml", line 1:
Error (warning 70 [missing-mli]): Cannot find interface file.
make[2]: *** [plugin/bignums_syntax.cmx] Error 2
make[1]: *** [all] Error 2
make: *** [all] Error 2
hmm, I wonder if this is an OCaml 4.13.1 issue?
Guillaume Melquiond (Oct 28 2021 at 06:51):Your OCaml compiler is too recent, and since Bignum forbids any warning (bad bad zoot), the compilation fails for no good reason.
Karl Palmskog (Oct 28 2021 at 06:53):@Guillaume Melquiond do you think we should patch the package to not choke on warnings? or make a new release?
Karl Palmskog (Oct 28 2021 at 06:54):ping @Michael Soegtrop who may want to be aware that an 8.14 Platform package currently fails with OCaml 4.13.1
Mukesh Tiwari (Oct 28 2021 at 06:55):Thanks for the quick reply @Guillaume Melquiond . I will switch to an older version of OCaml compiler.
Guillaume Melquiond (Oct 28 2021 at 06:55):Either one or the other. The OCaml documentation clearly states that using -warn-error in production is a poor practice. So, it is worth changing in the repository any way.
Karl Palmskog (Oct 28 2021 at 06:56):OK, then I think a new release is in order, and we change the 8.14.0 package to have a bound < 4.13
Karl Palmskog (Oct 28 2021 at 07:25):argh, there is no v8.14 branch in bignums.
Karl Palmskog (Oct 28 2021 at 07:35):@Guillaume Claret perhaps we could get a coq-bench worker for OCaml 4.13 so we can figure out how many packages more than bignums break?
Karl Palmskog (Oct 28 2021 at 07:54):looks like switching to Dune solves the problem, but probably breaks things like native
Pierre Roux (Oct 28 2021 at 07:56):Yes, please don't switch bignums to dune yet.
Karl Palmskog (Oct 28 2021 at 08:57):just checked that this affects aac-tactics as well... big sigh
Karl Palmskog (Oct 28 2021 at 08:58):I'm sure OCaml devs had their reasons, but making "missing" mli files into a warning may become a major issue going forward due to bad interaction coq_makefile
Enrico Tassi (Oct 28 2021 at 08:59):The problem is that all opam packages should call coq_makefile passing OCAMLWARN=, see for example https://github.com/LPCIC/coq-elpi/blob/bfaf9ce7355c298e51f5bd5726214d5c906f7e2f/coq-elpi.opam#L11
Karl Palmskog (Oct 28 2021 at 09:00):to me, seems terrible that we should put more boilerplate in opam packages just due to 4.13 and coq_makefile
Enrico Tassi (Oct 28 2021 at 09:00):The idea of fatal warnings on by default is very bad, I've been overly vocal about that, and percolated from dune to coq_makefile as well, with the extra issue that in opam packages you don't have a -p to pass to coq_makefile. So I suggest you pass OCAMLWARN=
Enrico Tassi (Oct 28 2021 at 09:01):It is the same with dune, you have to pass -p IIRC
Karl Palmskog (Oct 28 2021 at 09:01):sure, but that Dune boilerplate has been there from the start
Enrico Tassi (Oct 28 2021 at 09:01):I know...
Karl Palmskog (Oct 28 2021 at 09:02):we are talking about probably hundreds of package definitions here
Enrico Tassi (Oct 28 2021 at 09:03):I know, I would just make warnings non fatal in coq_makefile but there was resistance since we also use it from the CI of coq....
Karl Palmskog (Oct 28 2021 at 09:03):for example, in 4.14 they may call it CAMLWARN or whatever, and then we have to change everything again
Enrico Tassi (Oct 28 2021 at 09:03):no no, the variable is coq_makefile specific
Karl Palmskog (Oct 28 2021 at 09:07):OK, to be honest, we should definitely weigh switching everything with OCaml in the Coq opam repo we can to Dune ASAP against trying to hunt down hundreds of packages like this...
Enrico Tassi (Oct 28 2021 at 09:08):or make warnings non fatal which takes 1 minute
Karl Palmskog (Oct 28 2021 at 09:09):you mean modify coq_makefile? Or where would that change be made?
Enrico Tassi (Oct 28 2021 at 09:09):yes there is a default to flip, that is all
Karl Palmskog (Oct 28 2021 at 09:10):but that would come out in 8.14.1 at the absolute earliest
Karl Palmskog (Oct 28 2021 at 09:10):we would still be stuck with existing packages...
Karl Palmskog (Oct 28 2021 at 09:11):@Enrico Tassi this seems like something to take up at the next Coq call, do you agree?
Enrico Tassi (Oct 28 2021 at 09:17):well here it is https://github.com/coq/coq/pull/9605 , I should have complained more, I did not realize that one would have to change all existing packages orelse that would have set a time bomb.
Pierre Roux (Oct 28 2021 at 09:18):Karl Palmskog said:
we should definitely weigh switching everything with OCaml in the Coq opam repo we can to Dune ASAP
I think we should wait until there is a Dune version fully supporting coq-native (this could be envisioned with new Dune 3.0 features IIUC). For instance, switching paramcoq to dune now would make CoqEAL (and everything using it) unusable with coq-native (unless rolling up configure scripts as recently painfully experienced with multinomials).
Enrico Tassi (Oct 28 2021 at 09:18):I don't know if I have the energy, I've spent already enough time trying to convince the other devs pushing the idea that it was a silly one. But you are welcome to try again.
Karl Palmskog (Oct 28 2021 at 09:19):OK, thanks, this means at least we know which Coq versions are affected for coq_makefile
Paolo Giarrusso (Oct 28 2021 at 09:20):Can OCAMLWARN be set in the switch as an environment variable?
Karl Palmskog (Oct 28 2021 at 09:20):I didn't realize the history here, but indeed a time bomb seems to have exploded
Paolo Giarrusso (Oct 28 2021 at 09:21):That'd be a manual workaround, but it's a cheaper one.
Karl Palmskog (Oct 28 2021 at 09:22):yes, in limited circumstances this is a workaround, but we can't reasonably enforce this env var in general
Enrico Tassi (Oct 28 2021 at 09:22):If this is the case, then this is where it should be done: https://github.com/coq/opam-coq-archive/blob/master/scripts/opam-coq-init
Enrico Tassi (Oct 28 2021 at 09:23):indeed, that would make our CI pass, but fail in the user's hands
Paolo Giarrusso (Oct 28 2021 at 09:23):Better idea: opam "hotfix" for all existing Coq packages that support such a recent OCaml. How many are there?
Karl Palmskog (Oct 28 2021 at 09:24):my estimate would be "hundreds", but we can't know for sure unless Guillaume Claret sets up a 4.13 worker for coq-bench
Paolo Giarrusso (Oct 28 2021 at 09:25):No, I meant Coq releases
Paolo Giarrusso (Oct 28 2021 at 09:25):Isn't it only Coq 8.14.0 and maybe 8.13.late?
Karl Palmskog (Oct 28 2021 at 09:25):it looks like 8.13.0, 8.13.1, 8.13.2, 8.14.0 are compatible with 4.13
Enrico Tassi (Oct 28 2021 at 09:26):no, the PR in question was in 8.11 I guess
Paolo Giarrusso (Oct 28 2021 at 09:26):8.11 doesn't build with OCaml 4.13 I expect.
Enrico Tassi (Oct 28 2021 at 09:26):IMO the best hotfix is $ git grep '\[make "-j' | wc -l
Enrico Tassi (Oct 28 2021 at 09:27):which gives 1500 packages, then you can sed like s/]/ "CAMLWARN="]/
Enrico Tassi (Oct 28 2021 at 09:28):it is hard to know if the package builds .ml files
Enrico Tassi (Oct 28 2021 at 09:28):only these really need to be fixed
Enrico Tassi (Oct 28 2021 at 09:29):ok, I see that
Paolo Giarrusso (Oct 28 2021 at 09:29):That's looking for sed bugs, really, and that regexp seems far too strict.
Enrico Tassi (Oct 28 2021 at 09:29):sure, it was "pseudo code"
Enrico Tassi (Oct 28 2021 at 09:30):there is an ocaml libray to parse opam files and do a more semantic edit... but I've no time for that
Karl Palmskog (Oct 28 2021 at 09:30):OK, we need to set up issues in Coq itself and in the opam archive repo for this. I can do it tonight and summarize the discussion so far
Enrico Tassi (Oct 28 2021 at 09:30):I don't even know if it can print back
Paolo Giarrusso (Oct 28 2021 at 09:30):I don't think a robust version exist; I do such things, but not when shipping to thousands of users. So why not patch those 4 coq releases?
Karl Palmskog (Oct 28 2021 at 09:31):maybe it is the best solution indeed (to patch 8.13.X and 8.14.0 opam packages in the OCaml opam repo)
Enrico Tassi (Oct 28 2021 at 09:31):For that you need to bring it up at the call, and convince @Théo Zimmermann and @Emilio Jesús Gallego Arias
Enrico Tassi (Oct 28 2021 at 09:32):Ok, but you want that patch to be merged upstream eventually
Paolo Giarrusso (Oct 28 2021 at 09:33):Sure, you want the upstreaming as well.
Paolo Giarrusso (Oct 28 2021 at 09:34):You'd want to think the patch through: this wouldn't fix users of binary packages but they won't install opam packages, and this will change behavior of existing coq_makefile, but it seems acceptable. Maybe worth documenting because of the changes in some corner cases.
Karl Palmskog (Oct 28 2021 at 09:35):it will at least never break something that works currently with coq_makefile (right?)
Paolo Giarrusso (Oct 28 2021 at 09:36):Some users will get fewer warnings; might be worth a notice, but shouldn't be a showstopper.
Paolo Giarrusso (Oct 28 2021 at 09:37):For upstreaming, I think the usual compromise is warn-error in CI but not release, exactly because of newer compilers adding warnings, even for Coq CI. Dune didn't invent anything, I'd say we have enough relevant experience from C packaging.
Enrico Tassi (Oct 28 2021 at 09:40):What is wrong is to make the default such that all final users need to change it, rather than change it in CI and be done with it.
Paolo Giarrusso (Oct 28 2021 at 09:43):well: change it in CI _and_ on all developers’ machines at dev time, really. I still think it’s the right choice.
Karl Palmskog (Oct 28 2021 at 09:46):OK, so this is the timebomb timeline, right?
coq_makefile to error on all warnings by default and is shipped in 8.11coq_makefile option in opam packages, virtually all OCaml opam packages for Coq 8.13 and later that use coq_makefile are broken on OCaml 4.13 Théo Zimmermann (Oct 28 2021 at 09:54):Enrico Tassi said:
For that you need to bring it up at the call, and convince Théo Zimmermann and Emilio Jesús Gallego Arias
I don't know why you seem to indicate that I've had any role into making this change happen and I would need to be convinced to revert it. If you re-read this PR discussion (like I just did), all my comments were about warning that if this was turned on by default, it needed to be clearly documented how to change this setting.
Théo Zimmermann (Oct 28 2021 at 09:54):However, I don't get how @Karl Palmskog gets his assessment that "hundreds" of packages would need to be changed since this is only about OCaml warnings and therefore plugins.
Théo Zimmermann (Oct 28 2021 at 09:56):Adding OCAMLWARN= to the plugin packages (much like Dune's -p) doesn't seem like such a big deal to me, but I'm not an opam repo maintainer.
Théo Zimmermann (Oct 28 2021 at 09:57):Anyway, I don't care which solution is chosen: patching Coq and previous releases in opam, or changing package definitions. But clearly, we shouldn't have fatal warnings in opam package definitions, this goes against standard recommendations.
Karl Palmskog (Oct 28 2021 at 10:54):it's a bit strange to me that the OCAMLWARN change was never mentioned explicitly (i.e., with the word OCAMLWARN) in the Coq release notes
Enrico Tassi (Oct 28 2021 at 11:21):Paolo Giarrusso said:
well: change it in CI _and_ on all developers’ machines at dev time, really. I still think it’s the right choice.
As a dev I'm fine having warnings be displayed as such, and on my CI have them be fatal. Since #dev > #CI setup I think it should be the other way around. The fact that "disable fatal warnings" is number one FAQ in dune suggests I'm not the only one.
Enrico Tassi (Oct 28 2021 at 11:26):Théo Zimmermann said:
Enrico Tassi said:
For that you need to bring it up at the call, and convince Théo Zimmermann and Emilio Jesús Gallego Arias
I don't know why you seem to indicate that I've had any role into making this change happen
No hard feelings, but from the PR I cited you seem to believe it is the right default:
While I certainly agree that developing without warnings is doable and should be preferred in published projects, allowing warnings is useful when starting up, so even if strongly discouraged it must be possible and documented in a way that is not hackish.
Unless I misread your sentence, you strongly discourage the other default.
Théo Zimmermann (Oct 28 2021 at 11:50):You are over interpreting this as my position rather that what we end up doing as a group (by changing this default). If you look at all my comments (there or in the issue that led to this), all I've expressed was caution... Anyway, my response was just to say that I wasn't the one that needed to be convinced. I expect Emilio is.
Théo Zimmermann (Oct 28 2021 at 11:51):Karl Palmskog said:
it's a bit strange to me that the
OCAMLWARNchange was never mentioned explicitly (i.e., with the wordOCAMLWARN) in the Coq release notes
Indeed, I agree that it should have been documented in the release notes as well (dev/doc/changelog.md is the place where this was documented, and there, instead of talking about bors, which is completely irrelevant, talking about OCAMLWARN would have been good).
Karl Palmskog (Oct 28 2021 at 12:33):I concede that with only 8.13 and later, the number of individual packages affected may be smaller than what I originally feared above ("hundreds"). But it's time-consuming from an opam viewpoint to figure out whether a certain package actually builds OCaml code or not.
Emilio Jesús Gallego Arias (Oct 28 2021 at 14:42):This is a tricky one, we should discuss in the call, for now we should indeed hotfix Coq so warning 70 is not fatal, as we do for some
Emilio Jesús Gallego Arias (Oct 28 2021 at 14:43):indeed properly managing warnings is hard, a configure flag is not enough, you need something like different compilation profiles, even Dune's 2 profiles, dev and release are not enough, and people is discussing how to improve that
Emilio Jesús Gallego Arias (Oct 28 2021 at 14:43):my only point is that ignoring warnings is not right
Emilio Jesús Gallego Arias (Oct 28 2021 at 14:43):our CI should build totally silent
Emilio Jesús Gallego Arias (Oct 28 2021 at 14:44):in Coq we got used somehoe to people ignoring compilation output as it is so verbose
Emilio Jesús Gallego Arias (Oct 28 2021 at 14:44):but this is not something IMHO to encourage
Karl Palmskog (Oct 28 2021 at 14:50):@Emilio Jesús Gallego Arias OK will you add it to the call topics?
Emilio Jesús Gallego Arias (Oct 28 2021 at 14:51):Sure, for now I suggest we just add warning 70 to the list of allowed warnings
Emilio Jesús Gallego Arias (Oct 28 2021 at 14:51):we could backtrack on the -warn-error PR too
Emilio Jesús Gallego Arias (Oct 28 2021 at 14:51):I dunno
Karl Palmskog (Oct 28 2021 at 14:52):I mean, almost all plugins in the Coq opam repo are currently broken on 4.13
Karl Palmskog (Oct 28 2021 at 14:53):if this is not reason enough to roll back the whole OCAML_WARN thing, then I don't know what is. There will be new warnings from the OCaml compiler probably every release
Karl Palmskog (Oct 28 2021 at 14:54):there is just no way we are going to start enforcing OCAML_WARN= in opam packages submitted to the repo, because this requires reviewers to actually look through each package source code and figure out the build system
Emilio Jesús Gallego Arias (Oct 28 2021 at 15:04):Not sure what do you mean, what's wrong with adding 70 to the list of OK warning?
Karl Palmskog (Oct 28 2021 at 15:06):it means all plugin packages using coq_makefile will break immediately again when the OCaml compiler introduces a new warning with a new number (e.g., 71)
Karl Palmskog (Oct 28 2021 at 15:08):for all Dune packages, everybody knows to use -p, and we can also see that it's a package using Dune. But opam package reviewers can't even see that something is using coq_makefile
Karl Palmskog (Oct 28 2021 at 15:09):so we will not catch a missing OCAML_WARN=, and I think it's absurd to put it in every package that uses make, or what are you proposing?
Karl Palmskog (Oct 28 2021 at 15:11):the only reasonable thing to do in my view is to make OCAML_WARN= the default for coq_makefile in coq.8.13.0. ... coq.8.14.0. I don't see how this affects any Coq dev CI.
Karl Palmskog (Oct 28 2021 at 15:19):@Emilio Jesús Gallego Arias you argued the following in the PR:
there is no reason to ever disable any of the warnings we enable in "production" code
Now we see that OCaml regularly introduces new warnings, and this will break code that was written before the OCaml compiler was even released. "[N]o reason to ever disable [warnings]" is an untenable position, in my book.
Théo Zimmermann (Oct 28 2021 at 15:22):Karl Palmskog said:
there is just no way we are going to start enforcing
OCAML_WARN=in opam packages submitted to the repo, because this requires reviewers to actually look through each package source code and figure out the build system
Indeed, that makes sense. So changing the default in Coq seems to be the only option.
Gaëtan Gilbert (Oct 28 2021 at 15:26):we could define the enabled warnings exhaustively instead of using a-some stuff
Théo Zimmermann (Oct 28 2021 at 15:31):This would indeed be a much more robust solution for compatibility with future OCaml versions.
Guillaume Melquiond (Oct 28 2021 at 15:44):And I want to stress again that the OCaml developers discourage the use of -warn-error. Let me quote the documentation of the compiler: "it is not recommended to use the -warn-error option in production code, because it will almost certainly prevent compiling your program with later versions of OCaml when they add new warnings or modify existing warnings." (which is exactly what is currently happening)
Théo Zimmermann (Oct 28 2021 at 15:46):The "modify existing warning" line seems to rule out the option proposed by @Gaëtan Gilbert (at least according to these guidelines).
Guillaume Melquiond (Oct 28 2021 at 15:49):Yes, we should be careful with any existing warning that relies on an analysis that is not syntactic in an obvious way.
Emilio Jesús Gallego Arias (Oct 28 2021 at 16:44):A few comments:
Emilio Jesús Gallego Arias (Oct 28 2021 at 16:49):So I dunno, for now we have many ways to patch this, but we should think a bit more in the medium term on what kind of demands we make from plugins. Indeed, maybe making a reasoned list of warnings that we don't allow in the CI as @Gaëtan Gilbert proposes is the best, and we can just say "Coq's CI requires for code hygiene that OCaml plugins don't raise any of the following warnings: ...."
Emilio Jesús Gallego Arias (Oct 28 2021 at 16:49):And that's unrelated but that warning 70 enabled by default is really a bogus bogus decision by OCaml devs
Emilio Jesús Gallego Arias (Oct 28 2021 at 16:50):when there are so many people that don't write mli files due to their painful properties
Emilio Jesús Gallego Arias (Oct 28 2021 at 16:50)::
Emilio Jesús Gallego Arias (Oct 28 2021 at 16:50)::S
Karl Palmskog (Oct 28 2021 at 16:53):it's a bit strange to me to weigh Coq's CI on one hand and lots of plugins in Coq's opam repo on the other (and say that "CI matters more" as was done in that PR). Many projects in Coq's CI are never released and are not in any way organized to be consumed by Coq end users
Gaëtan Gilbert (Oct 28 2021 at 16:55):plugins not in CI don't matter
Karl Palmskog (Oct 28 2021 at 16:55):if you want to impose certain coding standards in Coq's CI this should not in my view have to be a problem for plugin devs and users (that want to use a released Coq version)
Karl Palmskog (Oct 28 2021 at 16:56):so as soon as a Coq opam package with a plugin for 8.13 is published, it's OK to break it, since not in CI?
Emilio Jesús Gallego Arias (Oct 28 2021 at 17:03):sorry @Karl Palmskog I don't understand what you mean
Emilio Jesús Gallego Arias (Oct 28 2021 at 17:03):You are talking of now or of the previous discussion?
Théo Zimmermann (Oct 28 2021 at 17:08):Gaëtan Gilbert said:
plugins not in CI don't matter
This may come as harsh so I feel obligated to rephrase this: it is the official position of the Coq development team that all authors of plugins should get their plugins into Coq's CI. We are committed to maintaining the plugins that get added to the CI and have no restriction on what can be added. However, we do not commit to anything when plugin authors do not submit their plugins into Coq's CI.
That being said, I'm not sure whether this was relevant to the current discussion.
Karl Palmskog (Oct 28 2021 at 17:31):what I mean is that the whole error-on-warnings was introduced explicitly for Coq CI purposes, but then shipped to end users in coq_makefile and causing problems for them. Instead, why not use one coq_makefile in CI and ship a different one?
Gaëtan Gilbert (Oct 28 2021 at 17:37):we could also switch warnings off in the release commit
Emilio Jesús Gallego Arias (Oct 28 2021 at 17:59):Ah, I see @Karl Palmskog , the reason was what I said, the idea was that plugin devs would get the same dev experience than in the Coq's CI
Emilio Jesús Gallego Arias (Oct 28 2021 at 18:00):But yeah, this is not easy to solve well without something like profiles
Emilio Jesús Gallego Arias (Oct 28 2021 at 18:00):and even that has many shortcomings, but I mentioned some day people at upstream OCaml / Dune are tying to come up with better ways
Emilio Jesús Gallego Arias (Oct 28 2021 at 18:00):by the way, IMHO we should deprecate coq_makefile for plugins
Emilio Jesús Gallego Arias (Oct 28 2021 at 18:01):there are linking issues tho, but for pure OCaml code I think it is pretty safe to recommend people to switch to dune
Karl Palmskog (Oct 28 2021 at 18:01):I'm favor of deprecating coq_makefile for plugins, but Dune-Coq 1.0 needs to come first, IMO
Emilio Jesús Gallego Arias (Oct 28 2021 at 18:01):the plugin dev experience is much better
Emilio Jesús Gallego Arias (Oct 28 2021 at 18:01):Karl Palmskog said:
I'm favor of deprecating coq_makefile for plugins, but Dune-Coq 1.0 needs to come first, IMO
I mean only the ocaml parts, so that's independent from (lang coq)
Emilio Jesús Gallego Arias (Oct 28 2021 at 18:02):it should be fairly easy to use dune to build the .cmxs file, and coq_makefile for the rest
Karl Palmskog (Oct 28 2021 at 18:02):but nearly all plugins do provide a Coq interface (.v file). Do you think they should use Dune for the OCaml parts and then coq_makefile for the Coq part?
Karl Palmskog (Oct 28 2021 at 18:02):I think that's a terrible experience
Emilio Jesús Gallego Arias (Oct 28 2021 at 18:02):why?
Emilio Jesús Gallego Arias (Oct 28 2021 at 18:03):it is actually better than the one now I think
Karl Palmskog (Oct 28 2021 at 18:03):what is even the top level build command?
Emilio Jesús Gallego Arias (Oct 28 2021 at 18:03):make
Emilio Jesús Gallego Arias (Oct 28 2021 at 18:03):coq_makefile can just call dune on the plugins
Karl Palmskog (Oct 28 2021 at 18:03):I don't want to have a separate package and invoke Dune in my makefile
Emilio Jesús Gallego Arias (Oct 28 2021 at 18:03):that would be automatically done by coq_makefile
Emilio Jesús Gallego Arias (Oct 28 2021 at 18:04):but developing any kind of OCaml code using coq_makefile is a PITA IMHO
Emilio Jesús Gallego Arias (Oct 28 2021 at 18:04):many things are missing
Karl Palmskog (Oct 28 2021 at 18:04):mixing Dune and make in any way has been absolutely terrible for me, not least due to build hygiene and _build
Karl Palmskog (Oct 28 2021 at 18:07):don't you even have to set up _CoqProject to point to _build currently?
Emilio Jesús Gallego Arias (Oct 28 2021 at 19:05):A bit of plumbing would be needed, btw it is also quite easy to have coq_makefile output to _build
Emilio Jesús Gallego Arias (Oct 28 2021 at 19:06):as we do in the main coq_makefile
Emilio Jesús Gallego Arias (Oct 28 2021 at 19:06):tell me about how much fun is mixing dune and make, as I had to build the current bridge we have in Coq and I don't even use :/
Théo Zimmermann (Oct 29 2021 at 08:19):If that's easy to do, making coq_makefile rely on Dune for building OCaml parts doesn't sound so bad, especially given that Dune is already a dependency of Coq.
Karl Palmskog (Oct 29 2021 at 08:21):OK, as long as coq_makefile users do not need to have any idea that Dune is used or need to make special Dune stuff in _CoqProject, then it's fine by me
Théo Zimmermann (Oct 29 2021 at 08:24):As long as it is easy to set up, I'd say. But for this to have a point, of course plugin authors should write Dune files, otherwise how do they get the benefits?
Théo Zimmermann (Oct 29 2021 at 08:24):(Dune files for OCaml parts)
Guillaume Melquiond (Oct 29 2021 at 08:27):Wasn't the idea that coq_makefile would generate the Dune infrastructure for all the .ml[g] files in its input? I guess I misunderstood.
Karl Palmskog (Oct 29 2021 at 08:28):Guillaume Melquiond said:
Wasn't the idea that
coq_makefilewould generate the Dune infrastructure for all the.ml[g]files in its input? I guess I misunderstood.
I was hoping for this to be the intended goal, but I'm not sure now due to Théo's comment.
Enrico Tassi (Oct 29 2021 at 08:32):If we use dune, we still have to call it with -p from the opam file (so that warnings are non fatal). So it has the same cost of adding OCAML_WARN=...
Théo Zimmermann (Oct 29 2021 at 08:34):Karl Palmskog said:
Guillaume Melquiond said:
Wasn't the idea that
coq_makefilewould generate the Dune infrastructure for all the.ml[g]files in its input? I guess I misunderstood.I was hoping for this to be the intended goal, but I'm not sure now due to Théo's comment.
Maybe I'm the one who misunderstood...
Théo Zimmermann (Oct 29 2021 at 08:37):Enrico Tassi said:
If we use dune, we still have to call it with
-pfrom the opam file (so that warnings are non fatal). So it has the same cost of addingOCAML_WARN=...
If the call to Dune is explicit, it's easy for reviewers to make sure that -p is present. But if the call is implicit, that's indeed a problem.
Enrico Tassi (Oct 29 2021 at 09:13):Bu that is the whole point. We have two options, IMO:
OCAML_WARN= in the old ones, and dune -p in the new ones, and we review things stay like this)coq_makefile work as they are by reverting the default (and we export OCAML_WARN=-warn-error in our CI, and we require projects in our CI to do the same export in their CI)2 is much more end user friendly almost immediately (but requires some work from the devs).
1 is a lot of work by devs that eventually leads to a user friendly situation (e.g. when all packages use one way or another dune).
I would pick 2 of course (which does not prevent pursuing 1 in the long term)
Gaëtan Gilbert (Oct 29 2021 at 09:22):2 is ok for me
Karl Palmskog (Oct 29 2021 at 09:23):for the record, I believe we have already enforced dune -p in existing packages, and this is easy to check
Emilio Jesús Gallego Arias (Oct 29 2021 at 10:11):2 is not very dev friendly tho, devs will see their plugins to compile locally, but fail in Coq's CI
Emilio Jesús Gallego Arias (Oct 29 2021 at 10:11):1 is also out of the question
Emilio Jesús Gallego Arias (Oct 29 2021 at 10:12):You can have coq_makefile actually realize if it is being called from OPAM, and maybe in this case assume it is a release build?
Emilio Jesús Gallego Arias (Oct 29 2021 at 10:13):dune -p is more important as to disable composition [that is to say, pass --only-packages], it is also easy to check by the opam linter, and there is a chance that next opam versions won't require a build field for dune packages [finally!]
Emilio Jesús Gallego Arias (Oct 29 2021 at 10:14): Gaëtan Gilbert (Oct 29 2021 at 10:19):let's not do opam-only behaviour
Théo Zimmermann (Oct 29 2021 at 11:19):Emilio Jesús Gallego Arias said:
- [having coq_makefile check whether they are inside opam build] seems Ok, has only the small drawback of being too lenient with warnings for very special situations where a dev pipes dev build commands over a full opam shell
That's basically the most common CI setup.
Enrico Tassi (Oct 29 2021 at 11:47):Emilio Jesús Gallego Arias said:
2 is not very dev friendly tho, devs will see their plugins to compile locally, but fail in Coq's CI
no, if
... , and we require projects in our CI to do the same export in their CI
Enrico Tassi (Oct 29 2021 at 11:48):We require them to run CI, we can as well ask them to add export: OCAML_WARN=.... to their setup (it is one line)
Emilio Jesús Gallego Arias (Oct 29 2021 at 11:50):My preference is for something that kinda works out of the box; opam-only is not such a problem, we can document in coq_makefile that setting COQ_MAKEFILE_RELEASE should be done for packages in all packaging systems, and you can add a bit of code that detects if inside opam and sets that automatically to coq_makefile
Emilio Jesús Gallego Arias (Oct 29 2021 at 11:50):IMHO any solution that involves modifying packages is less preferred, the more we can gather this kind of stuff in a central, common place the easiest is to maintain
Emilio Jesús Gallego Arias (Oct 29 2021 at 11:50):Dune has a bit of opam-specific stuff and has worked very well
Emilio Jesús Gallego Arias (Oct 29 2021 at 11:51):tho indeed, the dev vs release build modes have confused a lot of people doing packages; but IMHO that's more a fault of the docs
Emilio Jesús Gallego Arias (Oct 29 2021 at 11:51):now that we are doing the Coq survey, the OCaml survey highglighted how confusing dune docs are
Emilio Jesús Gallego Arias (Oct 29 2021 at 11:52):One tricky thing with coq_makefile tho is that it is a two-phase system, in the sense that you generated a makefile, and then you run that makefile, that proves quite tricky to maintain as some people do distribute the generate makefile
Enrico Tassi (Oct 29 2021 at 11:56):Emilio Jesús Gallego Arias said:
IMHO any solution that involves modifying packages is less preferred, the more we can gather this kind of stuff in a central, common place the easiest is to maintain
So you are suggesting to follow option 2 as well?
Enrico Tassi (Oct 29 2021 at 11:57):Oh, I see, you want the default to be dynamic
Karl Palmskog (Oct 29 2021 at 11:57):if there was any doubt, I'm strongly in favor of option 2 over option 1, but open to variations on option 2.
Enrico Tassi (Oct 29 2021 at 11:58):My problem with detecting "the release mode" is that it looks brittle: we can detect opam maybe, but what about nix, debian, ...
Enrico Tassi (Oct 29 2021 at 12:01):If we flip the default, there is no detection heuristic needed.
Karl Palmskog (Oct 29 2021 at 12:01):even in GitHub repos, does anyone really want error-on-warnings for plugins by default? If I just do make from CLI, very annoying to have to figure out to pass some environment variable to get the thing to compile
Enrico Tassi (Oct 29 2021 at 12:02):Well, if you use dune this is what you get. But they got it wrong, clearly.
Karl Palmskog (Oct 29 2021 at 12:02):sure, but there it is at least a flag -p that everyone is aware of, rather than an environment variable
Enrico Tassi (Oct 29 2021 at 12:03):hum, dune build does not pass -p
Enrico Tassi (Oct 29 2021 at 12:03):but yes, it is better documented for sure
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:08):Enrico Tassi said:
Well, if you use dune this is what you get. But they got it wrong, clearly.
Why is that wrong? Poorly documented yes, but wrong?
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:09):Enrico Tassi said:
My problem with detecting "the release mode" is that it looks brittle: we can detect opam maybe, but what about nix, debian, ...
This has to be documented, in the packaging section of the coq_makefile manual, as I mentioned we would just tell people "do coq_makefile --release" however, due to the current setup that is not uniform in terms of coq_makefile pre-boot stage, that won't be helpful.
Enrico Tassi (Oct 29 2021 at 12:09):Well, it is FAQ number one. This does not mean it is badly documented, but that everybofy wants to flip the bit, IMO.
And I heard they wanted to reconsider it for 3.0, but you are surely better informed on this than me.
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:10):Karl Palmskog said:
even in GitHub repos, does anyone really want error-on-warnings for plugins by default? If I just do
makefrom CLI, very annoying to have to figure out to pass some environment variable to get the thing to compile
So you say it is ok to ignore warnings? Then why to have warnings in the first place?
Enrico Tassi (Oct 29 2021 at 12:10):Nobody wants to ignore them.
Karl Palmskog (Oct 29 2021 at 12:10):most of us are just trying to get work done by possibly reusing someone's code
Karl Palmskog (Oct 29 2021 at 12:11):if the plugin outputs something I like, then I go with it, regardless of warnings. But if I get stuck on compilation I can't even try the thing.
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:11):Enrico Tassi said:
Well, it is FAQ number one. This does not mean it is badly documented, but that everybofy wants to flip the bit, IMO.
And I heard they wanted to reconsider it for 3.0, but you are surely better informed on this than me.
They want a more flexible mechanism as things get tricky with profiles and vendoring and conflicting warning sets, but so far, on the contrary, at the scale dune has been used, the current setup has resulted in noise-free warning-free builds for devs, which is a huge success
Karl Palmskog (Oct 29 2021 at 12:13):in my view, Coq is still mainly about making scientists productive in their research, and very few venues will reject your paper because your code emits warnings
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:13):Karl Palmskog said:
even in GitHub repos, does anyone really want error-on-warnings for plugins by default? If I just do
makefrom CLI, very annoying to have to figure out to pass some environment variable to get the thing to compile
This is not what happens, except in the rare even that a new OCaml version is released, and triggers a new warning; we merged the strict warning PR a few years ago and the problem just happens now. By the way, there is a lot more intrincancies on this, as actually a few plugins in the CI ignore coq_makefile setup and they don't follow our warning policy, etc... It seems to me few people do look at the build logs
Karl Palmskog (Oct 29 2021 at 12:14):due to this warning, almost every plugin that you clone+compile with 4.13 breaks on make. The jury is still out on how frequently this will happen going forward.
Enrico Tassi (Oct 29 2021 at 12:14):It happened before with coq-elpi on a warning about a missing labelled argument. I just didn't realize it could have been everywhere.
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:14):Karl Palmskog said:
in my view, Coq is still mainly about making scientists productive in their research, and very few venues will reject your paper because your code emits warnings
Warnings are a problem for us in the CI, to each person their use case I guess
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:15):For me any solution that requires modifying packages / setup is not OK
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:15):We should solve this in Coq
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:15):Things gotta work out of the box
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:15):without configuration
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:15):I recall when RoR got released, how it quickly gained traction
Enrico Tassi (Oct 29 2021 at 12:16):we just disagree on the "without warnings" part ;-)
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:16):Enrico Tassi said:
we just disagree on the "without warnings" part ;-)
So it is OK for you to have noisy builds?
Enrico Tassi (Oct 29 2021 at 12:16):totally yes on my machine, not on my CI
Enrico Tassi (Oct 29 2021 at 12:17):I want to push warning free commits, no questions asked.
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:17):You can do that easily with a profile used only on your local build
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:18):but indeed, things get tricky, I guess you would have CI failing often
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:18):if you are used to ignore warnigns
Karl Palmskog (Oct 29 2021 at 12:18):and this profile we are all expected to figure out and set up?
Enrico Tassi (Oct 29 2021 at 12:18):no, not even in dune, since profiles encompass more options
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:18):Karl Palmskog said:
and this profile we are all expected to figure out and set up?
No because devs should be warning-free in supported versions
Enrico Tassi (Oct 29 2021 at 12:19):what is hard to understand to me is why you identify "ignore warnings" with "still get a binary which can be run"..
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:19):That's a specific customization Enrico wants
Enrico Tassi (Oct 29 2021 at 12:19):I'm not blind, If I see one, I'm going to fix it. But I may want to run the binary before doing that.
Karl Palmskog (Oct 29 2021 at 12:20):I also do not want someone to prevent me from doing work locally due to warnings
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:20):Only case to ignore warnings is in packages, as to cover new, yet unhandled warnings
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:20):Enrico Tassi said:
I'm not blind, If I see one, I'm going to fix it. But I may want to run the binary before doing that.
I see your point, but there is a lot of empirical evidence that if you allow this, then devs just go ahead and ignore the warnings
Karl Palmskog (Oct 29 2021 at 12:20):so do you think warning 70 is a good thing just because it is a warning?
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:20):see the current set of warnings cI outputs, tens of thousand of lines last time I looked
Karl Palmskog (Oct 29 2021 at 12:21):to be honest one might consider forking OCaml to get rid of it
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:21):Karl Palmskog said:
so do you think warning 70 is a good thing just because it is a warning?
Why are you doing work in a yet untested OCaml version?
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:21):Warning 70 can be very useful of terribly annoying depending on the coding style
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:21):Dune just had to add a special flag to handle it
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:22):what there is no question is that warnings should not break packages
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:22):this we all agree
Enrico Tassi (Oct 29 2021 at 12:22):(debatable_warnings true)
Karl Palmskog (Oct 29 2021 at 12:22):if you go to ocaml.org it says "Release of OCaml 4.13.1", doesn't look untested to me
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:22):It was tested only for the main opam repos
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:22):so for coq-opam archive, totally unsupported
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:23):until there is a commit there that says "enabling CI for 4.13.1"
Karl Palmskog (Oct 29 2021 at 12:23):but there is no official list of OCaml versions supported by Coq devs, to my knowledge. Either Coq can be built on a version or it can't
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:23):Yes there is
Karl Palmskog (Oct 29 2021 at 12:24):why does the opam package then allow 4.13?
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:24):https://github.com/ocaml/dune/pull/4955
Karl Palmskog (Oct 29 2021 at 12:24):Emilio Jesús Gallego Arias said:
Yes there is
where? and has it been advertised to Coq users?
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:24):because Coq itself is supported
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:25):Anyways I'm not sure where you folks want to go here
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:25):The current state of the CI is pretty bad in terms of how noisy the builds are
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:25):basically we have all learnt to ignore output of coq_makefile
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:25):because we can't just parse the thing
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:26):anyways plugins authors chose to ignore already coq policy on warnigns
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:26):there is no question the current default for packages is wrong
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:27):@Karl Palmskog https://github.com/coq/coq/pull/14879 plus a few related commits
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:27):that were actually needed to get Coq running
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:27):by the way Coq won't work at all in OCaml 5.0
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:27):so you may want to start doing something on the coq-opam-archive
Karl Palmskog (Oct 29 2021 at 12:28):we do add upper bounds of OCaml versions of existing packages over time in the Coq opam archive
Karl Palmskog (Oct 29 2021 at 12:29):the problem here is that the package code is working fine on 4.13, but we can't build the package
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:29):So indeed, let's patch coq_makefile in the way we proposed above
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:30):There are very easy patches
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:30):that fix the stuff
Karl Palmskog (Oct 29 2021 at 12:30):OK, that sounds good to me, it avoids a huge amount of work to track down all plugins for 8.13 and 8.14.
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:30):I already mentioned all the options:
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:31):first is just a hotfix
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:31):second provides a more robust solution
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:31):anyways we got bigger problems in our hands
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:31):as we won't be able to use anything newer than OCaml 4.14 for a long time I feel
Karl Palmskog (Oct 29 2021 at 12:31):also an option (the one I prefer):
OCAML_WARN= the default, like before the PR https://github.com/coq/coq/pull/9605 Emilio Jesús Gallego Arias (Oct 29 2021 at 12:32):Then the warnings problem in the CI, is way more complex, that we need to discuss
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:32):Karl Palmskog said:
also an option (the one I prefer):
- make
OCAML_WARN=the default, like before the PR https://github.com/coq/coq/pull/9605
This provides a bad experience for devs, as I have mentioned a few times
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:32):I don't see why your proposal is better, seems worse in every aspect
Karl Palmskog (Oct 29 2021 at 12:32):sure, but devs don't care about 8.13 and 8.14
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:33):they may care, I'm still releasing serapi for 8.13 for example
Karl Palmskog (Oct 29 2021 at 12:33):but they are not used in CI
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:33):even in master it provides a bad experience
Karl Palmskog (Oct 29 2021 at 12:33):can't we at least make OCAML_WARN= the default for 8.13 and 8.14?
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:33):why should we do that when we have better solutions?
Karl Palmskog (Oct 29 2021 at 12:34):it's not a better solution in my view
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:34):and why we should do a 8.13 / 8.14 only solution, what aobut master?
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:34):why it is not better?
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:34):what problem my solution creates that yours doesn't?
Karl Palmskog (Oct 29 2021 at 12:34):we get a new timebomb for 8.13 and 8.14 when OCaml 4.13.2 or 4.14 introduce a bunch more warnings
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:34):nope
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:35):if we do solution 1), we do in the way @Gaëtan Gilbert mentioned, we use a positive list
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:35):if we do solution 2)
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:35):packages are built wihtout -warn-error so we don't care
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:35):but devs get a consistent experience
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:35):your solution is a hell for devs
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:36):they will push a commit that will work fine for them locally
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:36):but will break Coq CI
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:36):we should actually try to see the huge mess I'd create
Karl Palmskog (Oct 29 2021 at 12:36):my primary concern is 8.13 and 8.14, which most devs don't care about
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:36):we need a solution for master too
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:36):even if they don't care, after all the time I've been tracking Coq's CI
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:37):that would be a mess, unless of course we disable the warnings in the CI of Coq too
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:37):so OK, in that sense, feel free to do for 8.13 / 8.14 whatever you want, let's say the CI there is not a big deal
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:37):but we still need a solution for master
Karl Palmskog (Oct 29 2021 at 12:37):but why do we have to do the same solution for 8.13, 8.14 and master?
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:37):no we don't, if you wanna do double the work that's fine I guess
Karl Palmskog (Oct 29 2021 at 12:38):I don't have as many concerns about master, there we can at least prepare for whatever is chosen for 8.15 in the opam archive
Karl Palmskog (Oct 29 2021 at 12:39):8.13 and 8.14 packages are broken right now, 8.15 "packages" are in extra-dev and the like, where breakage is a regular thing
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:40):Yeah and what's preventing the one-line fix?
Karl Palmskog (Oct 29 2021 at 12:41):I don't know what packages are broken, I don't even know which packages are plugins most of the time
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:46):Sorry I don't follow at all, anyways here's the fix for 8.14 https://github.com/ocaml/opam-repository/pull/19903
Karl Palmskog (Oct 29 2021 at 12:47):this [the opam-repository PR] doesn't solve future timebombs as per above
Karl Palmskog (Oct 29 2021 at 12:47):with "one-line fix" I thought you meant inserting OCAML_WARN= everywhere
Emilio Jesús Gallego Arias (Oct 29 2021 at 12:50):I have been answering the same stuff over and over for all this thread, I'm sorry I'm not sure how can I do better
Enrico Tassi (Oct 29 2021 at 12:56):@Emilio Jesús Gallego Arias @Gaëtan Gilbert are you taking care of the hotfix (positive list rather than negative, or flip the default, the one you prefer)?
Enrico Tassi (Oct 29 2021 at 13:17):https://github.com/coq/coq/pull/15092
Emilio Jesús Gallego Arias (Oct 29 2021 at 13:18):Yup, I saw your message after the PR
Emilio Jesús Gallego Arias (Oct 29 2021 at 13:18):That should be a bit better
Emilio Jesús Gallego Arias (Oct 29 2021 at 13:19):what to do with warnings is a bit more complex, we can chat in the call some of these days
Emilio Jesús Gallego Arias (Oct 29 2021 at 13:19):if we consider the plugins to be vendored
Emilio Jesús Gallego Arias (Oct 29 2021 at 13:19):for example Dune policy is to never override the set of warnings the original authors chose to
Emilio Jesús Gallego Arias (Oct 29 2021 at 13:20):I dunno, that's a complex situation
Emilio Jesús Gallego Arias (Oct 29 2021 at 13:29):For this particular problem, we may want to add constraints on OCaml < 4.13 if we want to the coq packages not including the warning tweak
Paolo Giarrusso (Oct 29 2021 at 17:15):@Emilio Jesús Gallego Arias what you “mentioned a few times” does not seem accurate
Paolo Giarrusso (Oct 29 2021 at 17:15):or at least, I’m missing a huge step.
Paolo Giarrusso (Oct 29 2021 at 17:16):to be sure, you’re complaining about the industry standard in general, right?
Emilio Jesús Gallego Arias (Oct 29 2021 at 17:16):I mean I've mentioned the drawback of having a different dev vs ci setup
Emilio Jesús Gallego Arias (Oct 29 2021 at 17:16):a few times
Emilio Jesús Gallego Arias (Oct 29 2021 at 17:16):Paolo Giarrusso said:
to be sure, you’re complaining about the industry standard in general, right?
what industry standard?
Paolo Giarrusso (Oct 29 2021 at 17:18):yes, you mentioned it a few times, but we’ll agree that repeating an argument does not, per se, make it true, right?
Paolo Giarrusso (Oct 29 2021 at 17:18):also “industry standard” per se doesn’t make something a good idea by itself.
Paolo Giarrusso (Oct 29 2021 at 17:19):on the merits: the problematic experience seems to be the one where the warnings are shown in both CI and locally, but they only fail the build in CI. Is that right?
Paolo Giarrusso (Oct 29 2021 at 17:19):I completely agree that, without CI, developers are prone to ignore warning.
Paolo Giarrusso (Oct 29 2021 at 17:21):and I agree that “you only get the text of errors in CI” would be bad. But as long as they’re shown, and the developer knows the CI policy, the information seems to be there.
Paolo Giarrusso (Oct 29 2021 at 17:21):That only leaves the case of plugins outside Coq CI; I agree, but others have argued against prioritizing that.
Emilio Jesús Gallego Arias (Oct 29 2021 at 21:46):Paolo Giarrusso said:
yes, you mentioned it a few times, but we’ll agree that repeating an argument does not, per se, make it true, right?
I am not following at all, sorry
Emilio Jesús Gallego Arias (Oct 29 2021 at 21:47):Paolo Giarrusso said:
also “industry standard” per se doesn’t make something a good idea by itself.
ok and? I don't know what industry standard you are talking about sorry, and the search in the thread gives me nothing
Emilio Jesús Gallego Arias (Oct 29 2021 at 21:47):Paolo Giarrusso said:
That only leaves the case of plugins outside Coq CI; I agree, but others have argued against prioritizing that.
So you are arguing that not getting errors locally, but getting them in the CI is a good developer experience?
Emilio Jesús Gallego Arias (Oct 29 2021 at 21:48):Sorry, I have to difer here, that's a terrible [and wasteful] experience.
Emilio Jesús Gallego Arias (Oct 29 2021 at 21:48):The closer I can get my local setup to CI the better for me, it is extremely time-consuming to have address CI failures
Emilio Jesús Gallego Arias (Oct 29 2021 at 21:49):That's already a big pitfall IMHO, but moreover, a solution that requires modifying the setup of every package seems also like pretty painful to me.
Emilio Jesús Gallego Arias (Oct 29 2021 at 21:49):Especially when there are better altenatives, which don't suffer of such problems.
Can you point out again what the advantage of such a setup is? Because I still don't get it.
Paolo Giarrusso (Oct 29 2021 at 22:50):just to be sure.
Paolo Giarrusso (Oct 29 2021 at 22:51):the “terrible experience” would be getting all the same information, but as warnings not errors?
Paolo Giarrusso (Oct 29 2021 at 22:52):clearly, there must be some missing information, and I’d like to dig deeper.
Paolo Giarrusso (Oct 29 2021 at 22:53):the “industry standard” I was alluding to is “do not ship packages to end users with -warn-error” (or similar in other languages). The argument is the same as the one from the OCaml developers.
Paolo Giarrusso (Oct 29 2021 at 22:55):the recommended way to use dune also achieves that, and coq_makefile without -warn-error does too.
Paolo Giarrusso (Oct 29 2021 at 22:55):so, back to development setup.
Paolo Giarrusso (Oct 29 2021 at 22:56):actually, one more point on users: -warn-error also increases chances of bitrot.
Paolo Giarrusso (Oct 29 2021 at 22:58):for developers, it seems to me that, if you know CI uses -warn-error, and you want the same results locally, you just ensure your local build is warning-free. And for best results, use the same compiler version.
Paolo Giarrusso (Oct 29 2021 at 23:00):I’d also expect developers to have an easier time customizing build options (if it were needed, which it isn’t) than end users.
Paolo Giarrusso (Oct 29 2021 at 23:02):if coq_makefile doesn’t let developers customize it conveniently (by, say, reading some environment variable that lets you add -warn-error, if you really need), that should be fixed.
Paolo Giarrusso (Oct 29 2021 at 23:04):Can you point out again what the advantage of such a setup is? Because I still don't get it.
Paolo Giarrusso (Oct 29 2021 at 23:07):generally, it seems we’re going in circles; it might be the case that we’re failing to agree on the material facts of the case, potentially because we disagree on the value judgments about those facts.
Paolo Giarrusso (Oct 29 2021 at 23:10):I mean I've mentioned the drawback of having a different dev vs ci setup
Paolo Giarrusso (Oct 29 2021 at 23:10):a few times
Paolo Giarrusso (Oct 29 2021 at 23:11):yes, you mentioned it a few times, but we’ll agree that repeating an argument does not, per se, make it true, right?
I am not following at all, sorry
Paolo Giarrusso (Oct 29 2021 at 23:12):my reply was that yes, you’ve mentioned such drawbacks a few times. Each of those times, we’ve listened, and we disagreed. Repeating the same argument is not going to change our mind. To progress there, we’d have to understand where the difference comes from.
Paolo Giarrusso (Oct 29 2021 at 23:14):as the last point, I’ve worked with local warnings and -warn-error for months without any problems.
Paolo Giarrusso (Oct 29 2021 at 23:17):that is, as long as you know that all your warnings must be fixed to pass CI. If you start having local warnings that aren’t fatal in CI that’s a nightmare, so -warn-error should be the only difference.
Gaëtan Gilbert (Oct 30 2021 at 08:33):Paolo Giarrusso said:
the “terrible experience” would be getting all the same information, but as warnings not errors?
warnings kinda fly past what you see in the build log between all the OCAMLC / COQC (this doesn't apply for quiet mode dune build, but we're talking about coq_makefile)
also if you fix a warning in 1 file and run make again, incremental compilation means the warnings from other files don't get printed again
I think this can be compensated for if we make it easy to enable warn-error (that would also be convenient for CI) but does need to be known
Paolo Giarrusso (Oct 30 2021 at 09:28):Thanks for pointing out (some of) the missing facts to enable discussion progress :-)
Paolo Giarrusso (Oct 30 2021 at 09:29):Side point: I’d probably save the build log to a file and address all warnings in a pass, instead of rerunning the compiler. That could be _better_ than -warn-error, but YMMV of course.
Paolo Giarrusso (Oct 30 2021 at 09:34):I like your summary @Gaëtan Gilbert , but IOW: -warn-error seems to have some advantages for devs, disadvantages for end-users, and if need one choice for all, one side suffers (and we risk ending up in a shouting match). So “easy warn-error for devs”, if it can be technically done, seems a possible way out.
Paolo Giarrusso (Oct 30 2021 at 09:41):and even the (IMHO) baseline export COQ_MK_WARN_ERROR=1 (modulo exact naming) would already improve things, in that it restricts today’s problem to devs (who can disable it) — as long as CI keeps plugins mostly warning-free. Ignoring that inside opam (as some proposed) is not elegant but might have better tradeoffs in the most common scenarios.
Gaëtan Gilbert (Oct 30 2021 at 10:29):btw it should be possible to set a warn_error env variable in the docker images for ci too
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:09):Oh I see what you mean @Paolo Giarrusso , thanks for the write up; first, there is no question that -warn-error for users is a bug.
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:10):For developers, I am not an expert here, but last time I heard there was solid empirical experience that if devs don't use warn error, they just forget about the warnings
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:10):this costs a lot of money in the meidum term
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:10):so hence the default
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:10):in general, devs are terrible at anything that is not taken care for them
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:10):like running make twice, etc...
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:11):even when that stuff is run automatically they complain, for example linters
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:11):I do agree, personally I want to have to do nothing, and this is how I work today
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:12):my build system is runniing in the background, and I get real-time feedback on errors
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:12):and when I'm error free I know I'm good; I'd love for that to work for the test suite too
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:13):It is also important for me the part of the argument that packages should be configuration-free
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:13):any setup that involves people tweaking stuff for CI
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:13):is IMHO doomed to failure
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:14):the build / packaging system should have the right magic so the right thing is done in every situation
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:14):for example, in Debian, you do dh_coq and everything is taken care of
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:14):policy modifications go to dh_coq itself
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:15):unfortunately due to the way coq_makefile is desgined, we can't really have that
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:15):dune does a bit better, but not perfect
Karl Palmskog (Nov 02 2021 at 09:15):to me, the whole native stuff is an example of going in the opposite direction of configuration-free. For example, I don't even know what is the recommended way to handle all the following warnings in Coqtail that started showing up for 8.14:
Warning: native_compute disabled at configure time; falling back to
- vm_compute. [native-compute-disabled,native-compiler]
e.g., should we all now use vm_compute everywhere unless we really need native for speed?
Emilio Jesús Gallego Arias (Nov 02 2021 at 09:24):@Karl Palmskog that seems like a different issue [I guess it is fair to warn if you explicitly use native_compute and it is not available]
Enrico Tassi (Nov 02 2021 at 09:57):@Emilio Jesús Gallego Arias can you react to my comment on https://github.com/coq/coq/pull/15092 so that we can merge it and be done with this problem (in master)?
Paolo Giarrusso (Nov 02 2021 at 10:46):@Karl Palmskog agree on keeping that separate — native_compute discussions are bigger than this one
Paolo Giarrusso (Nov 02 2021 at 11:31):@Emilio Jesús Gallego Arias now we’re making progress; it seems that having the right setup for users and a good one for developers might require dune (not sure). That empirical evidence sounds likely, but that’s what -warn-error in CI is for. Re “fiddling with CI”, we can at least bring that down to export WARN_ERROR=y or such — and the Coq CI for plugins ensures that already.
Paolo Giarrusso (Dec 06 2021 at 12:51):Was any solution found? Equations just failed installation on 4.13.
Paolo Giarrusso (Dec 06 2021 at 12:52):CAMLOPT -c src/equations_plugin_mod.ml
File "src/equations_plugin_mod.ml", line 1:
Error (warning 70 [missing-mli]): Cannot find interface file.
Command exited with non-zero status 2
did you recompile Coq after doing opam update?
Karl Palmskog (Dec 06 2021 at 12:52):changes were merged to the general opam repo which suppress the 70 error. Everything will break again (on 8.13 and 8.14) if some new OCaml compiler warning is introduced, though.
Paolo Giarrusso (Dec 06 2021 at 12:54):Oh, this was patched in the _Coq_ package? I'll have to update my fork of that package
Karl Palmskog (Dec 06 2021 at 12:55):patching every plugin for 8.13 and 8.14 is simply not going to happen... the alternative in my mind was always to mark them incompatible with 4.13.
Paolo Giarrusso (Dec 06 2021 at 12:55):oh we agreed on that :-)
Karl Palmskog (Dec 06 2021 at 12:57):what I hope will happen for OCaml 5 is that we stay on 4.X-only as long as possible, and then completely drop all 4.X in one go. Then stuff like this is not likely to happen for a while.
Paolo Giarrusso (Dec 06 2021 at 12:58):Thanks but let me save you time — I found the patch
Paolo Giarrusso (Dec 06 2021 at 12:59):do you know if any 4.14 release is planned, or will OCaml go to 5.0?
Karl Palmskog (Dec 06 2021 at 13:00):to my knowledge, 4.14 will be the last 4.X release.
Paolo Giarrusso (Dec 06 2021 at 13:01):okay, so Coq _might_ need such a patch for 4.14 for any new warnings, but that's good enough since 5.x isn't supportable for now.
Paolo Giarrusso (Dec 06 2021 at 13:02):That's good enough to close the topic for me :-).
Karl Palmskog (Dec 06 2021 at 13:03):https://discuss.ocaml.org/t/the-road-to-ocaml-5-0/8584
Karl Palmskog (Dec 06 2021 at 13:03):for every major feature addition, seems they will lock down everything else (development, bugfixing, ...) for like 6 months. This does not seem like a good thing for Coq in general, unless there is a solid version like 4.07.1 again
Paolo Giarrusso (Dec 06 2021 at 13:24):4.14 looks like a long-term release, so hopefully that'll be (or become) stable. And 4.10.2 is already decent... the only reason I tried 4.13.1 is because of one bug on ARM that's first fixed there...
Paolo Giarrusso (Dec 06 2021 at 13:29):Last updated: Oct 13 2024 at 01:02 UTC