The Coq mailing list

[Damien Pous <Damien.Pous AT ens-lyon.fr>]

Hi,

Did some of you manage to build and use dynamically linked plugins in
native mode, on a ppc architecture ?

It works for me on Intel, either bytecode or native code ; on PPC it
works only with bytecode : with native code, I get errors about
absolute addressing, text relocs, and slidable images when I try to
compile the plugin (see below). I tried several combinations of -cc
"ld_classic -read_only_relocs suppress" ... without success.
(According to 
http://developer.apple.com/mac/library/releasenotes/DeveloperTools/RN-Id/index.html
, there is no support for text relocs in xcode 3.1 -- I don't know
what is a text reloc...)

The only solutions I have at the moment are either to build and use a
static toplevel (more details below) or use bytecode (way too slow).

Damien


Here are the details:

I'am running Mac OS X Leopard on a PPC and an Intel,
Xcode 3.1.3, ocaml 3.11.2, coq 8.2 -r 12786 on both

I want to compile the attached files :
- a.ml is the plugin, it defines a trivial empty tactic (thanks to
Matthieu and Thomas for the file it comes from !)
- A.v is the coq interface, it declares the ML module a, and uses the tactic
I run "coq_makefile a.ml A.v" to get a Makefile ; then "make byte" and
"make clean opt" work perfectly on Intel, while "make" fails on PPC,
when it tries to build a.cmxs :

ld: absolute addressing (perhaps -mdynamic-no-pic) used in
_camlA__fun_652 from a.o not allowed in slidable image. Use
'-read_only_relocs suppress' to enable text relocs
collect2: ld returned 1 exit status
File "caml_startup", line 1, characters 0-1:
Error: Error during linking
make: *** [a.cmxs] Error 2

since file a.cmo was nonetheless successfully compiled, the following
command works : "coqc -byte A.v" . Of course, "coqc -opt A.v" does not
(a.cmxs not found).


For the non-experts in the same situation, here is how I managed to
build and use a coq top-level :

1. build a .cmxa by replacing -shared with -a  :

ocamlopt -rectypes -a -I /Users/damien/coq/v8.2/kernel -I
/Users/damien/coq/v8.2/lib -I /Users/damien/coq/v8.2/library -I
/Users/damien/coq/v8.2/parsing -I /Users/damien/coq/v8.2/pretyping -I
/Users/damien/coq/v8.2/interp -I /Users/damien/coq/v8.2/proofs -I
/Users/damien/coq/v8.2/tactics -I /Users/damien/coq/v8.2/toplevel -pp
""camlp5"o -I /Users/damien/coq/v8.2/kernel -I
/Users/damien/coq/v8.2/lib -I /Users/damien/coq/v8.2/library -I
/Users/damien/coq/v8.2/parsing -I /Users/damien/coq/v8.2/pretyping -I
/Users/damien/coq/v8.2/interp -I /Users/damien/coq/v8.2/proofs -I
/Users/damien/coq/v8.2/tactics -I /Users/damien/coq/v8.2/toplevel
pa_extend.cmo pa_macro.cmo q_MLast.cmo grammar.cma -impl"  a.ml -o
a.cmxa

2. build the toplevel as follows :

coqmktop -opt -o coco a.cmxa

3. use it to compile other .v files :

coqc -image ./coco A.v

Attachment: a.ml
Description: Binary data

Attachment: A.v
Description: Binary data