Installation of altgr-ergo on Ubuntu 22.04 fails

[OrfeasLitos]

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.

[EliasGit2017]

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.

[OrfeasLitos]

Thanks, the workaround worked!

[OrfeasLitos]

I retract the above: The prover now works, but the "edit" window doesn't open.

[EliasGit2017]

Can you share what kind of error you get when running altgr-ergo yourfile.ae ?

[OrfeasLitos]

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.

[EliasGit2017]

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 use alt-ergo

[OrfeasLitos]

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.

[hra687261]

The migration was done in the PR #513.