| Summary: | sci-mathematics/coq-8.6.1-r1 - File "lib/pp_control.ml", line 61, characters 22-33: 61 | let ft = with_fp ch (output ch) (fun () -> flush ch) in Error: This expression has type bytes -> int -> int -> unit | ||
|---|---|---|---|
| Product: | Gentoo Linux | Reporter: | ernsteiswuerfel <erhard_f> |
| Component: | Current packages | Assignee: | Gentoo Science Mathematics related packages <sci-mathematics> |
| Status: | RESOLVED OBSOLETE | ||
| Severity: | normal | CC: | kingjon3377, sam |
| Priority: | Normal | ||
| Version: | unspecified | ||
| Hardware: | All | ||
| OS: | Linux | ||
| Whiteboard: | |||
| Package list: | Runtime testing required: | --- | |
| Bug Depends on: | |||
| Bug Blocks: | 750956 | ||
| Attachments: |
build.log
emerge --info build.log (8.12.0, ppc) |
||
Created attachment 667205 [details]
emerge --info
How about 8.12.0? Created attachment 667223 [details]
build.log (8.12.0, ppc)
With 8.12.0 (which is not keyworded on ppc) I get this build error:
[...]
bin/coqc -coqlib . -q -native-compiler yes theories/Init/Ltac.v -noinit -R theories Coq
File "./theories/Init/Ltac.v", line 11, characters 0-32:
Error:
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/var/tmp/portage/sci-mathematics/coq-8.12.0/work/coq-8.12.0/plugins/ltac/ltac_plugin.cmxs: R_PPC_REL24 relocation at 0xe935e13c for symbol `caml_call_gc' out of range\")")
I am having the exact same bug trying to install coq-8.6.1-r1 on AMD64. Closing because sci-mathematics/coq-8.6.1 is gone from the ::gentoo tree. |
Created attachment 667202 [details] build.log [...] "/usr/bin/ocamlfind" opt -rectypes -w -3-52-56 -I config -I lib -I kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I interp -I stm -I toplevel -I parsing -I printing -I intf -I engine -I ltac -I tools -I tools/coqdoc -I plugins/omega -I plugins/romega -I plugins/micromega -I plugins/quote -I plugins/setoid_ring -I plugins/extraction -I plugins/fourier -I plugins/cc -I plugins/funind -I plugins/firstorder -I plugins/derive -I plugins/rtauto -I plugins/nsatz -I plugins/syntax -I plugins/decl_mode -I plugins/btauto -I plugins/ssrmatching -I plugins/ltac -I "+camlp4" -thread -c lib/pp_control.ml File "lib/pp_control.ml", line 61, characters 22-33: 61 | let ft = with_fp ch (output ch) (fun () -> flush ch) in ^^^^^^^^^^^ Error: This expression has type bytes -> int -> int -> unit but an expression was expected of type string -> int -> int -> unit Type bytes is not compatible with type string make[1]: *** [Makefile.build:580: lib/pp_control.cmx] Error 2 make[1]: Leaving directory '/var/tmp/portage/sci-mathematics/coq-8.6.1-r1/work/coq-8.6.1' make: *** [Makefile:154: submake] Error 2