The Coq mailing list

[Nicolas Pelletier <nicolas.pelletier3 AT gmail.com>]

Hello Coq users,

I am trying to get Coq to run on my tablet (Android 7.1.1 on arm aarch64), and running into some difficulties. Here is what I did so far:

  1. installed termux from the Google store. The more advanced Linux solutions (such as Debian-noroot failed to boot)

  2. installed OCaml 4.04 + termux patches following the instsructions at http://ygrek.org.ua/p/ocaml-termux.html

  3. installed findlib with the opam from step 2

  4. installed camlp5 from source, as there is no termux package for it

  5. trying to compile Coq 8.7-beta2 from source, I get the following error many times at link time:

/data/data/com.termux/files/usr/bin/ld: plugins/ltac/ltac_plugin.o: relocation R_AARCH64_ADR_PREL_PG_HI21 against symbol `camlLtac_plugin__G_ltac' which may bind externally can not be used when making a shared object; recompile with -fPIC

I tried adding -fPIC to CFLAGS and -ccopt -fPIC to OCAMLOPT in the Makefiles and scripts defining these and running make again; I got the same errors.

So I am left wondering: is there another file to modify to activate these options? Is the Makefile regenerated at each compilation (overwriting my modifications)? Is PIC compilation impossible for some deeper reason? And if so, is it possible to compile statically to avoid the issue?

Thanks in advance for any help on this matter.

-- Nicolas