search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

Abella 2.0.6 does not work well with PG #124

Closed kyagrd closed 4 years ago

kyagrd commented 4 years ago

I am not exactly sure whether this is PG issue or abella issue

When I upgrade to 2.0.6, and also update PG to the latest gitup repo abella branch, it does not work well. PG only goes forward. Undo does not work and gives me "Syntax error" at the bottom of emacs. I am using GNU Emacs 26.3 on debian unstable.

RandomActsOfGrammar commented 4 years ago

I had the same issue about a month ago, which is long enough ago for me to forget exactly what I did to fix it. I now have Proof General working normally with Abella 2.0.6 in GNU Emacs 26.3 on Arch Linux. This issue was fixed for me while I was trying to solve a different issue, I think, related to getting the correct version of Abella installed. It might therefore be relevant that I have OCaml version 4.07.1. Both OCaml and Abella are installed through Opam.

One difference between our setups is that I have the normal Proof General installed from GitHub with Abella added to it rather than the Abella version of Proof General. The directions for adding Abella to a regular installation are in the abella directory of the Abella-specific Proof General repository.

kyagrd commented 4 years ago

I actually did a fresh install of abella after moving my old .opam direcitry somewhere else. I'm running the abella-pg script inside the pulled GithHub repo directory (PG/abella) after compiling it via make.

One thing is that there is also proofgeneral debian package installed in the system but I thought that running via abella-pg script bypasses the system installed proofgeneral. Maybe I was assuming wrong?

Next time, I should try removing the system installed proofgeneral and see if the same problem occurs. Currently, reverted back to 2.0.5 for now because of this issue.

kyagrd commented 4 years ago

Okay, I followed the instructions on the abella webpage on how to set up .emacs script for abella PG. Once I put that in the emacs script and run emacs normally rather than via abllea-pg script the problem went away.

So, I am closing myself.

To avoid the same problem, don't use the abella-pg script in the PG/abella directory but follow the instructions about .emacs setup as recommended.

chaudhuri commented 4 years ago

Sorry for the late reply, but yes, you have to follow the instruction in the abella user guide to get PG working.

This reminds me that I need to rebase the Abella code to the most recent PG version. We may also try to get the Abella mode merged upstream in PG. (I wasn't successful last time, but I didn't try particularly hard.)

chaudhuri commented 4 years ago

I've pushed an abella-PG mode that is up-to-date with PG master.

Bad news: it seems that PG has undergone some massive rewrite in their async branch, and their master branch is no longer being (actively?) maintained. Abella-PG may stop working whenever PG upstream makes the switch to the async branch. To be revisited in the near future...