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

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:	RESOLVED OBSOLETE

Alias:	None

Product:	Gentoo Linux
Classification:	Unclassified
Component:	Current packages (show other bugs)
Hardware:	All Linux

Importance:	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:	2022-11-26 00:08 UTC (History)
CC List:	2 users (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
View All Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.

Description ernsteiswuerfel archtester

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 archtester

2020-10-19 20:17:50 UTC

Created attachment 667205 [details]
emerge --info

Comment 2 Sam James archtester

2020-10-19 20:19:42 UTC

How about 8.12.0?

Comment 3 ernsteiswuerfel archtester

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\")")

Comment 4 currentcurrant 2021-01-24 00:22:33 UTC

I am having the exact same bug trying to install coq-8.6.1-r1 on AMD64.

Comment 5 Maciej Barć gentoo-dev

2022-11-26 00:08:36 UTC

Closing because sci-mathematics/coq-8.6.1 is gone from the ::gentoo tree.