Gentoo Websites Logo
Go to: Gentoo Home Documentation Forums Lists Bugs Planet Store Wiki Get Gentoo!
Bug 889278 - sci-mathematics/coq-8.12.0-r2 - make inconsistent assumptions over interface Coqpp_parse
Summary: sci-mathematics/coq-8.12.0-r2 - make inconsistent assumptions over interface ...
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: 2023-01-01 14:59 UTC by Toralf Förster
Modified: 2023-09-09 18:14 UTC (History)
0 users

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


Attachments
emerge-info.txt (emerge-info.txt,19.09 KB, text/plain)
2023-01-01 14:59 UTC, Toralf Förster
Details
emerge-history.txt.bz2 (emerge-history.txt.bz2,66.85 KB, application/x-bzip)
2023-01-01 14:59 UTC, Toralf Förster
Details
environment (environment,71.07 KB, text/plain)
2023-01-01 14:59 UTC, Toralf Förster
Details
etc.clang.tar.bz2 (etc.clang.tar.bz2,581 bytes, application/x-bzip)
2023-01-01 14:59 UTC, Toralf Förster
Details
etc.portage.tar.bz2 (etc.portage.tar.bz2,30.48 KB, application/x-bzip)
2023-01-01 14:59 UTC, Toralf Förster
Details
sci-mathematics:coq-8.12.0-r2:20230101-143733.log.bz2 (sci-mathematics:coq-8.12.0-r2:20230101-143733.log.bz2,17.89 KB, application/x-bzip)
2023-01-01 14:59 UTC, Toralf Förster
Details
temp.tar.bz2 (temp.tar.bz2,35.56 KB, application/x-bzip)
2023-01-01 14:59 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 2023-01-01 14:59:42 UTC
too long lines were shrinked:

Warning 70 [missing-mli]: Cannot find interface file.
"/usr/bin/ocamlfind" ocamlc -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67   -safe-string -strict-sequence  -I coqpp coqpp/coqpp_parse.cmo coqpp/coqpp_lex.cmo coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml coqpp/coqpp_main.ml -linkall -o bin/coqpp
File "coqpp/coqpp_main.ml", line 1:
Warning 70 [missing-mli]: Cannot find interface file.
File "coqpp/coqpp_main.ml", line 1:
Error: Files coqpp/coqpp_lex.cmo and coqpp/coqpp_parse.cmo
       make inconsistent assumptions over interface Coqpp_parse
"/usr/bin/ocamlfind" ocamlc -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67   -safe-string -strict-sequence    -I coqpp -I config -I clib -I lib -I kernel -I kernel/byterun -I library -I engine -I pretyping -I interp -I proofs -I gramlib/.pack -I parsing -I printing -I tactics -I vernac -I stm -
"/usr/bin/ocamlfind" opt -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67   -safe-string -strict-sequence   -I coqpp -I config -I clib -I lib -I kernel -I kernel/byterun -I library -I engine -I pretyping -I interp -I proofs -I gramlib/.pack -I parsing -I printing -I tactics -I vernac -I stm -I to

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

  This is an unstable amd64 chroot image at a tinderbox (==build bot)
  name: 17.1_no_multilib_hardened-j4-20221229-120038

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

GNUMAKEFLAGS="$GNUMAKEFLAGS --jobserver-style=pipe"
GNUMAKEFLAGS="$GNUMAKEFLAGS --shuffle"
gcc-config -l:
 [1] x86_64-pc-linux-gnu-12 *
clang/llvm (if any):
clang version 15.0.6
Target: x86_64-pc-linux-gnu
Thread model: posix
InstalledDir: /usr/lib/llvm/15/bin
Configuration file: /etc/clang/clang.cfg
/usr/lib/llvm/15
15.0.6
Python 3.10.9
Available Rust versions:
  [1]   rust-bin-1.66.0 *
The following VMs are available for generation-2:
1)	Eclipse Temurin JDK 11.0.17_p8 [openjdk-bin-11]
*)	Eclipse Temurin JDK 17.0.5_p8 [openjdk-bin-17]
3)	Eclipse Temurin JDK 8.352_p08 [openjdk-bin-8]
4)	Eclipse Temurin JRE 17.0.5_p8 [openjdk-jre-bin-17]
Available Java Virtual Machines:
  [1]   openjdk-bin-8 
  [2]   openjdk-bin-11 
  [3]   openjdk-bin-17  system-vm
  [4]   openjdk-jre-bin-17 

php cli (if any):
  [1]   php8.2 *

  HEAD of ::gentoo
commit 20f22f6c7323dcc2f101208666b8414f29bbbb8e
Author: Repository mirror & CI <repomirrorci@gentoo.org>
Date:   Sun Jan 1 14:02:13 2023 +0000

    Merge updates from master

emerge -qpvO sci-mathematics/coq
[ebuild  N    ] sci-mathematics/coq-8.16.1  USE="ocamlopt -debug (-doc) -gtk"
Comment 1 Toralf Förster gentoo-dev 2023-01-01 14:59:43 UTC
Created attachment 846412 [details]
emerge-info.txt
Comment 2 Toralf Förster gentoo-dev 2023-01-01 14:59:45 UTC
Created attachment 846414 [details]
emerge-history.txt.bz2
Comment 3 Toralf Förster gentoo-dev 2023-01-01 14:59:46 UTC
Created attachment 846416 [details]
environment
Comment 4 Toralf Förster gentoo-dev 2023-01-01 14:59:47 UTC
Created attachment 846418 [details]
etc.clang.tar.bz2
Comment 5 Toralf Förster gentoo-dev 2023-01-01 14:59:48 UTC
Created attachment 846420 [details]
etc.portage.tar.bz2
Comment 6 Toralf Förster gentoo-dev 2023-01-01 14:59:49 UTC
Created attachment 846422 [details]
sci-mathematics:coq-8.12.0-r2:20230101-143733.log.bz2
Comment 7 Toralf Förster gentoo-dev 2023-01-01 14:59:50 UTC
Created attachment 846424 [details]
temp.tar.bz2
Comment 8 Larry the Git Cow gentoo-dev 2023-09-09 18:14:03 UTC
The bug has been closed via the following commit(s):

https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=2f2d44de2a3172289669f4f28daa46a7d8f76de5

commit 2f2d44de2a3172289669f4f28daa46a7d8f76de5
Author:     Maciej Barć <xgqt@gentoo.org>
AuthorDate: 2023-09-09 13:17:40 +0000
Commit:     Maciej Barć <xgqt@gentoo.org>
CommitDate: 2023-09-09 18:13:59 +0000

    sci-mathematics/coq: drop old 8.12.0-r2
    
    Closes: https://bugs.gentoo.org/888964
    Closes: https://bugs.gentoo.org/889278
    Signed-off-by: Maciej Barć <xgqt@gentoo.org>

 sci-mathematics/coq/Manifest             |  1 -
 sci-mathematics/coq/coq-8.12.0-r2.ebuild | 90 --------------------------------
 2 files changed, 91 deletions(-)