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
Re: [PG-devel] Supported version of Emacs
I agree. One more argument: opam has problems and having Coq delivered only by opam is risky these days. So having a reliable fallback is good. Even if it is a bit outdated. P Le sam. 1 déc. 2018 à 03:53, Stefan Monnier a écrit : > > Now that you have mentioned it, we consider this pretty unoptimal and we > > agreed on removing Coq from Debian due to the perils of shipping an > > outdated version :( :( > > I find it perfectly adequate for my needs, FWIW. > And I'd be annoyed to have to install Coq manually. > 2 years old sounds like a really weird definition of outdated to me. > To take a "random" example, ProofGeneral tries to be compatible with > Emacs-24.3 which is 5 years old. > > > Stefan > ___ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel > ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
