The Coq mailing list

["Kyle Stemen" <ncyms8r3x2 AT snkmail.com>]

I have coq 8.6.1 running on my Android phone. So it is possible, but it took a lot of patches to get it running.

I sent out a PR to make it easier to install opam on Android. My plan was to work my way upstream after it was accepted, but I really appreciate that there is someone else wanting this too.

For the problem you just hit, I worked around it by downgrading binutils to version 2.28.

I'll try to remember the major changes I had to make...

The biggest problem is that the coq plugins aren't linked against their dependencies. They rely on the executable resolving the dependencies by dlopening the plugins in the correct order. Android doesn't allow that. On Android it's like RTLD_LOCAL is always passed to dlopen. I worked around it by:

1. Let the plugins get built without linking against the dependencies

2. Look at the list of undefined symbols in each plugin, and find the library that provides them.

3. Add the dependency after the fact with patchelf.

The version of patchelf that comes with termux seems to corrupt libraries, no matter which flags are used. I used the latest build off github, and it worked.

For plugins that aren't part of coq, like ssreflect, I had it just link against all the existing plugins, and let the linker remove the unused libraries.

Windows has a similar issue where the dependencies have to be explicitly linked. Opam uses flexdll there, which seems like even more of a hack than patchelf.

Also android doesn't support rpath. So I linked everything using absolute paths. I used patchelf to switch from the build paths to the installation paths at install time.

I couldn't find a good xwindows server for my phone. So I couldn't use coqide. So I was using coquille since I'm a vim user. I've made some major improvements on my fork:

https://github.com/bluelightning32/coquille

On Oct 16, 2017 3:31 AM, "Nicolas Pelletier nicolas.pelletier3-at-gmail.com |coq-club/Example Allow|" <jz2trd2i3t AT sneakemail.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