New indentation engine #591

Matafou · 2021-07-13T18:03:21Z

This PR proposes a new simplified indentation implementation.

It still uses smie. The main design choice for this new version is that the first word of a command is now a token "Com start". Together with the "." token for ending a command this makes the smie grammar parsing much more "local".

Users may experience a few changes in the indentation: a few special cases where the old indentation would avoid shifting to the right have been removed.

Non regression testing have been added. But:

Should the test go in the ci directory as I did, or should it go elsewhere? Ideally it would be nice (but not mandatory) to include this tests in the ci @erikmd

monnier · 2021-07-13T18:21:45Z

It still uses smie. The main design choice for this new version is that the first word of a command is now a token "Com start". Together with the "." token for ending a command this makes the smie grammar parsing much more "local".

;; Com1 .(1) ;; Definition foo := bar .(2) ;; ... ;; could easily lead to the grammar tree ;; ;; __.(2) ;; .(1) \ ;; / \ ... ;; / \ ;; Com1 := ;; / \ ;; Def foo bar ;; ;; which means that "(1)" is the parent of ":=", which is the parent ;; of "Def foo". This leads to hell. We need Def to be the parent. But ;; there are hundreds of commands in coq. so we adopt the policy below. ;; ;; 2. the lexer tries to always treat the first word of a command as a ;; dstinguished token "Com start". And a command is of the form ("Com ;; start" exp) in smie grammar. This way the top-node of a command is ;; always this token. ;; ;; This way the above script is parsed as: ;; ;; __.(2) ;; .(1) \ ;; / \ ... ;; / \ ;; Com1 Com start ;; | ;; := ;; / \ ;; foo bar I haven't looked at the actual code, but the above sounds great to me. Stefan

cpitclaudel · 2021-07-13T18:43:36Z

Awesome work. Thanks Pierre. I'm not qualified to look at the actual code, but the motivation looks 👍.

A few examples / tests that were developed to indent "correctly" in the current system. How are the following indented with the new code? (what's below is how they are currently indented)

  Instance spec_of_vect_memcpy : spec_of "vect_memcpy" :=
    fnspec! "vect_memcpy" (len: word) (a1_ptr a2_ptr : address) /
          {n1} (a1: VectorArray.t word n1)
          {n2} (a2: VectorArray.t word n2)
          (pr1: word.unsigned len < Z.of_nat n1)
          (pr2: word.unsigned len < Z.of_nat n2)
          R,
    { requires tr mem :=
        (vectorarray_value AccessWord a1_ptr a1 ⋆
                           vectorarray_value AccessWord a2_ptr a2 ⋆ R) mem;
      ensures tr' mem' :=
        tr' = tr /\
        let res := vect_memcpy len a1 a2 pr1 pr2 in
        (vectorarray_value AccessWord a1_ptr (fst res) ⋆
                           vectorarray_value AccessWord a2_ptr (snd res) ⋆ R) mem' }.

  Instance spec_of_crc32 : spec_of "crc32" :=
    fnspec! "crc32" data_ptr len / (data : list byte) R ~> r,
    { requires tr mem :=
        (word.unsigned len = Z.of_nat (length data) /\
         (listarray_value AccessByte data_ptr data * R)%sep mem);
      ensures tr' mem' :=
        tr' = tr /\
        r = crc32' data /\
        (listarray_value AccessByte  data_ptr data * R)%sep mem' }.

        <{ Trace := tr;
           Memory := mem;
           Locals := locals;
           Functions := functions }>
        cmd.seq
          (cmd.while
             (expr.op (if signed then bopname.lts else bopname.ltu)
                      (expr.var from_var)
                      (expr.var to_var))
             body_impl)
          k_impl
        <{ pred (nlet_eq vars v k) }>

Matafou · 2021-07-14T10:18:05Z

@cpitclaudel there is problem with the <{ }> thing. I will try to fix it before merging.

@monnier I think that tweaking the lexer to parenthesize each command is a good way to go indeed. I should perhaps re-do the lexer(s) completely but for now it seems to work OK.

Matafou · 2021-07-14T11:14:07Z

    <{ Trace := tr;
       Memory := mem;
       Locals := locals;
       Functions := functions }>
      cmd.seq
        (cmd.while
           (expr.op (if signed then bopname.lts else bopname.ltu)
                    (expr.var from_var)
                    (expr.var to_var))
           body_impl)
        k_impl
      <{ pred (nlet_eq vars v k) }>

(provided this is inside a real command) this is not indented as you want (see the shift of cmd.seq). I understand this is a hoare-like triple?
I will try to give a solution, but you were relying on a bug :-): basically you exploited the fact that this was indented badly (think that < as +):

  Definition foo :=
    + 3 +
    5. (* this should be (and is now) shifted to the right*)

cpitclaudel · 2021-07-14T13:01:26Z

Indeed, it's a hoare triple. The command being indented isn't too bad.

I will try to give a solution, but you were relying on a bug :-)

I suspected so :) I'm happy to change the syntax, too — but I was very happy when I found that trick, since it allowed me to indent very naturally:

Definition … :=
   <{ … }>
   Some code here
     and the continuation lines worked perfectly!
   <{ and this magically aligned with the first part of the triple :) }>

So the really nice part is that the two halves of the triple line up ^^ It would be fine if the program part was indented further.

monnier · 2021-07-14T13:47:12Z

I suspected so :) I'm happy to change the syntax, too — but I was very happy when I found that trick, since it allowed me to indent very naturally: ``` Definition … := <{ … }> Some code here and the continuation lines worked perfectly! <{ and this magically aligned with the first part of the triple :) }> ```

Actually, if you take the analogy with `+` and treat both `<` and `>` as having the same precedence, then the above would "naturally" indent to: ``` Definition … := <{ … }> Some code here and the continuation lines worked perfectly! <{ and this magically aligned with the first part of the triple :) }> ``` Stefan

Matafou · 2021-07-15T10:13:23Z

@monnier you are right but only if < and > are declared left associative. I think I will do this. It behaves the way @cpitclaudel wants. It is still a hack that said. I wonder if there could be a better way. Maybe a special "three parts" expression...

Matafou · 2021-07-15T10:17:04Z

@cpitclaudel the !fnspec ... / ... , ... gets a shift to the right after the ,. Is it ok?

cpitclaudel · 2021-07-15T13:42:40Z

@cpitclaudel the !fnspec ... / ... , ... gets a shift to the right after the ,. Is it ok?

Yes, that's even better than the current indentation actually :)

monnier · 2021-07-15T13:46:28Z

@monnier you are right but only if `<` and `>` are declared left associative.

Or just "associative" (i.e. have the same left and right precedence), as is used for `;`, `,`, etc..

I think I will do this. It behaves the way @cpitclaudel wants. It is still a hack that said.

Yup.

I wonder if there could be a better way. Maybe a special "three parts" expression...

I think doing it right with Clément's current syntax requires either changing the lexer (so it returns different tokens for the "<{" and the "}>" of the preconditions than those of the post conditions) or extra ad-hoc rules in the indentation rules: the grammar itself can't be made to understand the structure because it is basically assert ::= "<{" e "}>" e ::= ... | assert e assert but operator precedence grammars have as core constraint that you need a terminal between every pair of non-terminals. You can turn the grammar into: e ::= ... | "<{" e "}>" e "<{" e "}>" but this leads to unsolvable constraints, the closest solution to those constraints is to make those tokens "associative" (i.e. same precedence on both sides and same precedence for both tokens), so you lose the original structure. My guess is that if you want to indent the middle `e` deeper, the better solution is to add an ad-hoc indenting rule (e.g. indent deeper if you're right after a "}>" and the next token has higher left precedence). Stefan PS: This is also why you can't really have `.` as terminator but only as separator: terms ::= term terms ::= term "." terms is fine but term1 ::= term "." terms ::= term1 terms ::= term1 terms isn't since there's no terminal between `term1` and `terms`.

cpitclaudel · 2021-07-15T14:21:12Z

Thanks both! I'm fine with changing the syntax if that helps, the current one was co-evolved with the previous parser specifically so that it would indent nicely :)

Matafou · 2021-07-15T14:34:11Z

@monnier you are right but only if < and > are declared left associative.

Or just "associative" (i.e. have the same left and right precedence), as is used for ;, ,, etc..

That is not what I see. if I have (assoc "<" ">") I have this indentation:

  Definition foo :=
    < fooo
        bar >
      rab
      < foo
          bar >.

Maybe there is something wrong with my grammar? It says simply (exp "<" exp) (exp ">" exp).
Only with "left" do I have the two "<" at the same column.

Matafou · 2021-07-15T14:41:58Z

@erikmd can you tell me how to have the new indentation tests (currently in ci/test-indentation) should be made part of the CI?

Not a blocker anyways.

monnier · 2021-07-15T15:19:24Z

> > @monnier you are right but only if `<` and `>` are declared left associative. > Or just "associative" (i.e. have the same left and right precedence), as > is used for `;`, `,`, etc.. That is not what I see. if I have `(assoc "<" ">")` I have this indentation: ``` Definition foo := < fooo bar > rab < foo bar >. ```

Hmm... you might be right that the rule that does what I expected checks that the token is equal rather than just checking the precedence.

erikmd · 2021-07-20T18:57:04Z

@erikmd can you tell me how to have the new indentation tests (currently in ci/test-indentation) should be made part of the CI?

Not a blocker anyways.

Hi @Matafou, thanks for all this work on the indentation engine!
I've just seen your mention about CI, basically the place where you committed the indentation test-suite is very fine (in ci/), and we'll just need to add some "GitHub Actions job" + some shell commands in file .github/workflows/test.yml to launch the tests themselves automatically (and fail if an error has been detected).

Indeed, I guess it'd be very nice if this automation can be added before merging the PR (if you want we'll be able to discuss this briefly in the upcoming PG telco).

erikmd · 2021-07-20T19:24:29Z

Hi @Matafou, I've just run the tests.sh and I got this:

Testing indent-tac-boxed.v... TEST FAILURE ***
  *** details can be seen with:
  ***  diff --side-by-side --suppress-common-lines indent-tac-boxed.v indented_indent-tac-boxed.v
  *** or graphically: 
  ***  meld indent-tac-boxed.v indented_indent-tac-boxed.v
Testing indent-inside-command-boxed.v... TEST FAILURE ***
  *** details can be seen with:
  ***  diff --side-by-side --suppress-common-lines indent-inside-command-boxed.v indented_indent-inside-command-boxed.v
  *** or graphically: 
  ***  meld indent-inside-command-boxed.v indented_indent-inside-command-boxed.v
Testing indent_monadic.v... TEST FAILURE ***
  *** details can be seen with:
  ***  diff --side-by-side --suppress-common-lines indent_monadic.v indented_indent_monadic.v
  *** or graphically: 
  ***  meld indent_monadic.v indented_indent_monadic.v
Testing indent-inside-command.v... TEST FAILURE ***
  *** details can be seen with:
  ***  diff --side-by-side --suppress-common-lines indent-inside-command.v indented_indent-inside-command.v
  *** or graphically: 
  ***  meld indent-inside-command.v indented_indent-inside-command.v
Testing indent-tac.v... TEST FAILURE ***
  *** details can be seen with:
  ***  diff --side-by-side --suppress-common-lines indent-tac.v indented_indent-tac.v
  *** or graphically: 
  ***  meld indent-tac.v indented_indent-tac.v
Testing indent-commands-boxed.v... TEST FAILURE ***
  *** details can be seen with:
  ***  diff --side-by-side --suppress-common-lines indent-commands-boxed.v indented_indent-commands-boxed.v
  *** or graphically: 
  ***  meld indent-commands-boxed.v indented_indent-commands-boxed.v
Testing indent-commands.v... TEST FAILURE ***
  *** details can be seen with:
  ***  diff --side-by-side --suppress-common-lines indent-commands.v indented_indent-commands.v
  *** or graphically: 
  ***  meld indent-commands.v indented_indent-commands.v
Testing indent_equations.v... TEST FAILURE ***
  *** details can be seen with:
  ***  diff --side-by-side --suppress-common-lines indent_equations.v indented_indent_equations.v
  *** or graphically: 
  ***  meld indent_equations.v indented_indent_equations.v

Attaching a zip of the folder with *.log files.

test-indent.zip

I'm using Emacs 26.1 on Debian 10

Matafou · 2021-08-15T16:33:21Z

@erikmd I can't reproduce, not easy for me to install emacs-26.
@hendriktews can you check that with 27 it works and 26 it does not please?

hendriktews · 2021-08-25T22:23:51Z

Your tests.sh assumes that "." is in $PATH. IMO this is usually not the case and I would suggest to change that.
All the following is with ./ prepended to coq-test-indent.sh in tests.sh.
When I run tests.sh I don't see a difference between emacs 27 and 26, see the attached output from running cd ci/test-indent; echo; emacs --version; echo; ./tests.sh in all containers with different emacs versions that I have. new-indend-log.log
To investigate a bit further, I also attach the output of cd ci/test-indent; echo; emacs --version; echo; ./tests.sh; echo; ls -l .*log; echo; cat .*log for 27.1 new-indend-cat-log-27.log and 26.1 new-indend-cat-log-26.log for a changed coq-test-inden.sh. The change removes -q from the diff invocation and puts set-x and set +x around the diff and the preceding echo line.

Main design choice for this new version: the first word of a command is now a token "Com start". Together with the "." token for ending a command this makes the parsing much more "local". Users may experience a few changes in the indentation. A few special cases where the old indentation would reduce shifting to the right have been removed. Non regression testing have been added. See comments in coq-smie.el at coq-smie-grammar for more details.

Matafou · 2021-08-26T17:40:54Z

@erik @hendriktews I made my test directory CI ready.
The PG/ci/test-indent contains a makefile, you just need to launch make and if some test fails it exits with code 1.
I don't know what needs to be done to trigger the test now but I think I can merge now (if the checks are OK).

hendriktews · 2021-08-26T21:23:39Z

The tests run fine here with emacs 27.1, 26.3, 26.2, 26.1, 25.3 and 25.1.

I don't know what needs to be done to trigger the test now but I think I can merge now (if the checks are OK).

your tests run without coq installed, therefore copy and adopt the
build recipe in .github/workflows/test.yml, ie. insert the
following at the end of that file:


  # 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

(keep the spaces at the front of all lines - it must be indented below the jobs tag on line 13!)

Matafou · 2021-08-27T08:37:19Z

Many thanks @hendriktews! I just pushed the CI config.

hendriktews · 2021-08-27T21:04:37Z

The new tests run fine, well done!

Matafou · 2021-09-09T08:29:06Z

I will merge today if noone objects.

Matafou · 2021-09-10T16:56:43Z

Let us wait for bug reports now :-).

* href: #593 (comment)

Matafou force-pushed the new-indent branch from 343ff08 to 6c5f73e Compare July 15, 2021 14:40

Matafou force-pushed the new-indent branch from 6c5f73e to e56a8d7 Compare August 26, 2021 15:42

Matafou added 2 commits August 26, 2021 18:10

Fix ProofGeneral#574 indent of ltac "letins" pattern.

7e51652

Matafou force-pushed the new-indent branch from e56a8d7 to e07f537 Compare August 26, 2021 16:18

Indentation testing CI ready (hopefully).

8707022

Adding the CI for indentation.

260a6a2

erikmd mentioned this pull request Sep 8, 2021

Minor tweaks encountered while trying to run the CI tests #593

Merged

Matafou merged commit 32b15ff into ProofGeneral:master Sep 10, 2021

erikmd added a commit that referenced this pull request Sep 12, 2021

test: Extend dist-tests target after merging #591

ad36557

* href: #593 (comment)

erikmd added kind: enhancement kind: test labels Sep 12, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

New indentation engine #591

New indentation engine #591

Matafou commented Jul 13, 2021

monnier commented Jul 13, 2021 via email

cpitclaudel commented Jul 13, 2021

Matafou commented Jul 14, 2021

Matafou commented Jul 14, 2021

cpitclaudel commented Jul 14, 2021

monnier commented Jul 14, 2021 via email

Matafou commented Jul 15, 2021

Matafou commented Jul 15, 2021

cpitclaudel commented Jul 15, 2021

monnier commented Jul 15, 2021 via email

cpitclaudel commented Jul 15, 2021

Matafou commented Jul 15, 2021

Matafou commented Jul 15, 2021

monnier commented Jul 15, 2021 via email

erikmd commented Jul 20, 2021

erikmd commented Jul 20, 2021 •

edited

Loading

Matafou commented Aug 15, 2021

hendriktews commented Aug 25, 2021

Matafou commented Aug 26, 2021

hendriktews commented Aug 26, 2021

Matafou commented Aug 27, 2021

hendriktews commented Aug 27, 2021

Matafou commented Sep 9, 2021

Matafou commented Sep 10, 2021

New indentation engine #591

New indentation engine #591

Conversation

Matafou commented Jul 13, 2021

monnier commented Jul 13, 2021 via email

cpitclaudel commented Jul 13, 2021

Matafou commented Jul 14, 2021

Matafou commented Jul 14, 2021

cpitclaudel commented Jul 14, 2021

monnier commented Jul 14, 2021 via email

Matafou commented Jul 15, 2021

Matafou commented Jul 15, 2021

cpitclaudel commented Jul 15, 2021

monnier commented Jul 15, 2021 via email

cpitclaudel commented Jul 15, 2021

Matafou commented Jul 15, 2021

Matafou commented Jul 15, 2021

monnier commented Jul 15, 2021 via email

erikmd commented Jul 20, 2021

erikmd commented Jul 20, 2021 • edited Loading

Matafou commented Aug 15, 2021

hendriktews commented Aug 25, 2021

Matafou commented Aug 26, 2021

hendriktews commented Aug 26, 2021

Matafou commented Aug 27, 2021

hendriktews commented Aug 27, 2021

Matafou commented Sep 9, 2021

Matafou commented Sep 10, 2021

erikmd commented Jul 20, 2021 •

edited

Loading