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
Re: [PG-devel] Supported version of Emacs
I think the most important is that your documentation should contain or point to a documentation of coq stm. Cheers Pierre Le sam. 1 déc. 2018 à 01:46, Emilio Jesús Gallego Arias a écrit : > Pierre Courtieu writes: > > > I am all for it, where can I find the serapi documentation please? > > That's a good point, the documentation is fairly sketchy as we didn't > see the need to make the API stable yet. > > In fact one of the problems Paul has pointed out was lack of > specification of the XML protocol [which was 100% undocumented when the > effort started IIRC] > > I will add some specification for the 8.9 version, any recommendation on > to best document such a protocol? > > As the protocol is programmatically derived from > > https://github.com/ejgallego/coq-serapi/blob/v8.9/serapi/serapi_protocol.mli > I think I will use OCaml's `odoc` format. > > Binaries command line is reasonably documented with --help. > > Cheers, > E. > ___ 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&check 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] 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. P Le sam. 1 déc. 2018 à 16:24, Stefan Monnier a écrit : > 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&check 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 > ___ 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&check 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
Re: [PG-devel] Supported version of Emacs
Pierre Courtieu writes: > I think the most important is that your documentation should contain or > point to a documentation of coq stm. Why? I'd rather document SerAPI by itself, why to expose the low-level document manager? Note that the README is not accurate anymore, as SerAPI is not tied to the STM anymore, so yeah this may be confusing. I've already wrote a fair chunk of up-to-date documentation for it, hopefully will make it into the main branch soon. Cheers, E. ___ 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
Pierre Courtieu writes: > 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. The main problem is that Coq 8.6 is unsupported upstream, and it seems de-facto orphaned in Debian. So yeah, it is not optimal both for upstream and for the users for example when they run into long-solved bugs and report to us. Cheers, E. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel