File structure for large auto-generated merges

Stream: Equational

[Nicholas Carlini]

I am going to try and get https://github.com/teorth/equational_theories/pull/23 into a mergable state in a few hours.

Here's my proposal for how to format these large collections of auto-generated proofs. But I have no idea what I'm doing so someone please let me know if this makes sense as a plan for how future ones might want to work, too.

1. I'll make a new subdirectory for the "proof style" I'm using. This one will be called "SimpleRewrites"
2. Then, I'll make "SimpleRewrites/theorems" and put all of the theorems there.
3. I'll also make a "SimpleRewrites.lean" that references all of the theorems.
4. I'll finally make "SimpleRewrites/src" and put the source that auto-generates the theorems there
5. In "SimpleRewrites/README.md" I'll document how to run the script that generated these contradictions.
6. In .gitattributes add equational_theories/SimpleRewrites.lean linguist-generated

Does this make sense as a general format for auto-generated theorems? It would be nice to have a thought-through example for how to contribute large collections of theorems so that future people can pattern-match on a PR without having to figure out how to best lay things out themselves.

[Joachim Breitner]

This makes good sense. My https://github.com/teorth/equational_theories/pull/19 mostly follows this scheme as well. Also mark the generated files as generated in .gitattributes, and leave a comment on the files saying that they are generated and where to read more.

The readme can be in the parent directory.

[Nicholas Carlini]

Added this to my proposal.

[Terence Tao]

This looks good to me. If you go ahead and implement this, you can also update CONTRIBUTING.md to reflect this workflow.

[Nicholas Carlini]

Wrote some text here; feel free to suggest anything else https://github.com/teorth/equational_theories/pull/68/

[Shreyas Srinivas]

Looks good. But does CI actually build this stuff?

[Shreyas Srinivas]

The default build process builds everything from the toplevel file to its dependencies recursively.

[Shreyas Srinivas]

CC : @Joachim Breitner

[Joachim Breitner]

Correct, you should also import the main file of your subdirectory in the top level library file

[Nicholas Carlini]

Yes this should also be included in this file. I did do it for the simple rewrites (https://github.com/teorth/equational_theories/blob/583407a78f918f62e5b1aab4d0fc23bf4c861a37/equational_theories.lean#L3) but forgot to put it in the docs. If someone wants to add that before I get to it feel free I might be a while

[Shreyas Srinivas]

I'll add it. It is quicker on my end

[Shreyas Srinivas]

Ideally you want to add a Generated.lean file and import that in equational_theories.lean

[Shreyas Srinivas]

And then add the generated imports to Generated.lean

[Nicholas Carlini]

That makes sense too

[Shreyas Srinivas]

I'll fix this

[Shreyas Srinivas]

And make sure SimpleRewrites is added. Separately I will fix the contributing docs once this PR is done

[Shreyas Srinivas]

https://github.com/teorth/equational_theories/pull/73