The Coq installer is huge (at least on Windows), so is it possible to port Coq to Android phones?
This way, we can prove theorems at our leisure time without having to open the computer.
We can also use it to make a “math game” with the goal of proving theorems.
This looks like interesting!
Coq is already available in a browser (https://jscoq.github.io/) so it should allow making use of it from any tablet.
I don’t think the porting effort to Android would be worth it, but if someone wants to make an (unofficial) port, they are welcome to do so (Coq is free and open source software).
In the past (i.e. when I had an Android device), I installed a Debian
“chroot” inside the Android system. That means you can basically install
any console application from typical GNU/Linux distributions – you use
the Linux kernel from Android + the GNU &al tools from Debian. The
downside of this approach is that you need root access to your device.
Inside this Debian environment, I installed Emacs and OCaml (from the
package manager), opam2 (from the official download site), and compiled
Coq using opam2.
There’s also an alternative without root access requirement, where you
basically install Debian inside an App. E.g., have a look at Termux:
Yes, and Termux has a bunch of packages even without Debian (and it is much more efficient than installing a proot Debian inside). However, there seems some difficulties packaging OCaml: [Package request] Ocaml core · Issue #6201 · termux/termux-packages · GitHub