Proof General question

[Todd Wilson]

After many years of using the old emacs interface to Abella, I've recently been trying to use Proof General. It would be wonderful if PG could be configured to support the layout conventions that I use with my files automatically, but absent that, i would be happy if PG would simply not insert newlines every time I type "." at the end of a tactic or untab lines that I've already indented to support my layout convention when hitting newline to go to the next line. The PG documentation mentions a promising variable proof-next-command-insert-space, but setting this to nil doesn't have the effect I was expecting. In fact, customizing the variable and saving says that my ~/.emacs file has been written, but no change is made to the file. If I set the variable myself with setq, it doesn't help. Maybe this has something to do with the Abella PG being a fork of the original? Any suggestions?

[Kaustuv Chaudhuri]

I don't see anything in PG that *inserts* newlines when you hit '.'. However, if you have proof-electric-terminator-enable set to t then it will automatically run the command when you type '.' and as a side effect will move the cursor to the next line (if one exists). I suspect that's what you're seeing.

If so, the fix is simple: just put (setq proof-electric-terminator-enable nil) somewhere in your initialization scripts. If you want to use customization, you can also run M-x customize-variable proof-electric-terminator-enable to change the value of the variable and then C-x C-s to save the customization for future runs. I don't use customize, so I can't give you more precise guidance -- maybe asking on #emacs at irc.freenode.net will give you more fruitful answers about your initialization/customization files.

Neither of the Abella modes knows anything about indentation. Generally speaking TAB should indent the current line the same as the next line, but that's about all you get.

Kaustuv

On Fri, Feb 1, 2019 at 10:56 PM Todd Wilson <lambdaca...@gmail.com> wrote:

After many years of using the old emacs interface to Abella, I've recently been trying to use Proof General. It would be wonderful if PG could be configured to support the layout conventions that I use with my files automatically, but absent that, i would be happy if PG would simply not insert newlines every time I type "." at the end of a tactic or untab lines that I've already indented to support my layout convention when hitting newline to go to the next line. The PG documentation mentions a promising variable proof-next-command-insert-space, but setting this to nil doesn't have the effect I was expecting. In fact, customizing the variable and saving says that my ~/.emacs file has been written, but no change is made to the file. If I set the variable myself with setq, it doesn't help. Maybe this has something to do with the Abella PG being a fork of the original? Any suggestions?

--
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 post to this group, send email to abella-the...@googlegroups.com.
Visit this group at https://groups.google.com/group/abella-theorem-prover.
For more options, visit https://groups.google.com/d/optout.

[Todd Wilson]

I was enjoying some of the behavior of the electric '.', just not the insertion of whitespace, but I guess from what you're saying is that it is all or nothing. Also, my problem with indentation is that it's retroactively applied in an annoying manner. For example, if my proof script has

induction on 1. intros. case H1.
  search.

then, when I hit ENTER at the end of the second line to start my second subgoal, the indentation at the beginning of this line is deleted. There is an option abella-text-indent, which I can set to nil, but then I get no indentation at all: TAB does nothing, and I have to do all indentation manually with spaces, which is also a no-go. I'm hoping that there is a sensible middle ground somewhere.

[Kaustuv Chaudhuri]

This sounds like you have electric-indent-mode active, which is a general Emacs-level thing and not PG or Abella specific.

I would recommend turning it off because (a) it's painfully annoying, as you describe, and (b) when you need its functionality you can use C-j instead of RET.

Kaustuv

--

[Todd Wilson]

Setting electric-indent-mode to nil indeed fixed the annoying automatic reindentation of lines, so thanks for that, but indentation still doesn't work for me. In my example from above:

induction on 1. intros. case H1.
  search.

when I hit the RET key at the end of the second line, it doesn't reindent this line, but it leaves me in column 0 of the next line and hitting TAB has no effect. If I indent the beginning of my second subgoal, say

  case H2.

and then hit TAB, it deletes the indent at the beginning of this line. I have no idea why, since the previous line was indented two characters.

All I really want here is the default emacs treatment of tabs, where hitting TAB calls indent-relative, which indents according to the previous line. But my attempts to achieve this seem to be clobbered by PG during its start-up. If this really can't be achieved, how have others set up their PG environment to deal with tabbing?

On Monday, February 4, 2019 at 10:49:41 PM UTC-8, Kaustuv Chaudhuri wrote:

This sounds like you have electric-indent-mode active, which is a general Emacs-level thing and not PG or Abella specific.

I would recommend turning it off because (a) it's painfully annoying, as you describe, and (b) when you need its functionality you can use C-j instead of RET.

Kaustuv

On Mon, Feb 4, 2019 at 9:35 PM Todd Wilson <lambdaca...@gmail.com> wrote:

I was enjoying some of the behavior of the electric '.', just not the insertion of whitespace, but I guess from what you're saying is that it is all or nothing. Also, my problem with indentation is that it's retroactively applied in an annoying manner. For example, if my proof script has

induction on 1. intros. case H1.
  search.

then, when I hit ENTER at the end of the second line to start my second subgoal, the indentation at the beginning of this line is deleted. There is an option abella-text-indent, which I can set to nil, but then I get no indentation at all: TAB does nothing, and I have to do all indentation manually with spaces, which is also a no-go. I'm hoping that there is a sensible middle ground somewhere.

--
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-prover+unsub...@googlegroups.com.

[Kaustuv Chaudhuri]

Add to your ~/.emacs or equivalent:

(add-hook 'abella-mode-hook
          #'(lambda ()
              (setq indent-line-function 'indent-relative)))

Kaustuv

To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-p...@googlegroups.com.

To post to this group, send email to abella-the...@googlegroups.com.
Visit this group at https://groups.google.com/group/abella-theorem-prover.
For more options, visit https://groups.google.com/d/optout.

--

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.

[Todd Wilson]

That did it, thanks. Following the PG documentation, I had tried adding this to proof-mode-hook, but that didn't work. It might be nice to document abella-mode-hook, maybe even with this example, in the Emacs Support section of the Reference Guide.

To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-prover+unsub...@googlegroups.com.

To post to this group, send email to abella-the...@googlegroups.com.
Visit this group at https://groups.google.com/group/abella-theorem-prover.
For more options, visit https://groups.google.com/d/optout.

--
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-prover+unsub...@googlegroups.com.