Hi Julian,
Thank you very much for looking into our project! Currently Arthur Pan
<[email protected]> is the maintainer of cosette-parser, and he is
doing something similar to what you suggest: basically getting the
`relBefore` and `r` in line 124 and 144 of RelOptTestBase.java, and
outputting JSON to the prover. We can automatically extract ~400 cases
for the prover now (the remaining are `checkUnchanged()` cases). The
prover is now pretty much a WIP, so only a few cases are actually
proved, but I am working hard on getting better feature coverage.
Thanks again for your help and input! We’ll report back if we get
problems/progress. :)
Shuxian Wang
On 7 Aug 2021, at 12:08, Julian Hyde wrote:
Shuxian,
It would be great to carry on this integration. I downloaded and built
your project. (I also opened a pull request[1], adding a maven wrapper
and a README.)
It’s difficult to get at the RelNodes in RelOptRulesTest if you’re
outside Calcite. (Because it is a test, we don’t currently include
it in a library.) Therefore I suggest that you create a fork of
Calcite and modify the RelOptTestCase.Sql.checkPlanning method[2] to
call your checker. Of course you’ll have to modify
core/build.gradle.kts and add your checker library as a
testImplementation.
Julian
[1] https://github.com/cosette-solver/cosette-parser/pull/1
[2]
https://github.com/apache/calcite/blob/d46137a197a2840ea5ff9f3b38bb86d423c9af11/core/src/test/java/org/apache/calcite/test/RelOptTestBase.java#L87
On Jul 29, 2021, at 2:26 AM, Shuxian Wang <[email protected]> wrote:
Hello Calcite developers,
I am a Berkeley student working on a new version for the [Cosette SQL
prover](https://cosette.cs.washington.edu/).
This [new
implementation](https://github.com/cosette-solver/cosette-rs) aims
for higher performance and better SQL feature coverage.
One goal for us is to formally check as much rewrite rules in Calcite
as possible, which are those located in
https://github.com/apache/calcite/blob/master/core/src/test/java/org/apache/calcite/test/RelOptRulesTest.java.
The prover initially relies on a custom SQL parser, but we’ve
decided to build a [new
one](https://github.com/cosette-solver/cosette-parser) depending on
Calcite’s parser instead.
This parser takes in SQL and use Calcite to get a corresponding
RelNode.
Later on the parser translates that RelNode into a JSON format that
will be recognized by the prover.
This makes integrating with the Calcite testing component very
feasible, given a way to extract the RelNode before/after each
rewrite test and send them to the prover in JSON.
I writing to ask if there is any general interest in such
integration? If so, some help on extracting the RelNode from the
Calcite test cases would be appreciated.
Sincerely,
Shuxian Wang
