Problem installing 2.0.6 from opam

[Todd Wilson]

In the past I've installed Abella from git, but I thought I'd try it using opam. I am using Ubuntu 20.04. It tried to install 2.0.2 instead:

twilson-desktop:~$ opam install abella

The following actions will be performed:

  ∗ install ocamlbuild 0.14.0 [required by abella]

  ∗ install conf-m4    1      [required by ocamlfind]

  ∗ install ocamlfind  1.8.1  [required by abella]

  ∗ install abella     2.0.2

===== ∗ 4 =====

Do you want to continue? [Y/n] n

twilson-desktop:~$ opam --version

2.0.5

twilson-desktop:~$ ocaml --version

The OCaml toplevel, version 4.08.1

Any idea what the problem is?

[Kaustuv Chaudhuri]

It appears that the OPAM maintainers forcibly added a < 4.08.0 constraint to Abella around the time of the release of OCaml 4.08.0 because of the backwards incompatibility in OCaml for that version. (That's around when they removed the Pervasives module.)

The issue on Abella's side has been fixed in git for over a year and it should compile with any OCaml version in the 4.x series. So, I would suggest that you stick with git for the time being.

I will try to figure out how to fix the package description files on OPAM's side.

This issue is being tracked as #132: https://github.com/abella-prover/abella/issues/132

Kaustuv

--
You received this message because you are subscribed to the Google Groups "Abella" group.
To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-p...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/abella-theorem-prover/d64c49ac-4af7-4c60-b51a-a8aeced68dddn%40googlegroups.com.

[Todd Wilson]

Thanks. Are there instructions anywhere for installing from scratch on the major platforms using git that I can direct my students to?

[Kaustuv Chaudhuri]

I've packaged all the bugfixes over the past year into a new release of Abella, version 2.0.7.

I've also fixed the package descriptions on OPAM. As soon as the pull request below is merged, it should be available from OPAM.

https://github.com/ocaml/opam-repository/pull/18053

Kaustuv

[Todd Wilson]

I can confirm that 2.0.7 is now installable directly via opam. Thanks!