Haskell upgrade issues: SMTLib2 vs. logic-TPTP

[salmans]

Currently, smtlib2 (Razor's interface to the SMT solver) doesn't build with the latest version of GHC (7.8): initially, it termintes with an stack-overflow on the context stack. @ryandanas can confirm the same error on Linux; that is, this error is not specific to OSX. After finding workarounds to fix this bug, compilation fails with numerous other type errors. However, the package builds successfully using the older version of GHC (7.6). On the contrary, logic-TPTP (for parsing TPTP inputs) builds successfully on GHC 7.8 but not on GHC 7.6. The problem with TPTP is a known issue in the Haskell community about 7.6, which has been fixed in 7.8. I tried every possible solutiom to reconcile these two libraries over the weekend but I didn't make any progress. Since smtlib2 is the package that is not working with the latest version of GHC, I am going to contact its developer and ask him if they can migrate to GHC any time soon. For now, because smtlib2 is critical for our demo next week, I am going to downgrade GHC on my machine and stick to 7.6, which means we should postpone our TPTP work. Any ideas?

[dandougherty]

No ideas for fixing, of course, but I'm wondering: how come this didn't arise before?. We were already doing * some * work with TPTP, right?

Sent from my iPhone

On Jan 19, 2015, at 8:05 AM, Salman Saghafi notifications@github.com wrote:

Currently, smtlib2 (Razor's interface to the SMT solver) doesn't build with the latest version of GHC (7.8): initially, it termintes with an stack-overflow on the context stack. @ryandanas can confirm the same error on Linux; that is, this error is not specific to OSX. After finding workarounds to fix this bug, compilation fails with numerous other type errors. However, the package builds successfully using the older version of GHC (7.6). On the contrary, logic-TPTP (for parsing TPTP inputs) builds successfully on GHC 7.8 but not on GHC 7.6. The problem with TPTP is a known issue in the Haskell community about 7.6, which has been fixed in 7.8. I tried every possible solutiom to reconcile these two libraries over the weekend but I didn't make any progress. Since smtlib2 is the package that is not working with the latest version of GHC, I am going to contact its developer and ask him if they can migrate to GHC a ny time soon. For now, because smtlib2 is critical for our demo next week, I am going to downgrade GHC on my machine and stick to 7.6, which means we should postpone our TPTP work. Any ideas?

— Reply to this email directly or view it on GitHub.

[thedotmatrix]

As far as I know, TPTP was working fine before 7.6, and now is fine on 7.8. Additionally, since we weren't using TPTP recently, the logic-tptp package was not included in the cabal file (not built in).

Sticking with GHC 7.6 sounds like a good idea for this week. As far as TPTP work goes, I can still work on manually translating good candidates for case studies and taking more performance notes. I think the implementation of the TPTP repl-mode will have to wait though.

[salmans]

Yes, the reason it didn't happen before because we were not building logicTPTP with Razor. @dandougherty I remember you had this problem with the previous (first-order) version and I took out logic-TPTP from the list of Razor dependencies.

[salmans]

Henning (smtlib2's developer) just wrote back to me. He is investigating to see if he finds a fast/easy solution to migrate to GHC 7.8.3; at the same time, he is open to accepting patches from us in case we want to do the migration ourselves. This depends on how fast we want the migration happen.

[salmans]

Good news! Henning has done the upgrade to the new version. The updates are available on his GitHub repo. I am going to test the code this morning and make sure there aren't other issues when compiling Razor with 7.8 before I write back to him and ask him to push the changes to Hackage

[salmans]

I tested smtlib2 with GHC 7.8 in a cabal sandbox; Razor compiles with both smtlib2 and logic-TPTP. I asked Henning to make his library available on Hackage.

[salmans]

The latest version of smtlib2 is now on Hackage