Skip to content
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

Can we have -Q . "" in _CoqProject with coqtail? #3

Open
andres-erbsen opened this issue Mar 4, 2020 · 3 comments
Open

Can we have -Q . "" in _CoqProject with coqtail? #3

andres-erbsen opened this issue Mar 4, 2020 · 3 comments

Comments

@andres-erbsen
Copy link
Contributor

ffbe202 broke coqtail; I reverted. The error message is Error: Invalid character '-' at the beginning of identifier "R", I am guessing coqtail fails to parse "" at the end
of the first line.

But #2 seems quite appealing. Can we do better? I don't know. @whonore ? @mdempsky ? (I am also planning to look into it, but it is not on the top of my todo list and will take a while)

@whonore
Copy link

whonore commented Mar 4, 2020

I think this is just a bug in Coqtail's _CoqProject parsing and I should fix it. I don't think it should be hard to do, I'll take a look later today.

@whonore
Copy link

whonore commented Mar 4, 2020

I think this should be fixed now.

@andres-erbsen
Copy link
Contributor Author

Thanks! Works great for me now.

I am thinking I will not re-apply the patch in question, though. This semester's students already have figured out how to work with the psets, and file this change would make it easier for some, it would still force some people to update coqtail, so perhaps best just not to change the setup until next iteration of this class. I will leave this issue open as a reminder / space for potential discussion.

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

No branches or pull requests

2 participants