[Agda] Typechecking with multiple concurrent agda processes.

[Apostolis Xekoukoulotakis]

Now, with caching enabled and some small changes to the files typechecked,
I get this :

```
real 7m5.636s
user 18m29.676s
sys 0m15.526s
```

with 4 processes.

With a single agda process, I get :

```
real 14m20.085s
user 14m15.585s
sys 0m3.967s
```



On Wed, Aug 23, 2017 at 12:24 PM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> 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/1001e4ed/attachment.html>