Re: [PG-devel] Indentation tests
> You have something like that in Coq/ex/indent.v. > I dream of a smie with two grammars (and lexers): one for first lines of > commands and one inside commands. It would greatly simplify things I think. I don't really know how to define "first lines" and "inside", but you can definitely have "two grammars" with SMIE: You can combine two smie-grammars with something like (append (mapcar (lambda (x) (cons (concat "1" (car x)) (cdr x))) grammar1) (mapcar (lambda (x) (cons (concat "2" (car x)) (cdr x))) grammar2)) then you can combine the two tokenizing functions with: (defun combined-fun () (if (in-first-lines-of-commands) (let ((tok (fun1))) (if tok (concat "1" tok))) (let ((tok (fun2))) (if tok (concat "2" tok) this won't quite work right because: - the tokenizer can return nil for open/close parens and such in which case the above will fail to add the corresponding "1" or "2" prefix. - the relative precedence of the two grammars is left unspecified so it can lead to surprises when crossing between one part and the other. But neither of those two problems are hard to fix, I think. Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Indentation tests
I'd go with any large file in the source distribution of Coq. In fact, a good test might be to clone the Coq repo, reindent the whole standard library, check these changes in, then reindent again with your changes and look at the git diff. I expect the standard library + the Coq test suite to cover all or almost all of the syntax of Coq. Clément. On 01/12/2018 10.24, Stefan Monnier wrote: > I have a few tentative changes to coq-smie.el. > Does someone have some kind of test-suite somewhere against which I can > run my new code to try and avoid regressions? > > Ideally, it should be fully automated, including fixing my bugs and > outputting a Coq proof that the result is correct, but I'll settle for > a long file that I need to reindent manually. > > So far I have the coq/indent.v but it doesn't seem to include some cases > that are mentioned in coq-smie.el, so I'm hoping someone has something > a bit more complete. > > > Stefan > ___ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel > signature.asc Description: OpenPGP digital signature ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Indentation tests
I have a few tentative changes to coq-smie.el. Does someone have some kind of test-suite somewhere against which I can run my new code to try and avoid regressions? Ideally, it should be fully automated, including fixing my bugs and outputting a Coq proof that the result is correct, but I'll settle for a long file that I need to reindent manually. So far I have the coq/indent.v but it doesn't seem to include some cases that are mentioned in coq-smie.el, so I'm hoping someone has something a bit more complete. Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
