search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
489 stars 86 forks source link

howto configure warnings for 8.6 #140

Open hendriktews opened 7 years ago

hendriktews commented 7 years ago

I open this issue to foster the discussion about how to configure warnings in 8.6. If you have an opinion, please leave a comment.

erikmd commented 7 years ago

Hi @hendriktews, Thanks for recapitulating all this!

The mechanism to configure warnings should work for both, background compilation and coqtop invocation.

Agreed.

We could insert an Set Warnings command before we process the scripting buffer in coqtop.

Agreed.

[...] There seems to be a hierarchy in the warnings, but there is no documentation about it. It would be nice to have a list of all warnings and the ones that are enabled by default, but I cannot find either.

I didn't find much doc on the warnings in the current version of Coq refman, but it seems that the list of all warnings can be found by searching for the "CWarnings.create" pattern in the sources (e.g. with this link).

It would surely be impressive to have radio buttons for all the warnings, but do we need this?

Anyway that'd be indeed impressive! But maybe such a feature would be useful enough if there were radio buttons just for "warnings categories", not for each individual warning?

Is there a way to configure warnings in _CoqProject that works with other tools?

I think this is related to #113 as well as to coqbug 5109, which itself mentions PR coq/coq#305 ...

Best wishes! Erik

Matafou commented 7 years ago

coq_makefile accepts option "-arg foo" which pass option foo to coqc and coqtop, and IIRC I I implemented -arg recognition for pg. So I guess it should already work. I can't test right now but I will later today. There may be issues with options with complex syntax.

cpitclaudel commented 7 years ago

@Matafou Indeed, this could work; it would be nice to have a configuration system consistent with CoqIDE. That being said, _CoqProject is so horrendous that this could be another reason to push for a better format.

Matafou commented 7 years ago

Someone is recoding coq_makefile currently it may be time to list what you don't like with _CoqProject.

cpitclaudel commented 7 years ago

I saw Enrico's email. I'm hoping to chat about this at POPL. My issue with _CoqProject is the lack of semantics (It's just a bunch of command line arguments, but the syntax isn't specified, as far as I can tell)

cpitclaudel commented 7 years ago

Maybe a more precise characterization is that the original format was nice and simple (sequences of -optname optarg1 … optargn), but now that you can add paths you run into problems with quotes and escaping.

hendriktews commented 7 years ago

Here is the list of warnings in 8.6 (relying on the pattern CWarnings.create). I am not sure, a menu with 24 submenus and 71 tick boxes in total is useful, although it would be a nice little hack to generate the necessary emacs lisp code automatically...

24 categories with 71 warnings in total