Gentoo Websites Logo
Go to: Gentoo Home Documentation Forums Lists Bugs Planet Store Wiki Get Gentoo!
Bug 849638 - sci-mathematics/coq-8.15.2 - Error: No rule found for topbin/coqc_bin.exe
Summary: sci-mathematics/coq-8.15.2 - Error: No rule found for topbin/coqc_bin.exe
Status: RESOLVED FIXED
Alias: None
Product: Gentoo Linux
Classification: Unclassified
Component: Current packages (show other bugs)
Hardware: All Linux
: Normal normal (vote)
Assignee: Gentoo Science Mathematics related packages
URL:
Whiteboard:
Keywords:
Depends on:
Blocks:
 
Reported: 2022-06-04 07:15 UTC by Toralf Förster
Modified: 2023-09-09 13:26 UTC (History)
0 users

See Also:
Package list:
Runtime testing required: ---


Attachments
emerge-info.txt (emerge-info.txt,19.60 KB, text/plain)
2022-06-04 07:15 UTC, Toralf Förster
Details
emerge-history.txt.bz2 (emerge-history.txt.bz2,67.99 KB, application/x-bzip)
2022-06-04 07:15 UTC, Toralf Förster
Details
environment (environment,38.88 KB, text/plain)
2022-06-04 07:15 UTC, Toralf Förster
Details
etc.portage.tar.bz2 (etc.portage.tar.bz2,23.99 KB, application/x-bzip)
2022-06-04 07:15 UTC, Toralf Förster
Details
sci-mathematics:coq-8.15.2:20220604-011345.log (sci-mathematics:coq-8.15.2:20220604-011345.log,166.92 KB, text/plain)
2022-06-04 07:15 UTC, Toralf Förster
Details
temp.tar.bz2 (temp.tar.bz2,25.07 KB, application/x-bzip)
2022-06-04 07:15 UTC, Toralf Förster
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Toralf Förster gentoo-dev 2022-06-04 07:15:30 UTC
_build/install/default/bin/coqc.byte -coqlib _build_vo/default//lib/coq/ -q   -I _build/default/plugins/btauto -I _build/default/plugins/cc -I _build/default/plugins/derive -I _build/default/plugins/extraction -I _build/default/plugins/firstorder -I _build/default/plugins/funind -I _build/default/plugins/ltac -I _build/default/plugins/ltac2 -I _build/default/plugins/micromega -I _build/default/plugins/nsatz -I _build/default/plugins/ring -I _build/default/plugins/rtauto -I _build/default/plugins/ssr -I _build/default/plugins/ssrmatching -I _build/default/plugins/syntax _build_vo/default//lib/coq/theories/Init/Specif.v -o _build_vo/default//lib/coq/theories/Init/Specif.vo -noinit -R _build_vo/default//lib/coq/theories Coq  
File "topbin/dune", line 24, characters 7-15:
24 |  (name coqc_bin)
            ^^^^^^^^
Error: No rule found for topbin/coqc_bin.exe
make[1]: *** [Makefile.common:184: _build/default/coq-core.install] Error 1
make[1]: *** Waiting for unfinished jobs....

  -------------------------------------------------------------------

  This is an unstable amd64 chroot image at a tinderbox (==build bot)
  name: 17.1_hardened-j4-20220531-135334

  -------------------------------------------------------------------

gcc-config -l:
 [1] x86_64-pc-linux-gnu-9.3.1
 [2] x86_64-pc-linux-gnu-10.3.1
 [3] x86_64-pc-linux-gnu-12.1.1 *
clang/llvm (if any):
clang version 14.0.4
Target: x86_64-pc-linux-gnu
Thread model: posix
InstalledDir: /usr/lib/llvm/14/bin
/usr/lib/llvm/14
14.0.4
Python 3.9.13
Available Rust versions:
  [1]   rust-1.61.0 *
The following VMs are available for generation-2:
1)	Eclipse Temurin JDK 11.0.15_p10 [openjdk-bin-11]
*)	Eclipse Temurin JDK 17.0.3_p7 [openjdk-bin-17]
3)	Eclipse Temurin JDK 8.332_p09 [openjdk-bin-8]
Available Java Virtual Machines:
  [1]   openjdk-bin-8 
  [2]   openjdk-bin-11 
  [3]   openjdk-bin-17  system-vm

The Glorious Glasgow Haskell Compilation System, version 8.10.4
php cli:

  HEAD of ::gentoo
commit e3590f1248c73b0bb7a8e453e454daeed5c84ff4
Author: Repository mirror & CI <repomirrorci@gentoo.org>
Date:   Sat Jun 4 00:18:11 2022 +0000

    2022-06-04 00:18:10 UTC

emerge -qpvO sci-mathematics/coq
[ebuild  N    ] sci-mathematics/coq-8.15.2  USE="-debug (-doc) -gtk -ocamlopt"
Comment 1 Toralf Förster gentoo-dev 2022-06-04 07:15:32 UTC
Created attachment 782690 [details]
emerge-info.txt
Comment 2 Toralf Förster gentoo-dev 2022-06-04 07:15:33 UTC
Created attachment 782693 [details]
emerge-history.txt.bz2
Comment 3 Toralf Förster gentoo-dev 2022-06-04 07:15:34 UTC
Created attachment 782696 [details]
environment
Comment 4 Toralf Förster gentoo-dev 2022-06-04 07:15:35 UTC
Created attachment 782699 [details]
etc.portage.tar.bz2
Comment 5 Toralf Förster gentoo-dev 2022-06-04 07:15:37 UTC
Created attachment 782702 [details]
sci-mathematics:coq-8.15.2:20220604-011345.log
Comment 6 Toralf Förster gentoo-dev 2022-06-04 07:15:38 UTC
Created attachment 782705 [details]
temp.tar.bz2
Comment 7 Maciej Barć gentoo-dev 2023-09-09 13:26:52 UTC
The version 8.15.2 of sci-mathematics/coq is gone from the ::gentoo tree.