The Coq mailing list

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

(Thanks Kyle for your response and your work.)

I totally agree that it is much less efficient to use Coq on a phone instead of a regular desktop.

Nevertheless, there are times when a desktop is not an option at all: when waiting in a queue to check in for a flight, or waiting for food in a restaurant when dining alone, or being stuck without a laptop in a talk whose title was deceptive.

On phones with large screens, one can make productive use of Coq.

For example, if one is stuck on a proof, and then stuck waiting for food, they can look up the proof state where there are stuck and perhaps even make small changes so that their thought process has better ideas to chew on when the food finally arrives.

On my phone, I mainly use the console mode of emacs (emacs -nw) with company-coq. 

I usually SSH to my work desktop and open the proof I am stuck on in "emacs -nw".

On phones, it does not make sense to split the screen into several buffers. Disabling the "three-buffer mode" of proof general helps.

It would help to have a "one-buffer mode" in proof general. 

When my phone is in the landscape orientation, it is very unhelpful when proof-general splits my screen vertically to show both the code and the subgoal buffers at once.

In landscape mode, the lower ~half of the screen is already occupied by the keyboard. So there is only a quarter of a phone's width available for each buffer.

SSHing to my work desktop usually suffices for me, except when I am traveling for many days, especially to other countries. Then I do have to install everything, including Coq, on my phone itself, for times when I have no (or high-latency) connectivity.

Apps like GNURoot Debian make it possible to run a full-fledged "linux virtual machine" inside Android, at least until Android 6.1.

IIRC, CoqIDE works properly in GNURoot Debian.

-- Abhishek

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

On Tue, Oct 17, 2017 at 5:16 AM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

Yeah, and how do you use it? Does coqide work well on android?
Multi-touch screens is certainly something we want to try for
human/proof-assistant interactions.

P.

2017-10-17 7:25 GMT+02:00 Daniel Galvez <dt.galvez AT gmail.com>:
> It's been a long time since I've done any serious work in Coq, but curiosity
> brings me out of the depths of lurking on this mailing list.
>
> I'm surprised no one has asked yet: what has motivated more than a few of
> you to want to install coq on android?
>
> Sincerely,
> Daniel
>
> On Mon, Oct 16, 2017 at 9:58 PM, Nicolas Pelletier
> <nicolas.pelletier3 AT gmail.com> wrote:
>>
>> Thank you for these links. I could very well need the kind of patch
>> discussed in the PR, but for Coq. I am not familiar enough with the ARM ABI
>> to know which parts of it are necessary for 64bits; but this is worth
>> investigating further.
>>
>> As for getting OCaml and opam to work, I didn't need anything beyond the
>> termux patches and fixing a few pathes... so 64bits work better than 32bits
>> in this case.
>>
>> Regards,
>>
>> -- Nicolas
>
>
>
>
> --
> Daniel Galvez