search

markokoleznik / agda-writer

A simple GUI for Agda
Other
31 stars 2 forks source link

Error: Only one input allowed #33

Open markokoleznik opened 8 years ago

markokoleznik commented 8 years ago

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 8 years ago

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 8 years ago

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 8 years ago

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.

banacorn commented 8 years ago

Like this: https://github.com/banacorn/agda-mode/wiki/Conversations-between-Agda-&-agda-mode#load

markokoleznik commented 8 years ago

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