CN: Race solvers

[dc-mak]

There are a few axes on which to race:

• Incremental vs non-incremental solver
• CVC5 vs Z3
• (Potentially) derived constraints vs minimal constraints

This seems like a good fit: https://github.com/ocaml-multicore/eio?tab=readme-ov-file#racing, although it would commit us to OCaml 5 (but avoid wrapping all the solver code in a monad).

Note: racing an incremental solver with other ones will naturally bring up some concurrency query-to-query, because the process will be the same, so cancelling queries may need to lock and clean up appropriately.

There is also an inherent racy-ness that the solver might return an answer after cancel is sent, in which case the incremental solver will be accidentally closed would need to be restarted with the correct context before the next query.

[bcpierce00]

Is it bad to commit to OCaml 5 at this point?

[PeterSewell]

I'd be happy committing to OCaml 5 - it's surely ok intra-VERSE. Getting industry folk to install any OCaml can be problematic, but I don't know any reason why 5 should be worse than 4.n ?

…

On Tue, 17 Dec 2024 at 15:56, Benjamin Pierce ***@***.***> wrote: Is it bad to commit to OCaml 5 at this point? — Reply to this email directly, view it on GitHub <#770 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFMZZUMR4FFXRVCWAIQFDT2GBCSHAVCNFSM6AAAAABTYPCMB6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDKNBYHA2DINRUGE> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[cp526]

Some linux distributions will have OCaml versions older than that pre-installed, so dependency on a newer OCaml will require an extra installation step for those users, but I don't think that should stop us if there's a good reason (such as the above).

[podhrmic]

FWIW I doubt that any industry partners will be installing OCaml natively, most likely mean of deployment seem to be a Docker image (see GaloisInc/VERSE-Toolchain#48). So as long as it can be installed and packaged in a Docker image, the specific version does not matter.