Code cleanup

[digama0]

This is a todo list for myself or others to tackle, based on my reading of the code. This list is still incomplete, I haven't completed my first pass over the code yet.

• [ ] (WL) Create a best practice instruction file
• [ ] (WL) Create a maintainers guide
• [ ] Rename files to drop mm prefix
• [ ] Rename files to use words instead of DOS-compatible 8.3 names
• [x] Move source code to a src/ directory
• [X] Use #pragma once instead of include guards. (This is not standardized, but it is very widely supported.)
• [ ] Raise line limit from 79 characters to 100
• [x] Delete VAXC code (VAX machines are long out of use)
• [X] Remove foo(void) syntax Ugh, C is bugward compatible
• [ ] (DW) Change / FOO option syntax to unix-style --foo
• [ ] Use bool, true and false instead of 0 and 1
• [ ] (WL) replace flag with bool
• [ ] Move variable declarations from top of function to first use
• [ ] Standardize function brace style (I prefer open brace at EOL)
• [ ] Standardize return(x) and return (x) to return x
• [ ] Comments
  • [x] Use // comments instead of /* (or doc-comments where appropriate)
  • [ ] Standardize to 3rd person indicative mood
  • [ ] Standardize function documentation (doxygen?)
• [ ] Remove "old buggy compression" migration code
• [ ] parseProof returns magic numbers instead of an enum
• [ ] parseCompressedProof returns magic numbers instead of an enum
• [ ] Local labels use encoding without macros
• [ ] edit() function uses magic numbers
• [ ] hypReEntryFlagList uses magic numbers
• [ ] hasFloatingProof uses 'Y' and 'N' instead of true and false
• [ ] unkSubPrfSteps uses 'K' and 'U' instead of true and false
• [ ] interactiveUnify returns magic numbers instead of an enum
• [ ] readTexDefs returns magic numbers instead of an enum
• [ ] printTexComment returns magic numbers instead of defines
• [ ] processUndoStack returns defines instead of an enum
• [ ] Remove obsolete flag g_oldTexFlag
• [ ] Same code repeated 4 times here, extract a function
• [ ] Fix indentation in help0(), help1()
• [ ] Remove suggestion to contact Norm in help2() and bug()
• [ ] Suspicious error message and fix here. Is this standards-conforming?
• [ ] The code claims Aggregate initialization is not portable and does not use it to construct arrays, which explains some things. But I can't find any evidence of this online, even C89 seems to support it
• [ ] poolFree uses expressions like ((long *)ptr)[-3] that should be replaced by macros

[wlammen]

• Create a best practice instruction file
• Create a maintainers guide.
• replace flag with bool

[david-a-wheeler]

At a quick glance most look okay. However:

Use #pragma once instead of include guards. (This is not standardized, but it is very widely supported.)

If it's not in the standard, I think we should avoid it unless there's a strong need for it. I don't see the need. Include guards are old-school, but they always work. New doesn't mean better.

Raise line limit from 79 characters to 100

Any text editor can handle wide lines, but they're less nice when printing. Again, I don't see the big advantage. If the code needs that much indenting, maybe it should be broken up :-).

Remove foo(void) syntax

Why? This clearly & unambiguously states "there are no parameters". I think clarity is a good thing.

Standardize function brace style (I prefer open brace at EOL)

I also have that preference, but I'm happy to go either way. Both styles are in use. We probably ought to agree on some style, preferably a relatively common system. The real need is to enforce it with a style-checker; then we only have to argue about the style once & we can then just have the tools enforce it.

[david-a-wheeler]

BTW: I think it's critical to make such changes in relatively small chunks, focusing on one narrow issue at a time. That way, if one thing is accepted & the other rejected, the accepted work actually gets merged. It's also a lot easier to review changes when they're smaller & focused on one thing, which means progress is faster.

[david-a-wheeler]

Oh wait, I just remembered, do NOT change foo(void) to foo(). This is one of the differences between C and C++.

In C++, both foo(void) and foo() mean "takes no parameters". That is NOT true of C. In C:

• void foo() means "a function foo taking an unspecified number of arguments of unspecified type"
• void foo(void) means "a function foo taking no arguments"

Source: https://stackoverflow.com/questions/51032/is-there-a-difference-between-foovoid-and-foo-in-c-or-c

Since we mean "takes no parameters" it would be incorrect to remove the void in foo(void).

[david-a-wheeler]

We could also slowly transition from VAX-style option flags "/ARG" to Unix-style option flags "-s --long". Support both for a while, then eventually drop the old style. Then we could have filenames with slashes without weirdness :-).

[digama0]

Raise line limit from 79 characters to 100

Any text editor can handle wide lines, but they're less nice when printing. Again, I don't see the big advantage. If the code needs that much indenting, maybe it should be broken up :-).

The 79 character limit is a bit low unless you are working in a terminal. The 100 character limit suggestion is semi-arbitrary but matches e.g. the rust style guide. For metamath code specifically, 79 characters looks quite cramped given the indentation in many of the big functions.

The business with the H() function and improper indentation in mmhlpa.c seems to be specifically a result of the fact that the lines of output are themselves 79 characters, leaving no room for the rest of the code. (The rust style guide also suggests using 80 characters for comments / prose, even though the full line is 100 characters, which would solve this particular issue.)

BTW: I think it's critical to make such changes in relatively small chunks, focusing on one narrow issue at a time. That way, if one thing is accepted & the other rejected, the accepted work actually gets merged. It's also a lot easier to review changes when they're smaller & focused on one thing, which means progress is faster.

This is meant to be a tracking issue, which will correspond to many PRs, each of which will only address one or two of these issues at a time. I just don't want to pile on 30+ issues for all these little things when many of them probably won't be addressed for a while.

[benjub]

We could also slowly transition from VAX-style option flags "/ARG" to Unix-style option flags "-s --long". Support both for a while, then eventually drop the old style. Then we could have filenames with slashes without weirdness :-).

Currently, -a and --a are authorized labels in the Metamath language. Maybe this does not directly create ambiguities (for that, we would need Metamath commands with optional or multiple authorized ; I do not know if there are some), but this comes close, and this would put a requirement on future commands. A solution would be to require that labels begin with a (lowercase) letter. This would, in my opinion, be an improvement, but this would change the Metamath language.

[digama0]

I don't think this is a major issue. We can use label existence to disambiguate in the vast majority of cases, and if we really need to disambiguate we can use "label" when relevant.

[jkingdon]

We could also slowly transition from VAX-style option flags "/ARG" to Unix-style option flags "-s --long". Support both for a while, then eventually drop the old style. Then we could have filenames with slashes without weirdness :-).

I guess my impulse would be to leave option syntax alone. It affects a lot of scripts and user habits and the like and sounds like a lot of work that maybe I'd approach as "do this better in the next tool" rather than try to retrofit into metamath.exe? I mean, it appears that some people are a bit more worried than I am about the status quo (sounds like there's an issue with slashes in filenames which I apparently haven't run into but I probably just adjusted my habits to reflect whatever limitation exists), so maybe I'm not fully aware of why it would be worth it.

[digama0]

(sounds like there's an issue with slashes in filenames which I apparently haven't run into but I probably just adjusted my habits to reflect whatever limitation exists)

For the record, the issue is that on any linux-ish system, it is annoying to read ../set.mm/set.mm because this conflicts with the options for the read command. It works okay on windows because \ is the directory separator, and I imagine that the syntax comes from that heritage.

[david-a-wheeler]

Actually, I suspect Norm used the "/" for options because it comes from VAX VMS (Norm used VMS for many years). VMS user manual here: https://www.isis.stfc.ac.uk/Pages/vms-user-manual.pdf It's true that MS-DOS/Windows often uses "/" for options, but I think Norm was more influenced by VMS than DOS in this case.

[jkingdon]

For the record, the issue is that on any linux-ish system, it is annoying to read ../set.mm/set.mm because this conflicts with the options for the read command.

Looks like read "../set.mm/iset.mm" already works.

I'll agree with "annoying" although it would be worse if the only workaround were to cd to the directory containing set.mm first.