Stream: Coq devs & plugin devs

Topic: Warning 8

Jason Gross (Jul 27 2023 at 02:49):

Is there a reason that Warning 8 (this pattern-matching is not exhaustive) isn't fatal by default when building Coq?

Gaëtan Gilbert (Jul 27 2023 at 07:49):

it is fatal in dev mode
in release mode no warning is fatal

Michael Soegtrop (Jul 27 2023 at 08:36):

in release mode no warning is fatal

Is there a good reason for this? I would more expect that in release mode all warnings are fatal.

Gaëtan Gilbert (Jul 27 2023 at 08:37):

it helps to compile on newer ocaml which may have more warnings iirc

Karl Palmskog (Jul 27 2023 at 08:49):

if all warnings are fatal in release mode, doesn't this mean old Coq versions will break as new OCaml compilers introduce new warnings? We've had this problem before. (Of course, the RM could turn it off when tagging)

Michael Soegtrop (Jul 27 2023 at 08:51):

Can't one put an OCaml version dependent make flag into the opam file, so that warnings are fatal for selected OCaml versions?

Théo Zimmermann (Jul 27 2023 at 08:52):

What would be the point of making warnings fatal in release mode? Warnings are for developers.

Gaëtan Gilbert (Jul 27 2023 at 08:59):

if all warnings are fatal in release mode

all warnings are non fatal in release mode

Karl Palmskog (Jul 27 2023 at 09:03):

my reading of what some people said above was to make warnings fatal everywhere. I know that's not the case currently. Just pointing out the drawbacks with that.

Jason Gross (Jul 27 2023 at 21:47):

How do I turn on dev mode?

Gaëtan Gilbert (Jul 27 2023 at 21:52):

it's the default

Jason Gross (Jul 27 2023 at 22:03):

Uh, when I ran

$ ./configure -prefix "$HOME/.local64/coq/coq-master+fma/" -native-compiler yes
Done: 100% (2/2, 0 left) (jobs: 0)You have OCaml 4.11.2. Good!
You have OCamlfind 1.9.6. Good!
You have native-code compilation. Good!
You have the Zarith library 1.12 installed. Good!

  Architecture                : Linux
  Sys.os_type                 : Unix
  OCaml version               : 4.11.2
  OCaml binaries in           : /home/jgross/.opam/4.11.2+fp/bin/
  OCaml library in            : /home/jgross/.opam/4.11.2+fp/lib/ocaml
  Web browser                 : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &
  Coq web site                : http://coq.inria.fr/
  Bytecode VM enabled         : true
  Native Compiler enabled     : yes

  Paths where installation is expected by Coq Makefile:
  - Coq is expected in /home/jgross/.local64/coq/coq-master+fma/
  - the Coq library is expected in /home/jgross/.local64/coq/coq-master+fma//lib/coq
  - the Coqide configuration files is expected in /home/jgross/.local64/coq/coq-master+fma//etc/xdg/coq
  - the Coqide data files is expected in /home/jgross/.local64/coq/coq-master+fma//share/coq
  - the Coq man pages is expected in /home/jgross/.local64/coq/coq-master+fma//share/man
  - documentation prefix path for all Coq packages is expected in /home/jgross/.local64/coq/coq-master+fma//share/doc

If anything is wrong above, please restart './configure'.

*Warning* To compile the system for a new architecture
          don't forget to do a 'make clean' before './configure'.

and then make dunestrap and then dune build -p coq-core,coq-stdlib,coqide-server,coqide -j2 --verbose, it seemed to be treating warning 8 as non-fatal

Jason Gross (Jul 27 2023 at 22:03):

(That is, I saw a file with warning 8 scroll by, and it labeled it as a warning, and it kept building after that)

Gaëtan Gilbert (Jul 27 2023 at 22:08):

build -p is not default, see what the man page says about -p

Emilio Jesús Gallego Arias (Jul 28 2023 at 15:34):

dune build -p implies --release. You can use instead dune build {coq-core,coq-stdlib,coqide-server,coqide}.install -j 2

Emilio Jesús Gallego Arias (Jul 28 2023 at 15:37):

that will build the files in dev profile.

Flags for the release profile can be controlled in the dune file, see:

; Default flags for all Coq libraries and binaries.
(env
 (dev     (flags :standard -w -9-27@60@70 \ -short-paths)
          (coq (flags :standard -w +default)))
 (release (flags :standard)
          (ocamlopt_flags :standard -O3 -unbox-closures))
 (ireport (flags :standard -w -9-27+60-70)
          (ocamlopt_flags :standard -O3 -unbox-closures -inlining-report)))

If we wanted, we could update the release entry to override the current set of :standard flags.

But as noted in the thread, this may not be a good idea. Warnings are useless to users, so it makes no sense IMVHO to expose an error to the user they can't action on.

Note that the meaning of :standard is tied to the (lang dune 2.9) version we use. Newer dune versions use a different set of default flags, but this is properly versioned so we have control over it.

Last updated: Oct 13 2024 at 01:02 UTC