coq 8.14.1

[tchajed]

Created with brew bump-formula-pr.

[tchajed]

The error is an audit failure "Libraries were compiled with a flat namespace" in all the cmxs files.

I don't really understand how to fix this, or what might have changed. It does seem OCaml passes this flag: https://github.com/ocaml/ocaml/blob/3fa2cfce074d0a83225d7a21678b971bad959a7f/configure.ac#L954.

[tchajed]

I confirmed that the same error now appears when auditing coq 8.13.2 and 8.14.0, which is a relief since I wouldn't expect anything to have changed upstream.

[carlocab]

It does seem OCaml passes this flag: https://github.com/ocaml/ocaml/blob/3fa2cfce074d0a83225d7a21678b971bad959a7f/configure.ac#L954.

Yep. It shouldn't, though: ocaml/ocaml#10723

We've patched this in Homebrew OCaml:

homebrew-core/Formula/ocaml.rb

Lines 40 to 49 in ccd98dd

	# Remove use of -flat_namespace. Upstreamed at
	# https://github.com/ocaml/ocaml/pull/10723
	# We embed a patch here so we don't have to regenerate configure.
	patch :p0, :DATA
	# Fix -flat_namespace being used on Big Sur and later.
	patch do
	url "https://raw.githubusercontent.com/Homebrew/formula-patches/03cf8088210822aa2c1ab544ed58ea04c897d9c4/libtool/configure-big_sur.diff"
	sha256 "35acd6aebc19843f1a2b3a63e880baceb0f5278ab1ace661e57a502d9d78c93c"
	end

[carlocab]

The -flat_namespace flag comes from OCaml, so should be fixed there. I think we can ignore the audit for now, since it should be fixed when OCaml is updated.

[BrewTestBot]

@carlocab has triggered a merge.