Stream: Coq users

Topic: coq-bignums installation fails


view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 28 2021 at 06:17):

One could downgrade coq to 8.13.2, investigate what coqprime supports, or fix the error

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Oct 28 2021 at 06:51):

hmm, I wonder if this is an OCaml 4.13.1 issue?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Oct 28 2021 at 07:25):

argh, there is no v8.14 branch in bignums.

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Oct 28 2021 at 07:54):

looks like switching to Dune solves the problem, but probably breaks things like native

view this post on Zulip Pierre Roux (Oct 28 2021 at 07:56):

Yes, please don't switch bignums to dune yet.

view this post on Zulip Karl Palmskog (Oct 28 2021 at 08:57):

just checked that this affects aac-tactics as well... big sigh

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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=

view this post on Zulip Enrico Tassi (Oct 28 2021 at 09:01):

It is the same with dune, you have to pass -p IIRC

view this post on Zulip Karl Palmskog (Oct 28 2021 at 09:01):

sure, but that Dune boilerplate has been there from the start

view this post on Zulip Enrico Tassi (Oct 28 2021 at 09:01):

I know...

view this post on Zulip Karl Palmskog (Oct 28 2021 at 09:02):

we are talking about probably hundreds of package definitions here

view this post on Zulip 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....

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Oct 28 2021 at 09:03):

no no, the variable is coq_makefile specific

view this post on Zulip 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...

view this post on Zulip Enrico Tassi (Oct 28 2021 at 09:08):

or make warnings non fatal which takes 1 minute

view this post on Zulip Karl Palmskog (Oct 28 2021 at 09:09):

you mean modify coq_makefile? Or where would that change be made?

view this post on Zulip Enrico Tassi (Oct 28 2021 at 09:09):

yes there is a default to flip, that is all

view this post on Zulip Karl Palmskog (Oct 28 2021 at 09:10):

but that would come out in 8.14.1 at the absolute earliest

view this post on Zulip Karl Palmskog (Oct 28 2021 at 09:10):

we would still be stuck with existing packages...

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Oct 28 2021 at 09:19):

OK, thanks, this means at least we know which Coq versions are affected for coq_makefile

view this post on Zulip Paolo Giarrusso (Oct 28 2021 at 09:20):

Can OCAMLWARN be set in the switch as an environment variable?

view this post on Zulip Karl Palmskog (Oct 28 2021 at 09:20):

I didn't realize the history here, but indeed a time bomb seems to have exploded

view this post on Zulip Paolo Giarrusso (Oct 28 2021 at 09:21):

That'd be a manual workaround, but it's a cheaper one.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Oct 28 2021 at 09:23):

indeed, that would make our CI pass, but fail in the user's hands

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 28 2021 at 09:25):

No, I meant Coq releases

view this post on Zulip Paolo Giarrusso (Oct 28 2021 at 09:25):

Isn't it only Coq 8.14.0 and maybe 8.13.late?

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Oct 28 2021 at 09:26):

no, the PR in question was in 8.11 I guess

view this post on Zulip Paolo Giarrusso (Oct 28 2021 at 09:26):

8.11 doesn't build with OCaml 4.13 I expect.

view this post on Zulip Enrico Tassi (Oct 28 2021 at 09:26):

IMO the best hotfix is $ git grep '\[make "-j' | wc -l

view this post on Zulip Enrico Tassi (Oct 28 2021 at 09:27):

which gives 1500 packages, then you can sed like s/]/ "CAMLWARN="]/

view this post on Zulip Enrico Tassi (Oct 28 2021 at 09:28):

it is hard to know if the package builds .ml files

view this post on Zulip Enrico Tassi (Oct 28 2021 at 09:28):

only these really need to be fixed

view this post on Zulip Enrico Tassi (Oct 28 2021 at 09:29):

ok, I see that

view this post on Zulip Paolo Giarrusso (Oct 28 2021 at 09:29):

That's looking for sed bugs, really, and that regexp seems far too strict.

view this post on Zulip Enrico Tassi (Oct 28 2021 at 09:29):

sure, it was "pseudo code"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Oct 28 2021 at 09:30):

I don't even know if it can print back

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Oct 28 2021 at 09:32):

Ok, but you want that patch to be merged upstream eventually

view this post on Zulip Paolo Giarrusso (Oct 28 2021 at 09:33):

Sure, you want the upstreaming as well.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Oct 28 2021 at 09:35):

it will at least never break something that works currently with coq_makefile (right?)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Oct 28 2021 at 09:46):

OK, so this is the timebomb timeline, right?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Oct 28 2021 at 11:51):

Karl Palmskog said:

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

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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 14:43):

my only point is that ignoring warnings is not right

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 14:43):

our CI should build totally silent

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 14:44):

but this is not something IMHO to encourage

view this post on Zulip Karl Palmskog (Oct 28 2021 at 14:50):

@Emilio Jesús Gallego Arias OK will you add it to the call topics?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 14:51):

we could backtrack on the -warn-error PR too

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 14:51):

I dunno

view this post on Zulip Karl Palmskog (Oct 28 2021 at 14:52):

I mean, almost all plugins in the Coq opam repo are currently broken on 4.13

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Oct 28 2021 at 15:26):

we could define the enabled warnings exhaustively instead of using a-some stuff

view this post on Zulip Théo Zimmermann (Oct 28 2021 at 15:31):

This would indeed be a much more robust solution for compatibility with future OCaml versions.

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 16:44):

A few comments:

view this post on Zulip 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: ...."

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 16:50):

:

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 16:50):

:S

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Oct 28 2021 at 16:55):

plugins not in CI don't matter

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 17:03):

sorry @Karl Palmskog I don't understand what you mean

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 17:03):

You are talking of now or of the previous discussion?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Oct 28 2021 at 17:37):

we could also switch warnings off in the release commit

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 18:00):

But yeah, this is not easy to solve well without something like profiles

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 18:00):

by the way, IMHO we should deprecate coq_makefile for plugins

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 18:01):

the plugin dev experience is much better

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Oct 28 2021 at 18:02):

I think that's a terrible experience

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 18:02):

why?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 18:03):

it is actually better than the one now I think

view this post on Zulip Karl Palmskog (Oct 28 2021 at 18:03):

what is even the top level build command?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 18:03):

make

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 18:03):

coq_makefile can just call dune on the plugins

view this post on Zulip Karl Palmskog (Oct 28 2021 at 18:03):

I don't want to have a separate package and invoke Dune in my makefile

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 18:03):

that would be automatically done by coq_makefile

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 18:04):

many things are missing

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Oct 28 2021 at 18:07):

don't you even have to set up _CoqProject to point to _build currently?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 19:06):

as we do in the main coq_makefile

view this post on Zulip 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 :/

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Oct 29 2021 at 08:24):

(Dune files for OCaml parts)

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Oct 29 2021 at 08:28):

Guillaume Melquiond said:

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.

I was hoping for this to be the intended goal, but I'm not sure now due to Théo's comment.

view this post on Zulip 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=...

view this post on Zulip Théo Zimmermann (Oct 29 2021 at 08:34):

Karl Palmskog said:

Guillaume Melquiond said:

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.

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...

view this post on Zulip Théo Zimmermann (Oct 29 2021 at 08:37):

Enrico Tassi said:

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=...

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.

view this post on Zulip Enrico Tassi (Oct 29 2021 at 09:13):

Bu that is the whole point. We have two options, IMO:

  1. we modify all the opam files (OCAML_WARN= in the old ones, and dune -p in the new ones, and we review things stay like this)
  2. we make packages using 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)

view this post on Zulip Gaëtan Gilbert (Oct 29 2021 at 09:22):

2 is ok for me

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 10:11):

1 is also out of the question

view this post on Zulip 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?

view this post on Zulip 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!]

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 10:14):

  1. [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

view this post on Zulip Gaëtan Gilbert (Oct 29 2021 at 10:19):

let's not do opam-only behaviour

view this post on Zulip Théo Zimmermann (Oct 29 2021 at 11:19):

Emilio Jesús Gallego Arias said:

  1. [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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 11:50):

Dune has a bit of opam-specific stuff and has worked very well

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Oct 29 2021 at 11:57):

Oh, I see, you want the default to be dynamic

view this post on Zulip 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.

view this post on Zulip 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, ...

view this post on Zulip Enrico Tassi (Oct 29 2021 at 12:01):

If we flip the default, there is no detection heuristic needed.

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Oct 29 2021 at 12:02):

Well, if you use dune this is what you get. But they got it wrong, clearly.

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Oct 29 2021 at 12:03):

hum, dune build does not pass -p

view this post on Zulip Enrico Tassi (Oct 29 2021 at 12:03):

but yes, it is better documented for sure

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 make from 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?

view this post on Zulip Enrico Tassi (Oct 29 2021 at 12:10):

Nobody wants to ignore them.

view this post on Zulip Karl Palmskog (Oct 29 2021 at 12:10):

most of us are just trying to get work done by possibly reusing someone's code

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 make from 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:15):

For me any solution that requires modifying packages / setup is not OK

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:15):

We should solve this in Coq

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:15):

Things gotta work out of the box

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:15):

without configuration

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:15):

I recall when RoR got released, how it quickly gained traction

view this post on Zulip Enrico Tassi (Oct 29 2021 at 12:16):

we just disagree on the "without warnings" part ;-)

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Oct 29 2021 at 12:16):

totally yes on my machine, not on my CI

view this post on Zulip Enrico Tassi (Oct 29 2021 at 12:17):

I want to push warning free commits, no questions asked.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:18):

but indeed, things get tricky, I guess you would have CI failing often

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:18):

if you are used to ignore warnigns

view this post on Zulip Karl Palmskog (Oct 29 2021 at 12:18):

and this profile we are all expected to figure out and set up?

view this post on Zulip Enrico Tassi (Oct 29 2021 at 12:18):

no, not even in dune, since profiles encompass more options

view this post on Zulip 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

view this post on Zulip 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"..

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:19):

That's a specific customization Enrico wants

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Oct 29 2021 at 12:20):

I also do not want someone to prevent me from doing work locally due to warnings

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Oct 29 2021 at 12:20):

so do you think warning 70 is a good thing just because it is a warning?

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Oct 29 2021 at 12:21):

to be honest one might consider forking OCaml to get rid of it

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:21):

Dune just had to add a special flag to handle it

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:22):

what there is no question is that warnings should not break packages

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:22):

this we all agree

view this post on Zulip Enrico Tassi (Oct 29 2021 at 12:22):

(debatable_warnings true)

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:22):

It was tested only for the main opam repos

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:22):

so for coq-opam archive, totally unsupported

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:23):

Yes there is

view this post on Zulip Karl Palmskog (Oct 29 2021 at 12:24):

why does the opam package then allow 4.13?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:24):

https://github.com/ocaml/dune/pull/4955

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:24):

because Coq itself is supported

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:25):

Anyways I'm not sure where you folks want to go here

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:25):

basically we have all learnt to ignore output of coq_makefile

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:25):

because we can't just parse the thing

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:26):

anyways plugins authors chose to ignore already coq policy on warnigns

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:26):

there is no question the current default for packages is wrong

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:27):

that were actually needed to get Coq running

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:27):

by the way Coq won't work at all in OCaml 5.0

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:27):

so you may want to start doing something on the coq-opam-archive

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:29):

So indeed, let's patch coq_makefile in the way we proposed above

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:30):

There are very easy patches

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:30):

that fix the stuff

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:30):

I already mentioned all the options:

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:31):

first is just a hotfix

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:31):

second provides a more robust solution

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:31):

anyways we got bigger problems in our hands

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Oct 29 2021 at 12:31):

also an option (the one I prefer):

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:32):

Karl Palmskog said:

also an option (the one I prefer):

This provides a bad experience for devs, as I have mentioned a few times

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Oct 29 2021 at 12:32):

sure, but devs don't care about 8.13 and 8.14

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:33):

they may care, I'm still releasing serapi for 8.13 for example

view this post on Zulip Karl Palmskog (Oct 29 2021 at 12:33):

but they are not used in CI

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:33):

even in master it provides a bad experience

view this post on Zulip Karl Palmskog (Oct 29 2021 at 12:33):

can't we at least make OCAML_WARN= the default for 8.13 and 8.14?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:33):

why should we do that when we have better solutions?

view this post on Zulip Karl Palmskog (Oct 29 2021 at 12:34):

it's not a better solution in my view

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:34):

why it is not better?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:34):

what problem my solution creates that yours doesn't?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:34):

nope

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:35):

if we do solution 2)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:35):

packages are built wihtout -warn-error so we don't care

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:35):

but devs get a consistent experience

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:35):

your solution is a hell for devs

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:36):

they will push a commit that will work fine for them locally

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:36):

but will break Coq CI

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:36):

we should actually try to see the huge mess I'd create

view this post on Zulip Karl Palmskog (Oct 29 2021 at 12:36):

my primary concern is 8.13 and 8.14, which most devs don't care about

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:36):

we need a solution for master too

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:37):

but we still need a solution for master

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 12:40):

Yeah and what's preventing the one-line fix?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Oct 29 2021 at 12:47):

this [the opam-repository PR] doesn't solve future timebombs as per above

view this post on Zulip Karl Palmskog (Oct 29 2021 at 12:47):

with "one-line fix" I thought you meant inserting OCAML_WARN= everywhere

view this post on Zulip 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

view this post on Zulip 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)?

view this post on Zulip Enrico Tassi (Oct 29 2021 at 13:17):

https://github.com/coq/coq/pull/15092

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 13:18):

Yup, I saw your message after the PR

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 13:18):

That should be a bit better

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 13:19):

if we consider the plugins to be vendored

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 13:20):

I dunno, that's a complex situation

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 29 2021 at 17:15):

@Emilio Jesús Gallego Arias what you “mentioned a few times” does not seem accurate

view this post on Zulip Paolo Giarrusso (Oct 29 2021 at 17:15):

or at least, I’m missing a huge step.

view this post on Zulip Paolo Giarrusso (Oct 29 2021 at 17:16):

to be sure, you’re complaining about the industry standard in general, right?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 17:16):

a few times

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Oct 29 2021 at 17:18):

also “industry standard” per se doesn’t make something a good idea by itself.

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Oct 29 2021 at 17:19):

I completely agree that, without CI, developers are prone to ignore warning.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 29 2021 at 21:48):

Sorry, I have to difer here, that's a terrible [and wasteful] experience.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 29 2021 at 22:50):

just to be sure.

view this post on Zulip Paolo Giarrusso (Oct 29 2021 at 22:51):

the “terrible experience” would be getting all the same information, but as warnings not errors?

view this post on Zulip Paolo Giarrusso (Oct 29 2021 at 22:52):

clearly, there must be some missing information, and I’d like to dig deeper.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 29 2021 at 22:55):

so, back to development setup.

view this post on Zulip Paolo Giarrusso (Oct 29 2021 at 22:56):

actually, one more point on users: -warn-error also increases chances of bitrot.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 29 2021 at 23:10):

I mean I've mentioned the drawback of having a different dev vs ci setup

view this post on Zulip Paolo Giarrusso (Oct 29 2021 at 23:10):

a few times

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 30 2021 at 09:28):

Thanks for pointing out (some of) the missing facts to enable discussion progress :-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 02 2021 at 09:10):

this costs a lot of money in the meidum term

view this post on Zulip Emilio Jesús Gallego Arias (Nov 02 2021 at 09:10):

so hence the default

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 02 2021 at 09:10):

like running make twice, etc...

view this post on Zulip Emilio Jesús Gallego Arias (Nov 02 2021 at 09:11):

even when that stuff is run automatically they complain, for example linters

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 02 2021 at 09:13):

any setup that involves people tweaking stuff for CI

view this post on Zulip Emilio Jesús Gallego Arias (Nov 02 2021 at 09:13):

is IMHO doomed to failure

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 02 2021 at 09:14):

policy modifications go to dh_coq itself

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 02 2021 at 09:15):

dune does a bit better, but not perfect

view this post on Zulip 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?

view this post on Zulip 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]

view this post on Zulip 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)?

view this post on Zulip Paolo Giarrusso (Nov 02 2021 at 10:46):

@Karl Palmskog agree on keeping that separate — native_compute discussions are bigger than this one

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Dec 06 2021 at 12:51):

Was any solution found? Equations just failed installation on 4.13.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Dec 06 2021 at 12:52):

did you recompile Coq after doing opam update?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Dec 06 2021 at 12:55):

oh we agreed on that :-)

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Dec 06 2021 at 12:58):

Thanks but let me save you time — I found the patch

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Dec 06 2021 at 13:00):

to my knowledge, 4.14 will be the last 4.X release.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Dec 06 2021 at 13:02):

That's good enough to close the topic for me :-).

view this post on Zulip Karl Palmskog (Dec 06 2021 at 13:03):

https://discuss.ocaml.org/t/the-road-to-ocaml-5-0/8584

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Paolo Giarrusso (Dec 06 2021 at 13:29):

Namely https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/PSA.3A.20ARM.20OCaml.20.3C4.2E13.20reports.20stack.20overflows.20as.20SIGSEGV/near/263849175.


Last updated: Feb 01 2023 at 13:03 UTC