Bug 909329 – sci-mathematics/coq-8.17.1 - Error: No rule found for plugins/ltac2/ltac2_plugin.cmxs

• Status: CONFIRMED
• Product: Gentoo Linux

[Description Toralf Förster 2023-06-28 08:46:33 UTC]

      ocamlc ide/coqide/protocol/.protocol.objs/byte/serialize.{cmo,cmt}
File "user-contrib/Ltac2/dune", line 63, characters 0-632:
63 | (rule
64 |  (targets Init.glob Init.vos Init.vo)
65 |  (deps ../../theories/Init/Prelude.vo ../../plugins/ltac2/ltac2_plugin.cmxs)
66 |  (action (run coqc -R ../../theories Coq -boot -R . Ltac2 -I ../../plugins/micromega -I ../../plugins/ltac -I ../../plugins/extraction -I ../../plugins/derive -I ../../plugins/cc -I ../../plugins/btauto -I ../../plugins/syntax -I ../../plugins/ssrmatching -I ../../plugins/ssr -I ../../plugins/rtauto -I ../../plugins/ring -I ../../plugins/nsatz -I ../../plugins/ltac2 -I ../../plugins/funind -I ../../plugins/firstorder -w +default -q -w -deprecated-native-compiler-option -native-compiler off %{dep:Init.v})))
Error: No rule found for plugins/ltac2/ltac2_plugin.cmxs
File "theories/dune", line 2871, characters 1-973:  
2871 |  (rule

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

  This is an unstable amd64 chroot image at a tinderbox (==build bot)
  name: 23.0_systemd-20230627-181510

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

gcc-config -l:
 [1] x86_64-pc-linux-gnu-13 *
clang/llvm (if any):
clang version 16.0.6
Target: x86_64-pc-linux-gnu
Thread model: posix
InstalledDir: /usr/lib/llvm/16/bin
Configuration file: /etc/clang/clang.cfg
/usr/lib/llvm/16
16.0.6
Python 3.11.4
Available Rust versions:
  [1]   rust-1.69.0 *
The following VMs are available for generation-2:
*)	Eclipse Temurin JDK 17.0.7_p7 [openjdk-bin-17]
Available Java Virtual Machines:
  [1]   openjdk-bin-17  system-vm

php cli (if any):
go version go1.20.5 linux/amd64

  HEAD of ::gentoo
commit dbfe862f74d546ad85b8c46036ebb478d034cd85
Author: Repository mirror & CI <[e-mail]>
Date:   Wed Jun 28 08:02:05 2023 +0000

    2023-06-28 08:02:04 UTC

emerge -qpvO sci-mathematics/coq
[ebuild  N    ] sci-mathematics/coq-8.17.1  USE="-debug (-doc) -gui -ocamlopt -test"

[Comment 1 Toralf Förster 2023-06-28 08:46:34 UTC]

Created attachment 864767 [details]
emerge-info.txt

[Comment 2 Toralf Förster 2023-06-28 08:46:35 UTC]

Created attachment 864768 [details]
emerge-history.txt

[Comment 3 Toralf Förster 2023-06-28 08:46:36 UTC]

Created attachment 864769 [details]
environment

[Comment 4 Toralf Förster 2023-06-28 08:46:37 UTC]

Created attachment 864770 [details]
etc.clang.tar.xz

[Comment 5 Toralf Förster 2023-06-28 08:46:38 UTC]

Created attachment 864771 [details]
etc.portage.tar.xz

[Comment 6 Toralf Förster 2023-06-28 08:46:39 UTC]

Created attachment 864772 [details]
sci-mathematics:coq-8.17.1:20230628-083254.log

[Comment 7 Toralf Förster 2023-06-28 08:46:40 UTC]

Created attachment 864773 [details]
temp.tar.xz

[Comment 8 Agostino Sarubbo 2024-11-13 07:59:28 UTC]

*** Bug 936228 has been marked as a duplicate of this bug. ***