metamath / metamath-exe

Metamath program - source code for the Metamath executable
GNU General Public License v2.0
75 stars 25 forks source link

warnings caused by comments #158

Open benjub opened 12 months ago

benjub commented 12 months ago

@GinoGiotto :

mmwtex.c:863:1: warning: multi-line comment [-Wcomment]
  863 | // points to a quoted string, the quoted string is returned.  A non-alphanumeric\
      | ^
mmwtex.c:1667:9: warning: multi-line comment [-Wcomment]
 1667 |         //  #define PROCESS_EVERYTHING PROCESS_SYMBOLS + PROCESS_LABELS \
      |         ^
GinoGiotto commented 12 months ago

I committed the fixes in f4b2f6b and 15bd94e.

These warnings seem to be caused by the presence of the escape character \ at the end of lines. I'm not sure what it was used to communicate, but my guess is that it was used to indicate that the next line is a continuation of the previous one. I think the same idea can be conveyed using indentation (as I already did in other occasions), while in other circumstances I think it can simply be removed.

benjub commented 12 months ago

These warnings seem to be caused by the presence of the escape character \ at the end of lines. I'm not sure what it was used to communicate, but my guess is that it was used to indicate that the next line is a continuation of the previous one. I think the same idea can be conveyed using indentation (as I already did in other occasions), while in other circumstances I think it can simply be removed.

For command lines, it means indeed continuation to the next line, and you can paste in the terminal such multilines. I think it's ok to remove them. You can indicate on the MR that fixes it that it closes this issue, so that merging it will automatically close this issue. Thanks.

digama0 commented 12 months ago

Why didn't CI catch this? Are warnings being ignored?

digama0 commented 12 months ago

The \ at the end of prose can be removed, but the ones in the gcc invocation and the #define line are important, those are continuation lines from the commented shell code / C code itself. I would recommend using block comments for that.

GinoGiotto commented 12 months ago

The \ at the end of prose can be removed, but the ones in the gcc invocation and the #define line are important, those are continuation lines from the commented shell code / C code itself. I would recommend using block comments for that.

I committed the updated fix in 02a2103.

Why didn't CI catch this? Are warnings being ignored?

I'm not sure how the pipeline handles error checking, but I noticed that if the full set of options is executed then more warnings appear:

gcc m*.c -o metamath -O2 -Wall -Wextra -Wmissing-prototypes \
             -Wmissing-declarations -Wshadow -Wpointer-arith -Wcast-align \
             -Wredundant-decls -Wnested-externs -Winline -Wno-long-long \
             -Wconversion -Wstrict-prototypes -std=c99 -pedantic -Wunused-result
mmdata.c:64:18: warning: redundant redeclaration of 'nmbrTempAlloc' [-Wredundant-decls]
 temp_nmbrString *nmbrTempAlloc(long size);
                  ^~~~~~~~~~~~~
In file included from mmdata.c:20:0:
mmdata.h:592:18: note: previous declaration of 'nmbrTempAlloc' was here
 temp_nmbrString *nmbrTempAlloc(long size);
                  ^~~~~~~~~~~~~
mmfatl.c: In function 'initBuffer':
mmfatl.c:107:39: warning: declaration of 'buffer' shadows a global declaration [-Wshadow]
 static void initBuffer(struct Buffer* buffer) {
                                       ^~~~~~
mmfatl.c:92:22: note: shadowed declaration is here
 static struct Buffer buffer;
                      ^~~~~~
mmfatl.c: In function 'isBufferEmpty':
mmfatl.c:123:55: warning: declaration of 'buffer' shadows a global declaration [-Wshadow]
 inline static bool isBufferEmpty(struct Buffer const* buffer) {
                                                       ^~~~~~
mmfatl.c:92:22: note: shadowed declaration is here
 static struct Buffer buffer;
                      ^~~~~~
mmfatl.c: In function 'getLastBufferedChar':
mmfatl.c:136:54: warning: declaration of 'buffer' shadows a global declaration [-Wshadow]
 static char getLastBufferedChar(struct Buffer const* buffer) {
                                                      ^~~~~~
mmfatl.c:92:22: note: shadowed declaration is here
 static struct Buffer buffer;
                      ^~~~~~
mmfatl.c: In function 'isBufferOverflow':
mmfatl.c:148:58: warning: declaration of 'buffer' shadows a global declaration [-Wshadow]
 inline static bool isBufferOverflow(struct Buffer const* buffer) {
                                                          ^~~~~~
mmfatl.c:92:22: note: shadowed declaration is here
 static struct Buffer buffer;
                      ^~~~~~
mmfatl.c: In function 'appendText':
mmfatl.c:178:43: warning: declaration of 'buffer' shadows a global declaration [-Wshadow]
                            struct Buffer* buffer) {
                                           ^~~~~~
mmfatl.c:92:22: note: shadowed declaration is here
 static struct Buffer buffer;
                      ^~~~~~
mmfatl.c:183:24: warning: conversion to 'unsigned int' from 'int' may change the sign of the result [-Wsign-conversion]
   return buffer->begin - start;
          ~~~~~~~~~~~~~~^~~~~~~
mmfatl.c: In function 'initState':
mmfatl.c:237:43: warning: declaration of 'state' shadows a global declaration [-Wshadow]
 static void initState(struct ParserState* state, struct Buffer* buffer) {
                                           ^~~~~
mmfatl.c:227:27: note: shadowed declaration is here
 static struct ParserState state;
                           ^~~~~
mmfatl.c:237:65: warning: declaration of 'buffer' shadows a global declaration [-Wshadow]
 static void initState(struct ParserState* state, struct Buffer* buffer) {
                                                                 ^~~~~~
mmfatl.c:92:22: note: shadowed declaration is here
 static struct Buffer buffer;
                      ^~~~~~
mmfatl.c: In function 'unsignedToString':
mmfatl.c:276:23: warning: conversion to 'char' from 'unsigned int' may alter its value [-Wconversion]
       digits[--ofs] = (value % 10) + '0';
                       ^
mmfatl.c: In function 'checkOverflow':
mmfatl.c:293:47: warning: declaration of 'state' shadows a global declaration [-Wshadow]
 static bool checkOverflow(struct ParserState* state) {
                                               ^~~~~
mmfatl.c:227:27: note: shadowed declaration is here
 static struct ParserState state;
                           ^~~~~
mmfatl.c: In function 'handleText':
mmfatl.c:313:44: warning: declaration of 'state' shadows a global declaration [-Wshadow]
 static void handleText(struct ParserState* state) {
                                            ^~~~~
mmfatl.c:227:27: note: shadowed declaration is here
 static struct ParserState state;
                           ^~~~~
mmfatl.c: In function 'handleSubstitution':
mmfatl.c:342:52: warning: declaration of 'state' shadows a global declaration [-Wshadow]
 static void handleSubstitution(struct ParserState* state) {
                                                    ^~~~~
mmfatl.c:227:27: note: shadowed declaration is here
 static struct ParserState state;
                           ^~~~~
mmfatl.c: In function 'parse':
mmfatl.c:381:39: warning: declaration of 'state' shadows a global declaration [-Wshadow]
 static void parse(struct ParserState* state) {
                                       ^~~~~
mmfatl.c:227:27: note: shadowed declaration is here
 static struct ParserState state;
                           ^~~~~
mmfatl.c: In function 'fatalErrorInit':
mmfatl.c:416:18: warning: declaration of 'buffer' shadows a global declaration [-Wshadow]
   struct Buffer* buffer = getBufferInstance();
                  ^~~~~~
mmfatl.c:92:22: note: shadowed declaration is here
 static struct Buffer buffer;
                      ^~~~~~
mmfatl.c: In function 'fatalErrorPush':
mmfatl.c:423:23: warning: declaration of 'state' shadows a global declaration [-Wshadow]
   struct ParserState* state = getParserStateInstance();
                       ^~~~~
mmfatl.c:227:27: note: shadowed declaration is here
 static struct ParserState state;
                           ^~~~~
mmfatl.c: In function 'fatalErrorPrintAndExit':
mmfatl.c:439:18: warning: declaration of 'buffer' shadows a global declaration [-Wshadow]
   struct Buffer* buffer = getBufferInstance();
                  ^~~~~~
mmfatl.c:92:22: note: shadowed declaration is here
 static struct Buffer buffer;
                      ^~~~~~
mmfatl.c: In function 'fatalErrorExitAt':
mmfatl.c:468:25: warning: declaration of 'state' shadows a global declaration [-Wshadow]
     struct ParserState* state = getParserStateInstance();
                         ^~~~~
mmfatl.c:227:27: note: shadowed declaration is here
 static struct ParserState state;
                           ^~~~~
mmveri.c: In function 'assignVar':
mmveri.c:633:20: warning: declaration of 'foundFlag' shadows a previous local [-Wshadow]
               flag foundFlag = 0;
                    ^~~~~~~~~
mmveri.c:555:16: note: shadowed declaration is here
           flag foundFlag = 0;
                ^~~~~~~~~
mmveri.c:713:13: warning: declaration of 'p' shadows a previous local [-Wshadow]
   for (long p = 0; p < substSchemeLen; p++) {
             ^
mmveri.c:286:8: note: shadowed declaration is here
   long p = 0; // Position in bigSubstSchemeAss
        ^
mmveri.c:726:13: warning: declaration of 'p' shadows a previous local [-Wshadow]
   for (long p = 0; p < substSchemeLen; p++) {
             ^
mmveri.c:286:8: note: shadowed declaration is here
   long p = 0; // Position in bigSubstSchemeAss
        ^

It seems there is some lack of checks in the metamath-exe repo, but here fixes could be less trivial so I don't think I'm the right person to address that.

benjub commented 12 months ago

For the redundant declaration at mmdata.c:64 you can simply remove that line (and its comment) since it is indeed declared later in the file, at a more appropriate place IMO (and the function is not used in between these two declarations).

For mmfatl.c:183 the return type of the function should probably be changed to long, that is,

static long appendText(char const* source, enum SourceType type,

For mmfatl.c:276, using an explicit cast should be enough:

digits[--ofs] = (char) ((value % 10) + '0');

All other warnings are about shadowing.

It would be safer to ask someone who knows C well. Since many warnings come from mmfatl, maybe @wlammen can have a look ?

david-a-wheeler commented 12 months ago

Warnings aren't considered errors by default by most C compilers. We could do that; the challenge is that compilers often add new warnings, and they're sometimes false positives. I much prefer warning-free code, at least at release time, but we don't want end-users who recompile the program to have a build failure just because they're using a newer compiler.

digama0 commented 12 months ago

I think we should be running warnings as errors in CI. That is all I am saying. There is no reason for users to be prevented from running the program just because warnings are emitted, but that wouldn't happen in the first place if CI is green.

david-a-wheeler commented 12 months ago

I think we should be running warnings as errors in CI.

Agreed. I believe there's a trivial way to do that, I'll just have to look it up, but we first need to fix the warnings :-).

There is no reason for users to be prevented from running the program just because warnings are emitted, but that wouldn't happen in the first place if CI is green.

If the user uses a different compiler, including a different version, then it almost certainly will happen to them. But we'll have eliminated the warning messages we got, and that would be a great start.

In the longer term we could run two different compilers & make sure it's warning-free on both. I'm overseeing work on the Linux kernel to get that point with clang in addition to gcc. But that's a potential idea for some future time.