Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Tests failure with OCaml 5.2 #1047

Closed
kit-ty-kate opened this issue Feb 27, 2024 · 4 comments · Fixed by #1048 or #1049
Closed

Tests failure with OCaml 5.2 #1047

kit-ty-kate opened this issue Feb 27, 2024 · 4 comments · Fixed by #1048 or #1049

Comments

@kit-ty-kate
Copy link

The tests for alt-ergo currently fails when using OCaml 5.2

#=== ERROR while compiling alt-ergo.2.5.2 =====================================#
# context              2.2.0~beta2~dev | linux/x86_64 | ocaml-variants.5.2.0+trunk | file:///home/opam/opam-repository
# path                 ~/.opam/5.2/.opam-switch/build/alt-ergo.2.5.2
# command              ~/.opam/5.2/bin/dune build -p alt-ergo -j 1 --promote-install-files=false @install @runtest
# exit-code            1
# env-file             ~/.opam/log/alt-ergo-2395-562a0c.env
# output-file          ~/.opam/log/alt-ergo-2395-562a0c.out
### output ###
# File "tests/cram.t/run.t", line 1, characters 0-0:
# /usr/bin/git --no-pager diff --no-index --color=always -u _build/.sandbox/2230f8f3c94abeb6211ea04264c94d64/default/tests/cram.t/run.t _build/.sandbox/2230f8f3c94abeb6211ea04264c94d64/default/tests/cram.t/run.t.corrected
# diff --git a/_build/.sandbox/2230f8f3c94abeb6211ea04264c94d64/default/tests/cram.t/run.t b/_build/.sandbox/2230f8f3c94abeb6211ea04264c94d64/default/tests/cram.t/run.t.corrected
# index 938d571..b9a9b6d 100644
# --- a/_build/.sandbox/2230f8f3c94abeb6211ea04264c94d64/default/tests/cram.t/run.t
# +++ b/_build/.sandbox/2230f8f3c94abeb6211ea04264c94d64/default/tests/cram.t/run.t.corrected
# @@ -1,6 +1,6 @@
#    $ echo '(check-sat)' | alt-ergo --inequalities-plugin does-not-exist -i smtlib2 -o smtlib2 2>&1 >/dev/null | sed -E 's/\(\\".*\\"\)//'
#    alt-ergo: ; Fatal Error: [Dynlink] Loading the 'inequalities' reasoner (FM module) plugin in "does-not-exist" failed!
# -            >> Failure message: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure")
# +            >> Failure message: error loading shared library: Failure("$TESTCASE_ROOT/does-not-exist: cannot open shared object file: No such file or directory")
#  
#  Now we will have some tests for the models. Note that it is okay if the format
#  changes slightly, you should be concerned with ensuring the semantic is

This change in the compiler is expected and comes from ocaml/ocaml#12213 but it would be nice to have the tests fixed at some point so that we can make sure that all the packages are working as expected.

@bclement-ocp
Copy link
Collaborator

Thanks for the report! The new error message is better but hardcoding it was a mistake in the first place. The best would be to simply check for the "error loading shared library" string but iirc dune is picky in what it lets us do here — I'll look into it.

@bclement-ocp
Copy link
Collaborator

@kit-ty-kate this should be fixed by #1048. Do we need to publish a patch release on opam-repository?

bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Mar 1, 2024
We already use dune-site to manage plugin files. With this patch, we now
also use the dune-site mechanism to manage plugin loading for the
inequalities plugin. This should make alt-ergo work with bytecode-only
compilers again (see [1]).

We still use Dynlink directly for additional parsers. Support for parser
plugins is deprecated as it is not supported with the Dolmen frontend
and will be removed in a future release, so the churn doesn't seem worth
it.

Fixes OCamlPro#1047

[1] : ocaml/opam-repository#25294
@kit-ty-kate
Copy link
Author

Do we need to publish a patch release on opam-repository?

you don't have to per say but it would be nice for sure! ^_^

@bclement-ocp
Copy link
Collaborator

OK; it sounds like opam can live for a bit with this failure and we have some other minor stuff to do for compatibility with an internal lib so in that casewe will do a single patch release for these changes later this month.

bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Mar 1, 2024
We already use dune-site to manage plugin files. With this patch, we now
also use the dune-site mechanism to manage plugin loading for the
inequalities plugin. This should make alt-ergo work with bytecode-only
compilers again (see [1]).

We still use Dynlink directly for additional parsers. Support for parser
plugins is deprecated as it is not supported with the Dolmen frontend
and will be removed in a future release, so the churn doesn't seem worth
it.

Fixes OCamlPro#1047

[1] : ocaml/opam-repository#25294
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Mar 1, 2024
We already use dune-site to manage plugin files. With this patch, we now
also use the dune-site mechanism to manage plugin loading for the
inequalities plugin. This should make alt-ergo work with bytecode-only
compilers again (see [1]).

We still use Dynlink directly for additional parsers. Support for parser
plugins is deprecated as it is not supported with the Dolmen frontend
and will be removed in a future release, so the churn doesn't seem worth
it.

Fixes OCamlPro#1047

[1] : ocaml/opam-repository#25294
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Mar 1, 2024
We already use dune-site to manage plugin files. With this patch, we now
also use the dune-site mechanism to manage plugin loading for the
inequalities plugin. This should make alt-ergo work with bytecode-only
compilers again (see [1]).

We still use Dynlink directly for additional parsers. Support for parser
plugins is deprecated as it is not supported with the Dolmen frontend
and will be removed in a future release, so the churn doesn't seem worth
it.

Fixes OCamlPro#1047

[1] : ocaml/opam-repository#25294
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Mar 13, 2024
We already use dune-site to manage plugin files. With this patch, we now
also use the dune-site mechanism to manage plugin loading for the
inequalities plugin. This should make alt-ergo work with bytecode-only
compilers again (see [1]).

We still use Dynlink directly for additional parsers. Support for parser
plugins is deprecated as it is not supported with the Dolmen frontend
and will be removed in a future release, so the churn doesn't seem worth
it.

Fixes OCamlPro#1047

[1] : ocaml/opam-repository#25294
bclement-ocp added a commit that referenced this issue Mar 13, 2024
We already use dune-site to manage plugin files. With this patch, we now
also use the dune-site mechanism to manage plugin loading for the
inequalities plugin. This should make alt-ergo work with bytecode-only
compilers again (see [1]).

We still use Dynlink directly for additional parsers. Support for parser
plugins is deprecated as it is not supported with the Dolmen frontend
and will be removed in a future release, so the churn doesn't seem worth
it.

Fixes #1047

[1] : ocaml/opam-repository#25294
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Mar 13, 2024
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Mar 13, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
2 participants