alt-ergo
alt-ergo copied to clipboard
Installation of altgr-ergo on Ubuntu 22.04 fails
It looks like libgtksourceview2.0-dev
, needed to build conf-gtksourceview
, is not available anymore on Ubuntu 22.04:
$ opam install altgr-ergo
[ERROR] Package conflict!
* Missing dependency:
- conf-gtksourceview
depends on the unavailable system package 'libgtksourceview2.0-dev'. Use
`--no-depexts' to attempt installation anyway, or it is possible that a
depext package name in the opam file is incorrect.
$
$ lsb_release --release --id --short
Ubuntu
22.04
$
$ sudo apt install libgtksourceview-2.0-dev
[...]
E: Unable to locate package libgtksourceview-2.0-dev
E: Couldn't find any package by glob 'libgtksourceview-2.0-dev'
But libgtksourceview3.0-dev
is, please consider migrating to this:
$ sudo apt install libgtksourceview-3.0-dev
[...]
libgtksourceview-3.0-dev is already the newest version (3.24.11-2build1).
I tried to help by doing the migration myself: I replaced all occurrences of lablgtk{,2}
, conf-gtksourceview
, lablgtk2.sourceview2
and GSourceView2
with lablgtk3
, conf-gtksourceview3
, lablgtk3.sourceview3
and GSourceView3
respectively, but I got stuck because:
$ make altgr-ergo
dune build -p altgr-ergo @install
File "src/bin/gui/dune", line 10, characters 55-75:
10 | (libraries alt_ergo_common threads.posix lablgtk3 lablgtk3.sourceview3)
^^^^^^^^^^^^^^^^^^^^
Error: Library "lablgtk3.sourceview3" not found.
Hint: try:
dune external-lib-deps --missing --no-config --root . --ignore-promoted-rules --default-target @install --always-show-command-line --promote-install-files --release --only-packages altgr-ergo -p altgr-ergo --profile release @install
The hint didn't work as-is because of duplicate options, so I tried the intended:
$ dune external-lib-deps --missing -p altgr-ergo @install
Error: The following libraries are missing in the default context:
- lablgtk3.sourceview3
Hint: try:
opam install lablgtk3
Which was however already installed:
$ opam install lablgtk3
[NOTE] Package lablgtk3 is already installed (current version is 3.1.2).
As my familiarity with dune
is low, some searching told me that it's more complicated than one would expect: https://stackoverflow.com/questions/54876087/ocaml-dune-missing-library-opam-says-its-there
Indeed:
$ ocamlfind list | grep lablgtk3-sourceview3
lablgtk3-sourceview3 (version: n/a)
^^^
Which I couldn't find how to fix.
On a related note, the current github actions tester uses ubuntu-latest
, which for now points to Ubuntu 20.04, therefore the installation problem is not caught. Ubuntu 22.04 is still in beta: https://github.com/actions/virtual-environments
Thanks for going through this wall of text, hope this helps.
If you need to use altgr-ergo version 2.4.1, a docker image is available here : Altgr-ergo-2.4.1
You need to make sure your xserver allows access to non-network local connections by running xhost +local:root
then you can use altgr-ergo by launching a container with a volume to where your .ae
files are located :
docker run -it -v /tmp/.X11-unix:/tmp/.X11-unix -v ~/path/to-your-ae-files/:/home -e DISPLAY=unix$DISPLAY elias2049/altgr-ergo_gui:latest
This is a temporary solution as altgr-ergo will rely on gtk3
(in a not so distant future).
If you have troubles using this image, feel free to say it here, it might help me provide a better one.
Thanks, the workaround worked!
I retract the above: The prover now works, but the "edit" window doesn't open.
Can you share what kind of error you get when running altgr-ergo yourfile.ae
?
from inside docker:
root@d59764384b77:/home# altgr-ergo myfile.ae
[Error]GtkMain.init: initialization failed
ml_gtk_init: initialization failed
(altgr-ergo:9): GLib-GObject-WARNING **: 09:21:54.833: invalid (NULL) pointer instance
(altgr-ergo:9): GLib-GObject-CRITICAL **: 09:21:54.833: g_signal_connect_data: assertion 'G_TYPE_CHECK_INSTANCE (instance)' failed
(altgr-ergo:9): GLib-GObject-WARNING **: 09:21:54.851: invalid (NULL) pointer instance
(altgr-ergo:9): GLib-GObject-CRITICAL **: 09:21:54.851: g_signal_connect_data: assertion 'G_TYPE_CHECK_INSTANCE (instance)' failed
(altgr-ergo:9): GLib-GObject-WARNING **: 09:21:54.860: invalid (NULL) pointer instance
(altgr-ergo:9): GLib-GObject-CRITICAL **: 09:21:54.860: g_signal_connect_data: assertion 'G_TYPE_CHECK_INSTANCE (instance)' failed
(altgr-ergo:9): Gtk-CRITICAL **: 09:21:54.861: IA__gtk_settings_get_for_screen: assertion 'GDK_IS_SCREEN (screen)' failed
(altgr-ergo:9): Gdk-CRITICAL **: 09:21:54.862: IA__gdk_pango_context_get_for_screen: assertion 'GDK_IS_SCREEN (screen)' failed
(altgr-ergo:9): Pango-CRITICAL **: 09:21:54.862: pango_context_set_font_description: assertion 'context != NULL' failed
(altgr-ergo:9): Pango-CRITICAL **: 09:21:54.862: pango_context_set_base_dir: assertion 'context != NULL' failed
(altgr-ergo:9): Pango-CRITICAL **: 09:21:54.862: pango_context_set_language: assertion 'context != NULL' failed
(altgr-ergo:9): Pango-CRITICAL **: 09:21:54.862: pango_context_set_base_dir: assertion 'context != NULL' failed
(altgr-ergo:9): Gdk-CRITICAL **: 09:21:54.862: IA__gdk_pango_context_get_for_screen: assertion 'GDK_IS_SCREEN (screen)' failed
(altgr-ergo:9): Pango-CRITICAL **: 09:21:54.862: pango_context_set_font_description: assertion 'context != NULL' failed
(altgr-ergo:9): Pango-CRITICAL **: 09:21:54.862: pango_context_set_base_dir: assertion 'context != NULL' failed
(altgr-ergo:9): Pango-CRITICAL **: 09:21:54.862: pango_context_set_language: assertion 'context != NULL' failed
(altgr-ergo:9): Pango-CRITICAL **: 09:21:54.862: pango_context_set_base_dir: assertion 'context != NULL' failed
(altgr-ergo:9): GLib-GObject-CRITICAL **: 09:21:54.862: g_object_unref: assertion 'G_IS_OBJECT (object)' failed
(altgr-ergo:9): GLib-GObject-CRITICAL **: 09:21:54.862: g_object_unref: assertion 'G_IS_OBJECT (object)' failed
(altgr-ergo:9): Gtk-CRITICAL **: 09:21:54.862: IA__gtk_settings_get_for_screen: assertion 'GDK_IS_SCREEN (screen)' failed
(altgr-ergo:9): Gdk-CRITICAL **: 09:21:54.862: IA__gdk_screen_get_display: assertion 'GDK_IS_SCREEN (screen)' failed
(altgr-ergo:9): Gdk-CRITICAL **: 09:21:54.862: IA__gdk_keymap_get_for_display: assertion 'GDK_IS_DISPLAY (display)' failed
(altgr-ergo:9): GLib-GObject-CRITICAL **: 09:21:54.862: g_object_get: assertion 'G_IS_OBJECT (object)' failed
(altgr-ergo:9): Gdk-CRITICAL **: 09:21:54.862: IA__gdk_keymap_get_for_display: assertion 'GDK_IS_DISPLAY (display)' failed
Segmentation fault
One issue is that I can't run the why3 ide in the docker instance, which is where I want to use altgr-ergo.
It may be relevant that I'm on Wayland, the default for Ubuntu 22.04.
Yes, I forgot about the switch to wayland for Ubuntu 22.04 👀 .
FYI Why3 docker images include alt-ergo
by default (but it is an older version :
Package: alt-ergo Version: 2.0.0-5build1
as it is the one available on aptitude).
In your case I think you should be able to simply install alt-ergo
and not altgr-ergo
through opam :
opam install alt-ergo
(you will get version 2.4.1)
You won't have problems with libgtksourceview2.0-dev
as it is not required.
Running why3 config detect
once you successfully install alt-ergo
should give you access to the solver in the why3 ide.
-
altgr-ergo
is the opam package that embeds the alt-ergo SMT solver and the associated GUI (which is not used by many and hasn't been updated for a while). -
alt-ergo
is the opam package for the SMT solver and the associated CLI. It is how most people usealt-ergo
My workflow relies on the why3 ide and its killer feature, the proof tree on the left. I still need altgr-ergo
for the helpful "edit" window of the why3 ide. Is this the associated GUI you mentioned?
When I click Tools -> Edit while having an Alt-Ergo proof node selected, I get in the ide console:
There was an unrecoverable error during treatment of request:
command "edit"
with exception:
anomaly: Unix.Unix_error(Unix.ENOENT, "create_process", "altgr-ergo")
And since the docker image doesn't contain the why3 ide, I don't have an environment where both the ide and altgr-ergo are available.
The migration was done in the PR #513.