The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

On my phone (note 4, model SM-N910C), I have had success with GNURoot Debian:

https://play.google.com/store/apps/details?id=com.gnuroot.debian

IIRC, "sudo apt install coq" worked perfectly.

I do prefer termux over GNURoot Debian because termux is much more lightweight and integrates much better with the rest of Android. 

I have also tried to install coq in termux, but I never got past your step 2, perhaps because my phone's architecture is not arch64.

I have been monitoring the following PR, but I don't understand the discussion:

https://github.com/termux/termux-packages/pull/1343

--Abhishek
http://www.cs.cornell.edu/~aa755/

On Oct 16, 2017 6:31 AM, "Nicolas Pelletier" <nicolas.pelletier3 AT gmail.com> wrote:

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