2019-03-21 15:46:44 (GMT)
Howdy, I'd like to start with work I've been doing on Zipperposition recently to update its dependencies:
- move from Sequence to Iter (mostly a renaming, but it's also clearer what these iterators are)
- move to msat 0.8, which should be much more efficient (it's still in a branch, but I'll merge soon-ish). This should help Avatar on problems with a lot of ground case splitting.
2019-03-21 15:49:35 (GMT)
branch for msat 0.8: https://github.com/c-cube/zipperposition/tree/wip-msat-0.8
2019-03-21 17:30:51 (GMT)
Oh, that will probably help to get rid of these errors, right?
ERROR: File "src/core/res.ml", line 203, characters 6-12: Assertion failed.
2019-03-21 17:31:39 (GMT)
2019-03-21 17:32:34 (GMT)
Ahah damn. Yes it should. It's been a lot of effort to make the new API and refactor the internals, but I hope it'll be much better.
2019-03-21 17:33:17 (GMT)
@Alexander Bentkamp now that y'all have good testing infrastructure, it'd be excellent if you could take the wip-msat0.8 branch and test it on as many problems as possible, to see if similar stuff pops up
2019-03-21 17:45:6 (GMT)
Also I'm sure the very first priority we have is to write a zulip bot that writes here whenever a large benchmark is run :wink:
2019-03-21 17:49:19 (GMT)
I have problems to install iter on the Jenkins:
alias opam2=/home/mfleury/opam-2.0.2-x86_64-linux opam2 switch 4.05.0+flambda eval `opam2 config env` opam2 install zarith containers sequence oasis msat menhir jbuilder oseq iter
gives me
[ERROR] No package named iter found.
Do I need a certain version of opam? Or of ocaml?
2019-03-21 17:49:48 (GMT)
maybe you need opam update?
2019-03-21 17:50:19 (GMT)
(I feel like zulip is going to be really helpful for this kind of troubleshooting, at least)
2019-03-21 18:28:11 (GMT)
yes, that worked!
2019-03-21 18:28:40 (GMT)
now it can't find zipperposition.native. Where is the binary in that branch?
2019-03-21 18:32:55 (GMT)
ok, found it in ./_build/default/src/main/zipperposition.exe
2019-03-21 18:33:33 (GMT)
The tests are running now.
2019-03-21 18:36:31 (GMT)
I'm wondering, does anyone else use Sequence or Iter? I'm not sure I explained it properly when I visited you in Amsterdam
2019-03-21 19:22:13 (GMT)
Of course, I use Sequence all the time!
2019-03-21 19:22:46 (GMT)
Cool! Well then it's replaced by Iter on master (which is a clearer and shorter name, no other significant change for this release). :)
2019-03-21 19:44:43 (GMT)
Ok, the res.ml error is gone:
errors.txt
2019-03-21 19:46:18 (GMT)
Neat! It might not show, but normally raw performance of the SAT solver should have improved. Thanks for checking.