.gitignore and best practices

[mountain]

When init a project, it is nice to generate .gitignore file or append several lines to an existed .gitignore file.

Files to ignore:

• database/*.mm
• database/*.zip
• other temporary files

[tirix]

Why would you ignore *.mm files? Wouldn't those be the ones to commit?
I suppose you mean the *.mmp files.

[mountain]

Oh, I had not go through the whole process so far, I may be wrong.

In my understanding, the database is read only in developing stage?
you need convert yourproof.mmp to a patch? and then combine the patch to the original code base?

[tirix]

See for example this PR: this is directly a change to set.mm (like most PR in the set.mm repository).

It's true that MMJ2 does not modify the source .mm database, so usually the process follows these steps:

• manually modify the source .mm database to add your definitions, and/or incomplete theorems, in any text editor,
• use MMJ2 or another tool to write the proof(s), resulting in the proof(s) in compressed format
• manually paste the proof(s) back into the source .mm database, again, in any text editor.

One can then publish the modified .mm database on GitHub.

[tirix]

PS. my Eclipse plugin (video here) works the same way, it's just that in that case Eclipse is used both for editing the source MM file and for the MMP proof assistant.

[mountain]

Thanks, let me check...

If any step can be simplified or automated, I will gradually combine it into this toolkit.

[mountain]

@tirix the Eclipse Plugin is cool! I also have a question about complex proofs.

If a new math concept was introduced, just like Quadratic form or others, we need introduce new constant by $c and new class and construction by $a

• $c SomeThing $.
• $csth $a class SomeThing $.
• df-smth $a |- SomeThing = ... $.

If my understanding is not wrong, the above three lines can not include in a *.mmp file, the PA give me error message.

So two solutions here:

1. modify database file in database folder directly?
2. introduce a new .mm file in proofs folder which include the database by $[ DBPATH ]$, and then PA load this .mm file to start your development.

Is my understanding correct? If it is correct, what is the best practice in metamath community?

[mountain]

More comments about proofs, consensus and development

For me, the math knowledge and its development are immutable and incremental by its very nature, but in real practice, a lot of information was lost. Newton's fluxon method relied on geometry intuitions, many geometry techniques in the Principia which is not the standard method nowadays. But no one can easily deny the validity of Newton's method. The development is history itself, it is immutable, and math is something true everlast, so all the math proofs by human is an immutable true structure.

Only when we organize these knowledge and pass them generation by generation, we need compress all these proofs by giving a solid ground and a well-ordered way to express them. In this circumstance, revision and consensus are introduced.

And I think in metamath development, similar things happens.

[mountain]

@tirix I re-read your comments above, and understand it now, you had already covered my new questions.