On Fri, Mar 27, 2020 at 11:15:01AM -0600, Jerry James wrote:
On Fri, Mar 27, 2020 at 11:03 AM Jerry James
<loganjerry(a)gmail.com> wrote:
> Okay, I will give that a try.
Except I can't. We're already not using %_smp_mflags. Ugh.
I realized that my build machine has MAKEFLAGS=-j24 which is why it's
building coq in parallel (and quickly). So it seems like you could be
using _smp_mflags.
Another thing I tried today was enabling debugging in the GC (see
patch below). However it also didn't find any problems, so I'm still
at a loss.
Rich.
diff --git a/coq.spec b/coq.spec
index df2a847..1e590cc 100644
--- a/coq.spec
+++ b/coq.spec
@@ -164,6 +164,10 @@ done
%global opt_option -bytecode-compiler yes -byte-only -coqide byte
%endif
+# Use debug runtime.
+sed -i 's/^\(OCAMLC :=.*\)/\1 -runtime-variant d/' Makefile.build
+sed -i 's/^\(OCAMLOPT :=.*\)/\1 -runtime-variant d/' Makefile.build
+
%global coqdocdir %{?_pkgdocdir}%{!?_pkgdocdir:%{_docdir}/coq-%{version}}
%global coqdatadir %{_libdir}/coq
--
Richard Jones, Virtualization Group, Red Hat
http://people.redhat.com/~rjones
Read my programming and virtualization blog:
http://rwmj.wordpress.com
virt-top is 'top' for virtual machines. Tiny program with many
powerful monitoring features, net stats, disk stats, logging, etc.
http://people.redhat.com/~rjones/virt-top