Merge branch 'main' of https://github.com/teorth/equational_theories

0art0 · Oct 8, 2024 · fd25f3f · fd25f3f
2 parents 7ff497d + c3d8575
commit fd25f3f
Show file tree

Hide file tree

Showing 111 changed files with 18,043 additions and 423 deletions.
diff --git a/.github/ISSUE_TEMPLATE/bug_report.md b/.github/ISSUE_TEMPLATE/bug_report.md
@@ -0,0 +1,38 @@
+---
+name: Bug report
+about: Create a report to help us improve
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+**Describe the bug**
+A clear and concise description of what the bug is.
+
+**To Reproduce**
+Steps to reproduce the behavior:
+1. Go to '...'
+2. Click on '....'
+3. Scroll down to '....'
+4. See error
+
+**Expected behavior**
+A clear and concise description of what you expected to happen.
+
+**Screenshots**
+If applicable, add screenshots to help explain your problem.
+
+**Desktop (please complete the following information):**
+ - OS: [e.g. iOS]
+ - Browser [e.g. chrome, safari]
+ - Version [e.g. 22]
+
+**Smartphone (please complete the following information):**
+ - Device: [e.g. iPhone6]
+ - OS: [e.g. iOS8.1]
+ - Browser [e.g. stock browser, safari]
+ - Version [e.g. 22]
+
+**Additional context**
+Add any other context about the problem here.
diff --git a/.github/ISSUE_TEMPLATE/feature_request.md b/.github/ISSUE_TEMPLATE/feature_request.md
@@ -0,0 +1,20 @@
+---
+name: Feature request
+about: Suggest an idea for this project
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+**Is your feature request related to a problem? Please describe.**
+A clear and concise description of what the problem is. Ex. I'm always frustrated when [...]
+
+**Describe the solution you'd like**
+A clear and concise description of what you want to happen.
+
+**Describe alternatives you've considered**
+A clear and concise description of any alternative solutions or features you've considered.
+
+**Additional context**
+Add any other context or screenshots about the feature request here.
diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
@@ -0,0 +1,79 @@
+# Contributing to the Equational Theories Project
+
+Thank you for your interest in contributing to the Equational Theories Project! We welcome contributions from all sources: human-generated contributions from either professional mathematicians or interested members of the public, as well as computer-generated contributions from programs in various languages, automated theorem provers, or modern AI tools. (In fact, one of the main goals of this project is to learn how such a diverse pool of contributions can effectively be combined with each other to advance a common objective.)
+
+This guide provides detailed instructions on how to effectively and efficiently contribute to the project.
+
+## Project Coordination
+
+The project is managed using a [GitHub project dashboard](https://github.com/users/teorth/projects/1), which tracks tasks through various stages, from assignment to completion.
+
+## How to Contribute
+
+Contributions to the project are made through GitHub pull requests (PRs) that correspond to specific tasks outlined in the project's issues.
+The following instructions detail the process for claiming and completing tasks.
+
+### 1. Task Identification
+
+- Tasks are posted as GitHub issues and can be found in the `Unclaimed Outstanding Tasks` column of the project dashboard.
+- Each issue represents a specific task to be completed. The issue title and description contain relevant details and requirements.
+
+### 2. Claiming a Task
+
+- To claim a task, comment the single word `claim` on the relevant GitHub issue.
+- If no other user is assigned, you will automatically be assigned to the task, and the issue will move to the `Claimed Tasks` column.
+- You may only claim one task at a time. If you decide not to work on a task after claiming it, comment the single word `disclaim` on the issue. This will unassign you and return the issue to the `Unclaimed Outstanding Tasks` column, making it available for others to claim.
+
+### 3. Working on the Task
+
+Once you are assigned to an issue, begin working on the corresponding task. You should create a new branch from the `main` branch to develop your solution.
+
+> [!WARNING]
+> Before pushing any changes, you have the following options:
+>
+> - You might want to install the git pre-push hook by running:
+>
+>   ```bash
+>   scripts/install_pre-push.sh
+>   ```
+>   This will automatically run checks before every push, reducing the risk of CI check failures.
+>
+> - You can manually run the following script before pushing, reducing the risk of CI check failures:
+>
+>   ```bash
+>   scripts/run_before_push.sh
+>   ```
+>   This requires manual execution and won't stop the push if skipped.
+>
+> - You may push your changes without any safeguards, increasing the risk of CI check failures.
+
+### 4. Submitting a Pull Request
+
+- When you are ready to submit your solution, create a PR from your working branch to the project’s `main` branch.
+- After submitting the PR, comment the single phrase `propose PR #PR_NUMBER` on the original issue. This links your PR to the task, and the task will move to the `In Progress` column on the dashboard.
+- A task can only move to `In Progress` if it has been claimed by the user proposing the PR.
+
+### 5. Withdrawing or Updating a PR
+
+- If you need to withdraw your PR, comment the single phrase `withdraw PR #PR_NUMBER` on the issue. The task will return to the `Claimed Tasks` column, but you will remain assigned to the issue.
+- To submit an updated PR after withdrawal, comment the single phrase `propose PR #NEW_PR_NUMBER` following the same process outlined in step 4.
+
+### 6. Review Process
+
+- After finishing the task and ensuring your PR is ready for review, comment the single word `awaiting-review` on the PR. This will add the `awaiting-review` label to your PR and move the task from `In Progress` to the `PRs in Review` column of the dashboard.
+- The project maintainers will review the PR. They may request changes, approve the PR, or provide feedback.
+
+### 7. Task Completion
+
+- Once the PR is approved and merged, the task will automatically move to the `Completed` column.
+- If further adjustments are needed after merging, a new issue will be created to track additional work.
+
+### Additional Guidelines and Notes
+
+1. Please adhere to the issue claiming process. If an issue is already assigned to another contributor, refrain from working on it without prior communication with the current claimant. This ensures a collaborative and respectful workflow that values each contributor’s efforts.
+2. Be aware that this contribution process is still in an experimental phase. As a result, occasional issues and inefficiencies may arise. We are committed to continuously refining the process, and your constructive feedback is highly appreciated. You can share your thoughts and suggestions on the [Lean Zulip chat channel](https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/).
+3. Until the integration of sufficient CI automation, the management of the project dashboard is handled manually by the maintainers. We ask for your patience and understanding as we work to keep the process running smoothly.
+
+## Discussion
+
+The main discussion will be held in this [Lean Zulip channel](https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/).  Some secondary discussion will also be held at [this blog post](https://terrytao.wordpress.com/2024/09/25/a-pilot-project-in-universal-algebra-to-explore-new-ways-to-collaborate-and-use-machine-assistance/).
diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
@@ -149,6 +149,11 @@ jobs:
           ruby-version: "3.0"  # Specify Ruby version
           bundler-cache: true  # Enable caching for bundler
 
+      - name: Generate home_page/graphiti/graph.json
+        run: |
+          ~/.elan/bin/lake exe extract_implications --json > /tmp/implications.json
+          ruby scripts/generate_graphiti_data.rb /tmp/implications.json > home_page/graphiti/graph.json
+
       - name: Build website using Jekyll
         if: github.event_name == 'push' && env.HOME_PAGE_EXISTS == 'true'
         working-directory: home_page