Re: Integrate the Cosette prover in Calcite's RelNode rewrite tests

[Julian Hyde <jh...@gmail.com>]

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 <ws...@berkeley.edu> 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

Re: Integrate the Cosette prover in Calcite's RelNode rewrite tests

[Shuxian Wang <ws...@berkeley.edu>]

Hi Julian,

Thank you very much for looking into our project! Currently Arthur Pan 
<pa...@berkeley.edu> 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 <ws...@berkeley.edu> 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