Re: [PG-devel] [PATCH] coq: Add option to ignore warning from coqdep in auto-compilation mode.
Tom Prince writes: >Some developments don't fully qualify their imports, and so coqdep gives >warning about ambiguous imports. Allow these developments to use >auto-compilation mode anyway. Sorry about the delay, I somehow forgot about the issue. It's now fixed in the repository. The regular expression for detecting coqdep errors can be customized now and the default value is chosen more carefully to only match those cases where a library cannot be found. If you really want to ignore all warnings you can change coq-coqdep-error-regexp such that if will never match anything. But be prepared to hit the assertion in coq-map-module-id-to-obj-file, when you ignore the "library X is required and has not been found" warning for a require command. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] [PATCH] coq: Add option to ignore warning from coqdep in auto-compilation mode.
On Mon, 12 Sep 2011 08:20:44 +0200, Hendrik Tews wrote: > Tom Prince writes: >Some developments don't fully qualify their imports, and so coqdep gives >warning about ambiguous imports. Allow these developments to use >auto-compilation mode anyway. > Could you describe an example? What is coqdep printing in these > cases? *** Warning: in file categories/orders.v, required library setoids matches several files in path (found setoids.v in varieties, theory and categories; used the latter) ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] [PATCH] coq: Add option to ignore warning from coqdep in auto-compilation mode.
Tom Prince writes: Some developments don't fully qualify their imports, and so coqdep gives warning about ambiguous imports. Allow these developments to use auto-compilation mode anyway. Could you describe an example? What is coqdep printing in these cases? -(if (string-match "^\\*\\*\\* Warning" coqdep-output) +(if (and (not coq-auto-compilation-ignore-coqdep-warnings) + (string-match "^\\*\\*\\* Warning" coqdep-output)) I would rather prefer to change the regular expression here, in order to only ignore the warning about ambiguous imports. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
