New indentation engine

.github/workflows/test.yml

@@ -223,3 +223,32 @@ jobs:
             sudo chown -R coq:coq ./ci
             make -C ci/simple-tests all
           endGroup
+
+  # Run indentation tests in ci/test-indent on all supported emacs
+  # versions without coq installed.
+  test-indent:
+    runs-on: ubuntu-latest
+
+    strategy:
+      matrix:
+        emacs_version:
+          - 25.1
+          - 25.2
+          - 25.3
+          - 26.1
+          - 26.2
+          - 26.3
+          - 27.1
+      max-parallel: 4
+      # don't cancel all in-progress jobs if one matrix job fails:
+      fail-fast: false
+
+    steps:
+    - uses: actions/checkout@v2
+
+    - uses: purcell/setup-emacs@master
+      with:
+        version: ${{ matrix.emacs_version }}
+
+    - run: emacs --version
+    - run: make -C ci/test-indent

CHANGES

@@ -193,6 +193,16 @@ also https://wiki.ubuntu.com/Releases).
     - 92: Compile before require from current directory failing
       with 8.5
 
+*** indentation code refactored
+
+    A big refactoring of the code for indentation has been done. You
+    may experience a few changes in indentation results. Mostly small
+    shifts to the right.
+
+    Variable `coq-indent-box-style' only affects indentation after
+    quantifiers (used to affect script braces "{").
+
+
 * Changes of Proof General 4.4 from Proof General 4.3
 
 ** ProofGeneral has moved to GitHub!

ci/test-indent/.gitignore

@@ -0,0 +1 @@
+indented_*

ci/test-indent/Makefile

@@ -0,0 +1,22 @@
+# This file is part of Proof General.
+# 
+# © Copyright 2021  Pierre Courtieu
+# 
+# Authors: Pierre Courtieu
+# Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
+# 
+# License:     GPL2+ (GNU GENERAL PUBLIC LICENSE)
+
+TESTS:=$(wildcard indent-*.v)
+INDENTED:=$(subst indent-,indented_indent-, $(TESTS))
+
+all: $(INDENTED)
+
+indented_%.v: %.v
+	@echo "### testing indentation of $<..."
+	@./coq-test-indent.sh $<
+
+.PHONY: clean
+
+clean:
+	rm -f indented_indent*

ci/test-indent/coq-test-indent.el

@@ -0,0 +1,96 @@
+;;; Regression testing of indentation.
+
+;;; Initially the file is indented as it is supposed to be. Each line
+;;; is unindented, then indented. If the new indentation differ a
+;;; comment is added to signal it.
+
+;;; WARNING: there are relative path names, so this currently works
+;;; only frowhen the current directory is the one containin this file.
+
+(defun blank-line-p ()
+  (= (current-indentation)
+     (- (line-end-position) (line-beginning-position))))
+
+
+(defun line-fixindent ()
+  (save-excursion 
+    (let ((end (line-end-position)))
+      (re-search-forward "fixindent" end t))))
+
+
+(defun test-indent-line (&optional nocomment)
+  (interactive)
+  (unless (or (blank-line-p) (line-fixindent))
+    (back-to-indentation)
+    (let ((init-col (current-column)))
+      ;; avoid moving comments 
+      (unless (proof-inside-comment (point)) (delete-horizontal-space))
+      (indent-according-to-mode)
+      (let ((res (- (current-column) init-col)))
+        (unless (= 0 res)
+          (save-excursion
+            (end-of-line)
+            (unless nocomment
+              (insert (format " (*<=== %s%d INDENT CHANGED *)"
+                              (if (< res 0) "" "+")
+                              res))))
+          res)
+        0))))
+
+
+(defun remove-previous-comment ()
+  (interactive)
+  (save-excursion
+    (end-of-line)
+    (let* ((com (re-search-backward " (\\*<===" (line-beginning-position) t))
+           (strt (and com (point)))
+           (end (and com (line-end-position))))
+      (when com (delete-region strt end)))))
+
+
+(defun test--indent-region (beg end boxed &optional nocomment)
+  (let ((line-move-visual nil)
+        ;; we store the last line number rather than the position
+        ;; since by inderting things we shift the end pos, but not the
+        ;; end line.
+        (last-line (line-number-at-pos end))
+        (stop nil))
+    (set (make-local-variable 'coq-indent-box-style) boxed)
+    (goto-char beg)
+    (while (and (<= (line-number-at-pos) last-line)
+                (not stop))
+      (remove-previous-comment)
+      (test-indent-line nocomment)
+      (setq stop (/= (forward-line) 0)))))
+
+(defun remove-comments-region (beg end)
+  (interactive "r")
+  (goto-char beg)
+  (let ((line-move-visual nil))
+    (while (< (point) end);; loops because end position changes.
+      (remove-previous-comment)
+      (forward-line))))
+
+
+(defun test-indent-region (beg end &optional boxed nocomment)
+  (interactive "r\nP")
+  (test--indent-region beg end boxed nocomment))
+
+
+(defun test-indent-region-boxed (beg end &optional nocomment)
+  (interactive "r")
+  (test--indent-region beg end t nocomment))
+
+
+(defun test-indent-buffer (&optional nocomment) (interactive)
+       (test--indent-region (point-min) (point-max) nil nocomment))
+
+(defun test-indent-buffer-boxed (&optional nocomment) (interactive)
+       (test--indent-region (point-min) (point-max) t nocomment))
+
+(defun launch-test (orig indented &optional boxed)
+    (load-file "../../generic/proof-site.el")
+    (find-file orig)
+    (write-file indented)
+    (if boxed (test-indent-buffer-boxed t) (test-indent-buffer t))
+    (write-file indented))

ci/test-indent/coq-test-indent.sh

@@ -0,0 +1,43 @@
+#!/bin/bash
+
+# This script should be launched from its own directory, so that file
+# coq-test-indent.el is accessible.
+
+GREEN='\033[1;32m'
+RED='\033[1;31m'
+MAGENTA='\033[1;35m'
+NC='\033[0m' # No Color
+
+TESTFILE=$1
+INDENTEDTESTFILE=indented_$1
+
+BOXED="nil" 
+if [[ "$1" == *"boxed.v" ]];
+then
+    BOXED="t"
+fi
+
+echo "cp $TESTFILE $INDENTEDTESTFILE"
+cp $TESTFILE $INDENTEDTESTFILE
+
+emacs -q -batch --eval "(progn (load-file \"coq-test-indent.el\") (launch-test \"$TESTFILE\" \"$INDENTEDTESTFILE\" $BOXED))" 
+
+# echo "grep \"INDENT CHANGED\" $INDENTEDTESTFILE"
+# grep "INDENT CHANGED" $INDENTEDTESTFILE
+echo -n " diff -q $TESTFILE $INDENTEDTESTFILE..."
+diff -q $TESTFILE $INDENTEDTESTFILE
+if [[ "$?" == 1 ]] ;
+then echo " DIFFERENCES FOUND" 
+     diff -u $TESTFILE $INDENTEDTESTFILE
+     printf "${RED} TEST FAILURE ***${NC}\n"
+     echo "  *** details can be seen by reproducing the tests:"
+     echo "  *** cd ci/test-indent"
+     echo "  *** make"
+     echo "  ***  diff --side-by-side --suppress-common-lines $TESTFILE $INDENTEDTESTFILE"
+     echo "  *** or graphically: "
+     echo "  ***  meld $TESTFILE $INDENTEDTESTFILE"
+     exit 1 # Make the test program fail, so that CI knows.
+else echo "NO DIFFERENCE"
+     printf "${GREEN} TEST SUCCESS *** ${NC}\n"
+     exit 0
+fi