[Agda] --jobs?

Mateusz Kowalczyk fuuzetsu at fuuzetsu.co.uk
Mon Aug 25 12:36:43 CEST 2014


On 08/25/2014 09:37 AM, Andreas Abel wrote:
> I think the first step towards this would be to implement a stand-alone 
> import chaser.  Currently new agda files are processed right when the 
> scope checker hits an import statement.  A separate phase for import 
> resolution, yielding a dependency graph, would allow both simultaneous 
> processing of agda files (when --jobs) and progress reports like ghc does.
> 
> It would be nice if you could work on this.
> 
> Cheers,
> Andreas

OK, so it's just that no one got around to it rather than there being a
deeper meaning. I will consider doing this in near-ish future.

> On 25.08.2014 05:15, Mateusz Kowalczyk wrote:
>> Hi,
>>
>> I was running Agda over the categories library and watching htop and
>> noticed that Agda only uses a single core throughout: the whole run
>> looks like it does at [1].
>>
>> I didn't see a --jobs or anything of the sort in --help. Is there any
>> real challenge of making Agda take advantage of multiple cores?
>> Considering it's written in Haskell it seems like it would be fairly
>> easy to do so. Of course it's hard to do so well but at least some
>> should be easy.
>>
>> [1]: http://fuuzetsu.co.uk/images/1408936268.png
>>
> 
> 


-- 
Mateusz K.


More information about the Agda mailing list