| Summary: | sci-mathematics/coq-8.17.1 - Error: No rule found for plugins/ltac2/ltac2_plugin.cmxs | ||
|---|---|---|---|
| Product: | Gentoo Linux | Reporter: | Toralf Förster <toralf> |
| Component: | Current packages | Assignee: | Gentoo Science Mathematics related packages <sci-mathematics> |
| Status: | CONFIRMED --- | ||
| Severity: | normal | ||
| Priority: | Normal | ||
| Version: | unspecified | ||
| Hardware: | All | ||
| OS: | Linux | ||
| Whiteboard: | |||
| Package list: | Runtime testing required: | --- | |
| Attachments: |
emerge-info.txt
emerge-history.txt environment etc.clang.tar.xz etc.portage.tar.xz sci-mathematics:coq-8.17.1:20230628-083254.log temp.tar.xz |
||
Created attachment 864767 [details]
emerge-info.txt
Created attachment 864768 [details]
emerge-history.txt
Created attachment 864769 [details]
environment
Created attachment 864770 [details]
etc.clang.tar.xz
Created attachment 864771 [details]
etc.portage.tar.xz
Created attachment 864772 [details]
sci-mathematics:coq-8.17.1:20230628-083254.log
Created attachment 864773 [details]
temp.tar.xz
*** Bug 936228 has been marked as a duplicate of this bug. *** |
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 <repomirrorci@gentoo.org> 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"