markokoleznik/agda-writer

Error: Only one input allowed

Opened this issue · 5 comments

markokoleznik commented

Since the version 2.5 Agda uses new package management.

Now, the error is thrown when loading a file:
Error: Only one input file allowed

The easiest way (I think) is to check the Agda version and decide what execution command to perform but that is a rather ugly one. Any suggestions?

@banacorn How did you solve this? Also by "hacking" ? :)

banacorn commented

I do agda -V every time when I'm wiring Agda, and I cache the version number along the way for later use.

Ugly still:
https://github.com/banacorn/agda-mode/blob/master/lib/process.coffee#L29-L45

markokoleznik commented

Thanks @banacorn ! I'll also do in similar way. I'll store the version when user opens up the app or when the path to Agda is changed. I need to dig up the email you've sent me what actions are now used... :)

csetzer commented

The problem is that agda used to oorganise libraries via a variable agda2-include-dirs which can be customized from the emacs options for agda2. The new way is using files *.agda-lib. Because of this agda2-include-dirs should not contain any path (not even ".") If one deletes all paths the problem is solved.

markokoleznik commented

Agrrh, I have to find some time and finally fix that :) Thanks @banacorn (again) for pointing out what's to do 👍

  • ❤️1