[new release] colibrilib, colibrics and colibri2 (0.4)

[bobot]

CHANGES:

• Decision: Fix delayed decisions handling
• Array: experimental theory
• Quantifier: Improve eager instanciation heuristic
• Quantifier: Avoid creating new term
• Simplex: Fix redundant run
• Fix compilation in 32bit
• Fix sign of sqrt

[bobot]

@Gbury There is a strange behavior of dolmen in 5.0. I don't know where the problem is (colibri2, dolmen, ocaml) but after raising an exception inside a pipeline of dolmen, there is a syscall read with the file descriptor -1 (which result in a sys.error EBADF). Before sending the issue to 5.0 do you have an idea?

Catchpoint 1 (call to syscall read), 0x00007ffff7a6d992 in __GI___libc_read (fd=fd@entry=-1, buf=buf@entry=0x55555765ef5c, nbytes=nbytes@entry=65536) at ../sysdeps/unix/sysv/linux/read.c:26
26	in ../sysdeps/unix/sysv/linux/read.c
(gdb) bt
#0  0x00007ffff7a6d992 in __GI___libc_read (fd=fd@entry=-1, 
    buf=buf@entry=0x55555765ef5c, nbytes=nbytes@entry=65536)
    at ../sysdeps/unix/sysv/linux/read.c:26
#1  0x000055555687b401 in read (__nbytes=65536, __buf=0x55555765ef5c, __fd=-1)
    at /usr/include/x86_64-linux-gnu/bits/unistd.h:38
#2  caml_read_fd (fd=-1, flags=<optimized out>, buf=buf@entry=0x55555765ef5c, 
    n=65536) at runtime/unix.c:87
#3  0x000055555686d20d in caml_ml_input (vchannel=<optimized out>, 
    buff=<optimized out>, vstart=<optimized out>, vlength=<optimized out>)
    at runtime/io.c:935
#4  <signal handler called>
#5  0x0000555556202aaf in camlStdlib__input_297 () at stdlib.ml:421
#6  0x0000555556223b3a in camlStdlib__Lexing__lex_refill_313 () at lexing.ml:85
#7  0x0000555556046dd5 in camlDolmen_smtlib2_v6_script__Lexer____ocaml_lex_token_rec_727 () at src/languages/smtlib2/v2.6/script/lexer.ml:581
#8  0x000055555614c98d in camlDolmen_std__Transformer__lexer_824 ()
    at src/standard/transformer.ml:95
#9  0x0000555556042884 in camlDolmen_smtlib2_v6_script__Parser___menhir_run_326_8362 () at src/languages/smtlib2/v2.6/script/parser.ml:8005
#10 0x000055555614ca20 in camlDolmen_std__Transformer__fun_1152 ()
    at src/standard/transformer.ml:101
#11 0x0000555555f1cde9 in camlDolmen_loop__Parser__fun_1835 ()
    at src/loop/parser.ml:153
--Type <RET> for more, q to quit, c to continue without paging--c
#12 0x0000555555f1cf08 in camlDolmen_loop__Parser__wrap_parser_1135 () at src/loop/parser.ml:168
#13 0x0000555555f01bee in camlDolmen_loop__Pipeline__eval_gen_fold_937 () at src/loop/pipeline.ml:156
#14 0x0000555555f01b2b in camlDolmen_loop__Pipeline__eval_936 () at src/loop/pipeline.ml:148
#15 0x0000555555f01d4d in camlDolmen_loop__Pipeline__run_aux_985 () at src/loop/pipeline.ml:169
#16 0x0000555555f01eee in camlDolmen_loop__Pipeline__run_996 () at src/loop/pipeline.ml:194
#17 0x0000555555c223e7 in camlColibri2_solver__Input__read_6712 () at colibri2/solver/input.ml:542
#18 0x0000555555b653d6 in camlColibri2_main__Main__entry () at colibri2/bin/main.ml:53
#19 0x0000555555b5621b in caml_program ()
#20 <signal handler called>
#21 0x000055555687e378 in caml_startup_common (pooling=<optimized out>, argv=0x7fffffffe088) at runtime/startup_nat.c:129
#22 caml_startup_common (argv=0x7fffffffe088, pooling=<optimized out>) at runtime/startup_nat.c:85
#23 0x000055555687e3ef in caml_startup_exn (argv=<optimized out>) at runtime/startup_nat.c:136
#24 caml_startup (argv=<optimized out>) at runtime/startup_nat.c:141
#25 caml_main (argv=<optimized out>) at runtime/startup_nat.c:148
#26 0x0000555555b531b2 in main (argc=<optimized out>, argv=<optimized out>) at runtime/main.c:37

[Gbury]

@bobot there is indeed a bug with dolmen and ocaml 5.0, related to finalisers. It turns out to be a bug in the implementation of the gc in 5.0, see ocaml/ocaml#11995 . I have a fix for dolmen that I'll push as soon as possible, and then I'll add conflicts on old releases of dolmen, and re-do the 0.8.1 release.

[Gbury]

For some more explanation: a finaliser is called too early (before the related value is unreachable), and the finaliser actually closes the in_channel, which makes the subsequent reads of the input file into errors.

[bobot]

I propose to add in this MR the conflict now in dolmen 0.8.0 in all version for ocaml 5.0.

[Gbury]

Since i expect the finaliser bug to be patched in an upcoming 5.0.1 (and basically all other versions of ocaml), maybe a constraint != "5.0.0" would actually be better for the future ?

[kit-ty-kate]

Flint's tests also fail on OCaml 5.0:

# File "flint/tests/dune", line 9, characters 8-15:
# 9 |  (names dynamic)
#             ^^^^^^^
# (cd _build/default/flint/tests && ./dynamic.exe)
# Fatal error: exception Dynlink.Error (Dynlink.Cannot_open_dll "Dynlink.Error (Dynlink.Cannot_open_dll \"Failure(\\\"/home/opam/.opam/5.0/lib/ctypes/ctypes.cmxs: cannot open shared object file: No such file or directory\\\")\")")

[bobot]

For ocaml 5.0 the problem was in ctypes: yallop/ocaml-ctypes#727 , I will surely add the patch on the last version of ctypes. (EDIT: a point release will be done later)

[bobot]

I think it is okay now. The last problem are 5.0 because of ctypes which is in another MR, macos-homebrew-ocaml-4.14-arm64 (and I don't understand what is happening) but it is experimental and s390x-ocaml-4.14 but just not enough memory for the compilation.

[Gbury]

Not sure why my review was requested (since this PR does not modify dolmen packages anymore), but I'm happy to approve, ^^

[bobot]

@kit-ty-kate could you merge this PR?

[bobot]

@kit-ty-kate Flint and the others have been removed, so the remaining packages are not failing anymore.

[mseri]

The remaining failures are likely going away once the mac-compatible arb, flint and calcium are released

[mseri]

Thanks

[mseri]

Thanks