Gentoo Websites Logo
Go to: Gentoo Home Documentation Forums Lists Bugs Planet Store Wiki Get Gentoo!
Bug 750251 - 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
Summary: sci-mathematics/coq-8.6.1-r1 - File "lib/pp_control.ml", line 61, characters ...
Status: UNCONFIRMED
Alias: None
Product: Gentoo Linux
Classification: Unclassified
Component: Current packages (show other bugs)
Hardware: PPC Linux
: Normal normal (vote)
Assignee: Gentoo Science Mathematics related packages
URL:
Whiteboard:
Keywords:
Depends on:
Blocks: 750956
  Show dependency tree
 
Reported: 2020-10-19 20:17 UTC by ernsteiswuerfel
Modified: 2020-10-24 01:47 UTC (History)
1 user (show)

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


Attachments
build.log (coq-8.6.1-r1:20201019-191754.log,762.49 KB, text/plain)
2020-10-19 20:17 UTC, ernsteiswuerfel
Details
emerge --info (file_750251.txt,5.96 KB, text/plain)
2020-10-19 20:17 UTC, ernsteiswuerfel
Details
build.log (8.12.0, ppc) (coq-8.12.0:20201019-224954.log,591.88 KB, text/plain)
2020-10-19 22:59 UTC, ernsteiswuerfel
Details

Note You need to log in before you can comment on or make changes to this bug.
Description ernsteiswuerfel 2020-10-19 20:17:31 UTC
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
Comment 1 ernsteiswuerfel 2020-10-19 20:17:50 UTC
Created attachment 667205 [details]
emerge --info
Comment 2 Sam James archtester gentoo-dev Security 2020-10-19 20:19:42 UTC
How about 8.12.0?
Comment 3 ernsteiswuerfel 2020-10-19 22:59:53 UTC
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\")")