[Agda] Typechecking with multiple concurrent agda processes.

[Apostolis Xekoukoulotakis]

My priv. response to ASR :

> https://github.com/HoTT/HoTT-Agda/tree/master/theorems
<https://github.com/HoTT/HoTT-Agda/tree/master/theorems>
>
> You need to put all three indices into a single Everything.agda file.

I think that it would be better if each agda process was kept alive and was
given files to typecheck when available. If I enabled caching, then the
cost of deserialization would be low.
Thus I could call agda with this command :

```
agda --interaction --caching
```

The problem is that I do not know the commands. Is there documentation
somewhere? The only command I need, is to typecheck the next file.

On Tue, Aug 22, 2017 at 4:52 PM, Andrés Sicard-Ramírez <asr at eafit.edu.co>
wrote:

> On 22 August 2017 at 07:58, Apostolis Xekoukoulotakis
> <apostolis.xekoukoulotakis at gmail.com> wrote:
> > It is not efficient in any way. Still with 10 processes, I can reduce the
> > time of compiling everything from HoTT-agda (in the theorem folder) from
> 17
> > min to 10 min.
>
> I couldn't find the theorem folder.
>
> Best,
>
> --
> Andrés
> La información contenida en este correo electrónico está dirigida
> únicamente a su destinatario y puede contener información confidencial,
> material privilegiado o información protegida por derecho de autor. Está
> prohibida cualquier copia, utilización, indebida retención, modificación,
> difusión, distribución o reproducción total o parcial. Si usted recibe este
> mensaje por error, por favor contacte al remitente y elimínelo. La
> información aquí contenida es responsabilidad exclusiva de su remitente por
> lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje
> contenga. The information contained in this email is addressed to its
> recipient only and may contain confidential information, privileged
> material or information protected by copyright. Its prohibited any copy,
> use, improper retention, modification, dissemination, distribution or total
> or partial reproduction. If you receive this message by error, please
> contact the sender and delete it. The information contained herein is the
> sole responsibility of the sender therefore Universidad EAFIT is not
> responsible for what the message contains.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170823/f26a3cc5/attachment.html>