[
https://issues.apache.org/jira/browse/CALCITE-1977?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=17390270#comment-17390270
]
Shuxian Wang commented on CALCITE-1977:
---------------------------------------
Hello all,
I would like to bring some update on the Cosette's part. Currently Cosette is
being re-implemented, which will eventually be consisted with a
[frontend/parser|https://github.com/cosette-solver/cosette-parser], and a
[backend/prover|https://github.com/cosette-solver/cosette-rs]. The end product
will accept a SQL file as input, which contains some CREATE TABLE statements
for specifying schema info, followed by a pair of SQL queries that is intended
to be check for equivalence.
The parser is completely in Java and relies on Cosette's parser and validator
to obtain a RelNode from the SQL. The prover is in Rust, and we have a
intermediate JSON format for parser–prover communication. I think there are two
ways to integrate:
# First is to use the standard way of generating the SQL file, but this might
be too cumbersome as we are unparsing and parsing the queries during the
process.
# A tighter integration is to add a hook somehow in the testing setup, such
that RelNodes of every pair of queries in the test are extracted. Then we can
reuse the code in our parser to translate these RelNodes into the JSON format
that prover will understand.
> Use Cosette to check whether planner rules are valid
> ----------------------------------------------------
>
> Key: CALCITE-1977
> URL: https://issues.apache.org/jira/browse/CALCITE-1977
> Project: Calcite
> Issue Type: Bug
> Reporter: Julian Hyde
> Priority: Major
>
> Use [Cosette|http://cosette.cs.washington.edu/], an automated SQL solver from
> University of Washington, to check whether planner rules are valid.
> I don't know whether Cosette is written in Java, so the simplest approach
> might be to instrument the planner to generate a script. Suppose
> {{FilterProjectTransposeRule}} has just fired successfully. Then
> {{RelOptRuleCall#transformTo}} would generate the line
> {code}
> assertEquivalent(
> "select * from (select empno from emp) where empno > 10",
> "select empno from (select * from emp where empno > 10)")
> {code}
> (Those SQL statements are the result of converting the before and after
> {{RelNode}} instances to SQL.)
> We could run the Calcite test suite to produce a large script with probably
> thousands of those statements. Then the Cosette researchers can take that
> script and run it through Cosette (using whatever language they develop in).
> It would find bugs in Cosette (at first mostly deficiencies in Cosette's SQL
> parser, I fear) but also would find bugs in Calcite if the transformation is
> not valid. (Not too many, I hope!)
--
This message was sent by Atlassian Jira
(v8.3.4#803005)
