Skip to content

With an empty .apia file, we get an error. #66

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jonaprieto opened this issue Aug 28, 2016 · 5 comments
Open

With an empty .apia file, we get an error. #66

jonaprieto opened this issue Aug 28, 2016 · 5 comments

Comments

@jonaprieto
Copy link
Collaborator

jonaprieto commented Aug 28, 2016

Use an empty file or a file with all lines commented in YAML. An error appears.
With:

module NoTheorem where

postulate
  D   : Set
  _≡_ : D  D  Set
  a b : D

postulate foo : a ≡ b
{-# ATP prove foo #-}

Try with an empty .apia:

$ touch .apia
$ apia NoTheorem.agda
apia: UnexpectedEvent {_received = Just EventStreamEnd, _expected = Just EventDocumentStart}
@asr
Copy link
Owner

asr commented Aug 28, 2016

@jonaprieto I assigned you this issue.

@jonaprieto
Copy link
Collaborator Author

Ok. I have something in mind to solve this.

@asr asr assigned asr and unassigned jonaprieto Dec 31, 2016
@asr
Copy link
Owner

asr commented Dec 31, 2016

I'll try to fix this issue.

@jonaprieto
Copy link
Collaborator Author

I was working on this issue in the branch: hotfix/Issue66 but also trying to use parse combinators.
I couldn´t resolve the parsing, but it almost complete the integration.

@asr
Copy link
Owner

asr commented Dec 31, 2016

I see. Which will be next step?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants