Metamath software future directions

[wlammen]

Currently the development of metamath.exe is orphanized. The discussion in pull request metamath/set.mm#2392 showed, there is interest in moving forward, and there exist already some ideas under the hood.

This issue is meant to evaluate the current state of affairs, and bundle further discussions in a single location, instead of hijacking other threads for this purpose.

To me, there seems to be neither a team dedicated to, nor matured results about, future directions of Metamath. Lets change this starting a discussion from scratch. As far as I am concerned, I will be busy over Xmas, but will have spare time afterwards.

Please post your ideas, regardless of whether they are blurred or laser-sharp. I am looking forward to learn about your visions.

Ideally, I should have started with my own ideas first, but I am in a bit of a hurry right now. Sorry.

Wolf

[wlammen]

If you don't like the idea of an inner circle, and want a broader public to share thoughts, consider opening a discussion in Google groups.

[tirix]

Thanks for starting this thread!

• I'd like to share here a link to metamath-knife, which ambition it is to become a widely usable library for Metamath, with functions similar to metamath-exe. Of course, it shall not prevent to maintain and develop metamath-exe!
• Before any major refactoring is done, I would like to get the opportunity to merge here changes I have done to generate the "structured typesetting" pages. At the time I did these changes, Norm had not yet setup this repository, and he asked me to hold on my changes until he was ready. I'll try to open a PR shortly (edit: see PR Structured Typesetting (STS) generation #9 )

[savask]

I think everyone agrees that a general cleanup of the codebase is necessary. I would suggest:

• Removing obsolete features, for example, mmmaci.c (Macintosh interface functions, whatever that is)
• Removing obsolete code - metamath-exe files often store older revisions in comments, for example, here are a few lines from mmpars.c:

char *readRawSource(/*vstring inputFn,*/ /* 2-Feb-2018 nm Unused argument */
         vstring fileBuf, /* added 31-Dec-2017 */
         /*long bufOffsetSoFar,*/  /* deleted 31-Dec-2017 nm */
         long *size /* 31-Dec-2017 Now an input argument */)
{
  long charCount = 0;
  /*char *fileBuf;*/ /* 31-Dec-2017 */
  char *fbPtr;
  /*long lineNum;*/ /* 2-Feb-2018 Now computed in rawSourceError() */
  flag insideComment;
  /* flag insideLineComment; */ /* obsolete */

Also I would like to see some optimizations for the minimization procedure. About an year ago I attempted to do it myself, but after failing to understand the code, I mailed a sketch of the idea to Norman, and he added it to his todo-list. I guess now I'll have to give it another try, so hopefully code cleanup will help.

[digama0]

Also I would like to see some optimizations for the minimization procedure. About an year ago I attempted to do it myself, but after failing to understand the code, I mailed a sketch of the idea to Norman, and he added it to his todo-list. I guess now I'll have to give it another try, so hopefully code cleanup will help.

Could you post this email or a distilled version of it in a new issue (or a PR, if your investigation made it that far)?

Deleting all the code history comments (except the changelog itself) sounds like a good idea. This looks like a technique from the days before version control; with git this stuff is entirely noise.

I would be careful about deleting obsolete features. It might be that you don't use it (or understand it) but someone else does, and I would hate for this to be a reason not to upgrade.

[savask]

Could you post this email or a distilled version of it in a new issue (or a PR, if your investigation made it that far)?

Done that in issue #10 .

I would be careful about deleting obsolete features. It might be that you don't use it (or understand it) but someone else does, and I would hate for this to be a reason not to upgrade.

I think the mmmaci.c thing I mentioned can be safely removed, metamath.c file writes at the top:

    mmmaci.c - THINK C Macintosh interface (obsolete)

[david-a-wheeler]

I think a lot of future work would be better put in metamath-knife but of course I'd say that :-). If speed is your goal, Rust can give you the same speed without memory safety failures.

I agree that removing obsolete code is a good idea; version control systems are a better place for that.

I was just thinking that C++ might ease up memory management a little bit (see, for example, memory pool management in mmdata.c), but perhaps maintainability of metamath-exe is the main concern. In any case, I will be glad to offer some help if someone starts the refactor.

If Metamath-exe is rewritten in C++, I suggest that be created as a fork of Metamath-exe. Switching languages is a big deal. Many people know C but not C++. More importantly, making the switch to C++ "worth it" requires a significant amount of rewriting. It might probably ease up memory management slightly, but not very much. Both C and C++ require manual memory management, and C++'s prime simplification is calling the destructor when a variable goes out of scope. You have to do a fair amount of rewriting to make the switch to C++ really useful.

Even if switching to C++ is the eventual goal, I suggest starting with a cleanup of the C code to remove no-longer-used code, making variable names clearer, adding a CI test pipeline with tests, etc. All of that is lower-risk, and would make a C++ fork easier to implement.

[wlammen]

The earliest standards covering C are from Kernigan & Richie, but at the time Metamath sprang into existence (1992) the ANSI C standard was in effect. In a few locations Norman Megill mentioned this standard, for example in (0.198) mminou.c line 326ff, or on his website http://us2.metamath.org/index.html#contribute: "The metamath program (version 0.198 7-Aug-2021), which is an ASCII-based ANSI C program with a command-line interface."

ANSI C (aka ISO89, ISO90)

Link: https://en.wikipedia.org/wiki/ANSI_C

The standard has to be bought from the ANSI, but copies (or close approximations to it) are found on the internet:
http://web.archive.org/web/20030222051144/http://home.earthlink.net/~bobbitts/c89.txt

Macros identifying ANSI C

See https://sourceforge.net/p/predef/wiki/Standards:
A close candidate is __STD_C__ that exists on fully compliant compilers.

Unfortunately, not all compilers actually supported this macro. It is known that some versions of Microsoft MSVC will set this macro only, if explicitly requested (https://docs.microsoft.com/de-de/cpp/preprocessor/predefined-macros?view=msvc-170).

So ANSI C is silently assumed to be the C standard followed by Metamath software.

Question: Shall we stick with that?

[digama0]

I don't think we need to stick with an old C standard. Adherence to the details of the standard is less important than the side effect of being broadly compilable on a variety of platforms and compilers. The best way to respect this design decision is to keep sticking with things that will compile on any modern C compiler. I think we can use C11 for that purpose, although if we can stick to an older subset then that's fine too. But I don't think we should bend over backwards to support ancient compilers.

[benjub]

I tend to agree with @digama0, without knowing the specifics. It would be nice if metamath.c were compilable with the certified compiler CompCert (https://compcert.org/). Its manual says that it currently handles all of C99 except switch statements, variable-length arrays, and longjmp/setjmp (see Section 1.4.2 of https://compcert.org/man/manual.pdf; it allows the C11 features: anonymous structures and unions, _Alignof, _Alignas, but it may be safer to avoid them). I guess to maximize the portability, also avoid the "optional features" of C11. Maybe avoid K&R function definitions, which may be removed in C2x.

[digama0]

It turns out that the code currently does not compile with -std=c89 (aka "ANSI C"); the type ssize_t does not exist, and neither does vsnprintf(). According to https://stackoverflow.com/questions/52537188/format-strings-safely-when-vsnprintf-is-not-available , it looks like vsnprintf is actually a pretty important function, and we should not work around it, so I think upgrading to C99 is forced. (I for one will be happy to see all those /* */ comments replaced by // comments, which is an affordance of C99.)

[wlammen]

There is yet another reason to upgrade: cppreference has discontinued support for versions before C99 https://en.cppreference.com/w/c

[wlammen]

I propose to update to the latest C version broadly available. If compcert is included, this would be C11.

CompCert is certainly an interesting project. If I understand right, it is aimed at embedded systems. Such systems indeed have severe problems, especially if programs are run concurrently. This is not the case with metamath. If you are on the paranoid side, you may turn off all optimizations on a wide-spread C compiler to achieve similar results. The reason is that the wide-spread use statistically iron out all bugs initially present. Only the theorem verification code really needs extra scrutiny, not the user interface related code. I wonder whether one should create a separate program just containing core routines, and just able to verify a complete .mm file.

Note that extra risks like flawed system libraries and hardware failures cannot be eliminated by a highly verified compiler.

[digama0]

Having looked at the code some more, it's not really as portable as I thought at first. It has quite a few preprocessor directives for things like __STDC__ or __WATCOMC__. Of course, if we wanted to compile with CompCert we could just have one more set of preprocessor directives for whatever oddities it has, but that's not exactly ideal portability. In particular, the issues with compiling in a compiler like CompCert are much more likely to be in the contents of the standard library and/or IO rather than core C language features.

[benjub]

It is mentioned that CompCert has applications, among others, to embedded systems, but for us, I think the key point is that it is formally verified, that is, there is "a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program" (https://compcert.org/index.html).

After considering https://compcert.org/compcert-C.html, https://en.wikipedia.org/wiki/C11_%28C_standard_revision%29, https://en.wikipedia.org/wiki/C2x, is it possible to have metamath.c conform to the following subset of C11: C11 with the following exceptions:

• switch statements should be structured as in MISRA-C, that is, no "Duff's device" (this looks to be the case for the single switch statement in the file metamath.c; I haven't checked the other files);
• no variable-length arrays
• no longjmp/setjmp
• no "C11 optional features" (see https://en.wikipedia.org/wiki/C11_%28C_standard_revision%29#Optional_features)
• no K&R function definitions (they may be removed in C2x)

I hope this question makes sense (this is not my strong suit), and thanks @wlammen for all this work.