The Coq mailing list

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

I am the author of that termux PR.

I was using gnuroot debian until I upgraded to Android Oreo.

https://github.com/corbinlc/GNURootDebian/issues/206

Android runs a mostly Linux kernel. gnuroot runs using proot. proot is a userspace chroot jail. It mostly let's the Linux programs talk to straight to the Android kernel, except it rewrites the file paths in the syscalls so that Linux thinks it can write to /. I think proot uses ptrace to intercept the syscalls.

Linux syscalls have been slowly added over time. So now there are a lot of redundant ones. Android Oreo blocks all the syscalls that bionic (Android's libc) doesn't use. Linux's libc uses those blocked syscalls, and proot doesn't translate them to allowed syscalls.

So I don't see how the GNUroot authors are going to fix it any time soon.

On Oct 16, 2017 7:07 AM, "Abhishek Anand abhishek.anand.iitg-at-gmail.com |coq-club/Example Allow|" <x9q55qc2ot AT sneakemail.com> wrote:

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