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

Invalid generated Coq code when subquery contains predicate #54

Open
duremar opened this issue Oct 13, 2017 · 2 comments
Open

Invalid generated Coq code when subquery contains predicate #54

duremar opened this issue Oct 13, 2017 · 2 comments

Comments

@duremar
Copy link

duremar commented Oct 13, 2017

perhaps something is wrong with processing a predicate with two arguments (b1):
cosette_bug

@stechu stechu closed this as completed in 43cbd27 Oct 13, 2017
@stechu
Copy link
Contributor

stechu commented Oct 13, 2017

Thanks for the bug report! There is a minor mistake in Coq code generation.
@duremar I believe this is fixed through 43cbd27. The web frontend deployment takes about 15 mins to work.

@stechu stechu reopened this Oct 13, 2017
@stechu stechu closed this as completed Oct 13, 2017
@duremar
Copy link
Author

duremar commented Oct 14, 2017

thank you for quick fix
i've found another example of invalid code generation:

schema s(??);
table a(s);
predicate p(s);

query q1
`select * from a x where exists ( select * from a y where p(y) )`;

query q2
`select * from a x`;

verify q1 q2;

it works if where p(y) removed from the program but fails otherwise

@akcheung akcheung reopened this Oct 14, 2017
@duremar duremar changed the title example from pullsubquery.cos doesn't work in web demo Invalid generated Coq code when subquery contains predicate Oct 16, 2017
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

3 participants