Re: [PATCH 0/5] Conflict Counterexample Generation

[Akim Demaille]

Hi Vincent!

> Le 13 mai 2020 à 13:41, Vincent Imbimbo <address@hidden> a écrit :
> 
> Hey Akim,
> 
> Unfortunately in your latest rebase, we lost all the commit messages, so
>> I'm currently writing them.
> 
> Sorry for the inconvenience. If you're talking about the bug fix commits, a
> lot of them were moving code around, which I thought was kind of ugly to
> have in a repo. Also, after the heavy rebasing, I wasn't sure if scratched
> implementations from earlier versions still worked.

No worries.  I wrote the git commit messages ready:

commit 3a0af03df24166f29147ea16e56a5eba7e32abca
Author: Akim Demaille <address@hidden>
Date:   Wed May 13 07:31:31 2020 +0200

    cex: add gnulib dependencies
    
    * bootstrap.conf (gnulib_modules): Add linked-list.

commit c10fcb647e7e8bccbe2d4d2238d45352289cda1f
Author: Vincent Imbimbo <address@hidden>
Date:   Tue May 12 18:10:43 2020 -0400

    cex: add support for state-item pair graph generation
    
    * src/lssi.h, src/lssi.c, src/state-item.h, src/state-item.c: New.

commit 41a91c0b66c8f246918ee49328ac4cf42e6332a9
Author: Vincent Imbimbo <address@hidden>
Date:   Tue May 12 21:42:45 2020 -0400

    cex: introduce the parse simulator
    
    * src/derivation.h, src/derivation.c,
    * src/parse-simulation.h, src/parse-simulation.c: New.

commit ea6bac333c5eb5295bf6769a0e2a9789051e43fb
Author: Vincent Imbimbo <address@hidden>
Date:   Tue May 12 21:59:57 2020 -0400

    cex: introduce counterexample search
    
    * src/counterexample.h, src/counterexample.c: New.

commit ae07d7b26fb281ddf07715a5777437922aa686ec
Author: Vincent Imbimbo <address@hidden>
Date:   Tue May 12 22:01:08 2020 -0400

    cex: bind counterexample generation
    
    * src/complain.h, src/complain.c: Add support for -Wcounterexample.
    * src/conflicts.c (report_counterexamples): New.
    (rule_conflicts_print): Use it when -Wcounterexample is given.
    * src/getargs.h, src/getargs.c: Add support for --trace=cex.
    * src/main.c (main): Init and deinit counterexample generation.

commit 71fbf5fcf08eb117ba750bf8e9cfa4ca9eabc6d3
Author: Vincent Imbimbo <address@hidden>
Date:   Tue May 12 22:01:39 2020 -0400

    cex: add tests
    
    * tests/counterexample.at: New.



>> I also had to fix some conflicts with complain.[ch] (what did you rebase
>> against?).
> 
> I forked sometime in October maybe? There's been a warning option added in
> the meantime. I couldn't pull from master as the merge commit would've made
> it a lot harder to rebase.

I took care of that.


>> The changes in bootstrap.cfg are also lacking, so I'm adding them.  There
>> are many warnings to address (e.g., "int foo()" is not a valid signature in
>> C, you need "int foo(void)", or global/local name conflicts).
>> 
> I wasn't getting warnings during my build, I should have tested on more
> than MacOS.

No, that's not the problem.  The issue is that you had not enabled
compiler warnings I guess.  That's what I meant here:
https://github.com/akimd/bison/pull/15#issuecomment-587063993

>> I also need to make sure the test suite passes on the CI, which requires
>> adjust the test cases, or maybe disabling some of them.  I'm not done yet.
>> I've pushed the current state of the branch as
>> https://github.com/akimd/bison/tree/cex.
>> 
> So I mentioned in the cover letter that I didn't want to update these until
> we had decided where cex output goes. Right now none of the tests contain
> their expected results. IIRC the effects of cex are non-deterministic on
> the existing.at tests (there's a lot of conflicts without unifying
> examples), so those tests should probably just not use it.

Yep, you did warn me.  Yet I will not push changes that break the test suite.
I'll see what's the best approach to handle these cases.  But I first have
to get this compile properly.  This morning's changes are not enough
(https://travis-ci.org/github/akimd/bison/jobs/686444542).

Cheers!