Helping with documentation

Graph controls: Use mouse to pan, use scroll or two fingers to zoom in/out. Click on nodes to navigate to their GitHub entry.

Eventually we want to turn all the nodes in this graph green by adding documentation. To help follow the steps below!

Steps to help with documentation

This whole process can be done without downloading Lean, but having it installed provides helpful tools.

Phase 1: Get the Code

  1. Fork the PhysLean GitHub repository. (Copy the master branch only)
  2. Clone your forked repository to your local machine. (Optional, you can also edit directly on GitHub)
There are many good tutorials on the GitHub steps involved in these instructions, see e.g. Youtube video as an example of some of the GitHub steps involved here.

Phase 2: Choose a File to Document

  1. Use the graph above to identify an undocumented file (a red node) where you think you could help.
  2. In your local copy of PhysLean, open the file ./scripts/MetaPrograms/module_doc_no_lint.txt.
  3. Remove the line corresponding to the file you want to document.
  4. Navigate to the file you want to document.

Phase 3: Write the Documentation

You can write the documentation manually or use a helper script if you have Lean installed. See any of the green nodes in the graph for examples of good documentation.

Option A: Without Lean

Edit the .lean file you chose and add the following sections:

  1. Module Title: Add a title heading at the top of the file, starting with # .
  2. Overview: Add an ## i. Overview section after the title, explaining the physical content of the module.
  3. Key Results: Add a ## ii. Key results section. This should list the key definitions, theorems, and lemmas with brief explanations.
  4. Table of Contents: Add a ## iii. Table of contents section. This can be left blank and will be filled in automatically later.
  5. References: Add a ## iv. References section for any relevant literature.
  6. Structure the Code: Organize the rest of the file with section and subsection headings (e.g., ## A., ### A.1., #### A.1.2).

Option B: With Lean

If you have Lean installed, a script can help you structure the documentation.

  1. Run lake exe module_doc_lint in your terminal.
  2. Follow the interactive steps, using existing documented files as a guide.

Phase 4: Submit Your Changes

  1. Commit your changes to your forked repository.
  2. Create a pull request to the main PhysLean repository for review.