* Package:    sci-mathematics/gappalib-coq-1.5.3:0
 * Repository: gentoo
 * Maintainer: sci-mathematics@gentoo.org
 * Upstream:   https://gitlab.inria.fr/gappa/coq/-/issues/
 * USE:        abi_x86_64 amd64 elibc_glibc kernel_linux
 * FEATURES:   network-sandbox preserve-libs sandbox userpriv usersandbox

>>> Unpacking source...
>>> Unpacking gappalib-coq-1.5.3.tar.gz to /var/tmp/portage/sci-mathematics/gappalib-coq-1.5.3/work
>>> Source unpacked in /var/tmp/portage/sci-mathematics/gappalib-coq-1.5.3/work
>>> Preparing source in /var/tmp/portage/sci-mathematics/gappalib-coq-1.5.3/work/gappalib-coq-1.5.3 ...
>>> Source prepared.
>>> Configuring source in /var/tmp/portage/sci-mathematics/gappalib-coq-1.5.3/work/gappalib-coq-1.5.3 ...
./configure --prefix=/usr --build=x86_64-pc-linux-gnu --host=x86_64-pc-linux-gnu --mandir=/usr/share/man --infodir=/usr/share/info --datadir=/usr/share --sysconfdir=/etc --localstatedir=/var/lib --libdir=/usr/lib64
checking for x86_64-pc-linux-gnu-gcc... x86_64-pc-linux-gnu-gcc
checking whether the C compiler works... yes
checking for C compiler default output file name... a.out
checking for suffix of executables... 
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether the compiler supports GNU C... yes
checking whether x86_64-pc-linux-gnu-gcc accepts -g... yes
checking for x86_64-pc-linux-gnu-gcc option to enable C11 features... none needed
checking how to run the C preprocessor... x86_64-pc-linux-gnu-gcc -E
checking for coqc >= 8.8... /usr/bin/coqc
checking for coqdep... /usr/bin/coqdep
checking for ocamlfind... /usr/bin/ocamlfind
checking for Flocq >= 3.0... yes
checking for native development files... yes
checking for bytecode development files... yes
checking for x86_64-pc-linux-gnu-g++... x86_64-pc-linux-gnu-g++
checking whether the compiler supports GNU C++... yes
checking whether x86_64-pc-linux-gnu-g++ accepts -g... yes
checking for x86_64-pc-linux-gnu-g++ option to enable C++11 features... none needed
configure: building remake...
/usr/lib/gcc/x86_64-pc-linux-gnu/15/../../../../x86_64-pc-linux-gnu/bin/ld: /var/tmp/portage/sci-mathematics/gappalib-coq-1.5.3/temp/ccqrPHHK.o: in function `main':
remake.cpp:(.text.startup+0xfd9): warning: the use of `tempnam' is dangerous, better use `mkstemp'

=== Summary ===
Vernacular directory    /usr/lib64/coq/user-contrib
Plugin directory        /usr/lib64/ocaml/coq-gappa
Plugin compilation      native bytecode

configure: creating ./config.status
config.status: creating Remakefile
>>> Source configured.
>>> Compiling source in /var/tmp/portage/sci-mathematics/gappalib-coq-1.5.3/work/gappalib-coq-1.5.3 ...
Building src/Gappa_common.vo
Building src/Gappa_decimal.vo
Building src/Gappa_definitions.vo
Building src/Gappa_dyadic.vo
Building src/Gappa_fixed.vo
Building src/Gappa_real.vo
Building src/Gappa_float.vo
Building src/Gappa_pred_bnd.vo
Building src/Gappa_round.vo
Building src/Gappa_round_aux.vo
Building src/Gappa_round_def.vo
Building src/Gappa_library.vo
Building src/Gappa_pred_abs.vo
Building src/Gappa_pred_nzr.vo
Building src/Gappa_pred_fixflt.vo
Building src/Gappa_pred_rel.vo
File "./src/Gappa_real.v", line 338, characters 6-14:
Warning: Notation Rle_Rinv is deprecated since 8.19. Use Rinv_le_contravar.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_real.v", line 338, characters 6-14:
Warning: Notation Rle_Rinv is deprecated since 8.19. Use Rinv_le_contravar.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_real.v", line 349, characters 15-31:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_real.v", line 349, characters 15-31:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_real.v", line 349, characters 15-31:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_real.v", line 349, characters 15-31:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_real.v", line 349, characters 15-31:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_real.v", line 349, characters 15-31:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_real.v", line 349, characters 15-31:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_real.v", line 349, characters 15-31:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_real.v", line 349, characters 15-31:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_real.v", line 349, characters 15-31:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
Building src/Gappa_rewriting.vo
Finished src/Gappa_definitions.vo
Building src/Gappa_tree.vo
Building src/Gappa_user.vo
Building src/Gappa_obfuscate.vo
Finished src/Gappa_round_def.vo
Building src/Gappa_tactic_loader.v
Finished src/Gappa_tactic_loader.v
Building src/Gappa_tactic.vo
Finished src/Gappa_obfuscate.vo
Building src/gappatac.ml
Finished src/gappatac.ml
Building src/gappatac.cmxs
Building src/gappatac.cmo
File "src/gappatac.c", line 35, characters 17-35:
Error: Unbound value Tactics.generalize
Failed to build src/gappatac.cmo
Failed to build src/Gappa_tactic_loader.vo
Failed to build all
Finished src/Gappa_real.vo
Failed to build src/Gappa_tactic.vo
File "src/gappatac.c", line 35, characters 17-35:
Error: Unbound value Tactics.generalize
Failed to build src/gappatac.cmxs
Finished src/Gappa_dyadic.vo
Finished src/Gappa_common.vo
Finished src/Gappa_round_aux.vo
Finished src/Gappa_pred_nzr.vo
File "./src/Gappa_pred_fixflt.v", line 323, characters 11-18:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_pred_fixflt.v", line 323, characters 11-18:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_pred_fixflt.v", line 323, characters 0-23:
Error:
In environment
x : R
ml, el : Z
xu : float2
n : Z
p : positive
mx, ex : Z
Hx1 : {| Fnum := mx; Fexp := ex |} = x
Hx2 : (Z.abs (Fnum {| Fnum := mx; Fexp := ex |}) < Z.pow_pos 2 p)%Z
Hxi :
  (lower {| lower := {| Fnum := ml; Fexp := el |}; upper := xu |} <= Rabs x)%R
H2 : (0 < {| Fnum := ml; Fexp := el |})%R
H0 : (0 < ml)%Z
H0' : ml <> 0%Z
Hx0 : mx <> 0%Z
e : Z
He :
  IZR mx <> 0%R -> (bpow radix2 (e - 1) <= Rabs (IZR mx) < bpow radix2 e)%R
The term "0" has type "nat" while it is expected to have type "Z".

Failed to build src/Gappa_pred_fixflt.vo
Failed to build src/Gappa_library.vo
File "./src/Gappa_pred_abs.v", line 269, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_pred_abs.v", line 269, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_pred_abs.v", line 269, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_pred_abs.v", line 269, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
Finished src/Gappa_rewriting.vo
Finished src/Gappa_pred_abs.vo
Finished src/Gappa_decimal.vo
Finished src/Gappa_round.vo
Finished src/Gappa_pred_bnd.vo
Finished src/Gappa_tree.vo
Finished src/Gappa_user.vo
File "./src/Gappa_float.v", line 304, characters 16-23:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_float.v", line 304, characters 16-23:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_float.v", line 352, characters 16-23:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Gappa_float.v", line 352, characters 16-23:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
Finished src/Gappa_pred_rel.vo
Finished src/Gappa_fixed.vo
Finished src/Gappa_float.vo
 * ERROR: sci-mathematics/gappalib-coq-1.5.3::gentoo failed (compile phase):
 *   (no error message)
 * 
 * Call stack:
 *     ebuild.sh, line 136:  Called src_compile
 *   environment, line 328:  Called die
 * The specific snippet of code:
 *       ./remake --jobs=$(makeopts_jobs) || die
 * 
 * If you need support, post the output of `emerge --info '=sci-mathematics/gappalib-coq-1.5.3::gentoo'`,
 * the complete build log and the output of `emerge -pqv '=sci-mathematics/gappalib-coq-1.5.3::gentoo'`.
 * The complete build log is located at '/var/log/portage/sci-mathematics:gappalib-coq-1.5.3:20250302-193849.log'.
 * For convenience, a symlink to the build log is located at '/var/tmp/portage/sci-mathematics/gappalib-coq-1.5.3/temp/build.log'.
 * The ebuild environment file is located at '/var/tmp/portage/sci-mathematics/gappalib-coq-1.5.3/temp/environment'.
 * Working directory: '/var/tmp/portage/sci-mathematics/gappalib-coq-1.5.3/work/gappalib-coq-1.5.3'
 * S: '/var/tmp/portage/sci-mathematics/gappalib-coq-1.5.3/work/gappalib-coq-1.5.3'