init

.github/CODE_OF_CONDUCT.md

@@ -0,0 +1,134 @@
+# Contributor Covenant Code of Conduct
+
+## Our Pledge
+
+We as members, contributors, and leaders pledge to make participation in our
+community a harassment-free experience for everyone, regardless of age, body
+size, visible or invisible disability, ethnicity, sex characteristics, gender
+identity and expression, level of experience, education, socio-economic status,
+nationality, personal appearance, race, caste, color, religion, or sexual identity
+and orientation.
+
+We pledge to act and interact in ways that contribute to an open, welcoming,
+diverse, inclusive, and healthy community.
+
+## Our Standards
+
+Examples of behavior that contributes to a positive environment for our
+community include:
+
+* Demonstrating empathy and kindness toward other people
+* Being respectful of differing opinions, viewpoints, and experiences
+* Giving and gracefully accepting constructive feedback
+* Accepting responsibility and apologizing to those affected by our mistakes,
+  and learning from the experience
+* Focusing on what is best not just for us as individuals, but for the
+  overall community
+
+Examples of unacceptable behavior include:
+
+* The use of sexualized language or imagery, and sexual attention or
+  advances of any kind
+* Trolling, insulting or derogatory comments, and personal or political attacks
+* Public or private harassment
+* Publishing others' private information, such as a physical or email
+  address, without their explicit permission
+* Other conduct which could reasonably be considered inappropriate in a
+  professional setting
+
+## Enforcement Responsibilities
+
+Community leaders are responsible for clarifying and enforcing our standards of
+acceptable behavior and will take appropriate and fair corrective action in
+response to any behavior that they deem inappropriate, threatening, offensive,
+or harmful.
+
+Community leaders have the right and responsibility to remove, edit, or reject
+comments, commits, code, wiki edits, issues, and other contributions that are
+not aligned to this Code of Conduct, and will communicate reasons for moderation
+decisions when appropriate.
+
+## Scope
+
+This Code of Conduct applies within all community spaces, and also applies when
+an individual is officially representing the community in public spaces.
+Examples of representing our community include using an official e-mail address,
+posting via an official social media account, or acting as an appointed
+representative at an online or offline event.
+
+## Enforcement
+
+Instances of abusive, harassing, or otherwise unacceptable behavior may be
+reported to the community leaders responsible for enforcement at
+[xy.r@outlook.com](mailto:xy.r@outlook.com), 
+[imkiva@islovely.icu](mailto:imkiva@islovely.icu) or
+[ice1000kotlin@foxmail.com](mailto:ice1000kotlin@foxmail.com).
+All complaints will be reviewed and investigated promptly and fairly.
+
+All community leaders are obligated to respect the privacy and security of the
+reporter of any incident.
+
+## Enforcement Guidelines
+
+Community leaders will follow these Community Impact Guidelines in determining
+the consequences for any action they deem in violation of this Code of Conduct:
+
+### 1. Correction
+
+**Community Impact**: Use of inappropriate language or other behavior deemed
+unprofessional or unwelcome in the community.
+
+**Consequence**: A private, written warning from community leaders, providing
+clarity around the nature of the violation and an explanation of why the
+behavior was inappropriate. A public apology may be requested.
+
+### 2. Warning
+
+**Community Impact**: A violation through a single incident or series
+of actions.
+
+**Consequence**: A warning with consequences for continued behavior. No
+interaction with the people involved, including unsolicited interaction with
+those enforcing the Code of Conduct, for a specified period of time. This
+includes avoiding interactions in community spaces as well as external channels
+like social media. Violating these terms may lead to a temporary or
+permanent ban.
+
+### 3. Temporary Ban
+
+**Community Impact**: A serious violation of community standards, including
+sustained inappropriate behavior.
+
+**Consequence**: A temporary ban from any sort of interaction or public
+communication with the community for a specified period of time. No public or
+private interaction with the people involved, including unsolicited interaction
+with those enforcing the Code of Conduct, is allowed during this period.
+Violating these terms may lead to a permanent ban.
+
+### 4. Permanent Ban
+
+**Community Impact**: Demonstrating a pattern of violation of community
+standards, including sustained inappropriate behavior,  harassment of an
+individual, or aggression toward or disparagement of classes of individuals.
+
+**Consequence**: A permanent ban from any sort of public interaction within
+the community.
+
+## Attribution
+
+This Code of Conduct is adapted from the [Contributor Covenant][homepage],
+version 2.1, available at
+[https://www.contributor-covenant.org/version/2/1/code_of_conduct.html][v2.1].
+
+Community Impact Guidelines were inspired by
+[Mozilla's code of conduct enforcement ladder][Mozilla CoC].
+
+For answers to common questions about this code of conduct, see the FAQ at
+[https://www.contributor-covenant.org/faq][FAQ]. Translations are available
+at [https://www.contributor-covenant.org/translations][translations].
+
+[homepage]: https://www.contributor-covenant.org
+[v2.1]: https://www.contributor-covenant.org/version/2/1/code_of_conduct.html
+[Mozilla CoC]: https://github.com/mozilla/diversity
+[FAQ]: https://www.contributor-covenant.org/faq
+[translations]: https://www.contributor-covenant.org/translations

.github/CONTRIBUTING.md

@@ -0,0 +1,79 @@
+# Contribution guidelines
+
+All contributors should read and understand this guideline before their contribution. Maintainers will reject any contribution not following this guideline as necessary.
+
+This guideline is agreed upon by all maintainers.
+
+## Outside contributors
+
+You are encouraged to:
+
+- Report any bugs encountered in using Aya.
+  - Please include a minimal reproduction and the commit hash you are using to run the reproduction.
+  - Please include the error report.
+- Ask any questions about Aya in the discussion area.
+
+These are currently not accepted:
+
+- PRs adding new language features without prior consent,
+  because we have our own plans and accepting a PR means maintaining it.
+  We refer to [Lean FAQ](https://leanprover.github.io/lean4/doc/faq.html)
+  "Are pull requests welcome?" to explain the rationale.
+- Feature proposals -- but please do share your ideas!
+  We do not guarantee anything yet, so suggested features
+  probably won't be considered.
+
+Your responsibility:
+
+- Unethical behaviors not adhering to [the Code of Conduct](CODE_OF_CONDUCT.md) is not allowed and will be taken proper action upon by maintainers.
+
+If you are interested in contributing more and becoming a member of the organization, please contact the maintainers.
+
+## Members of the organization
+
+You are encouraged to:
+
+- Open issues about the feature planning, implementation and other aspects of the Aya prover.
+- Open bug fixing PRs.
+- Open feature adding PRs when the addition of the feature is already agreed on by the community.
+
+You are not allowed to:
+
+- Push to the main branch, except for a few exceptions.
+  Merging your PR into the main branch is wholly handled by the @bors bot.
+- Force-push to the main branch. This is strictly prohibited. No exception.
+- Perform other destructive and/or irreversible actions on the organization or repository settings without the maintainers' consent.
+
+Your responsibility:
+
+- PRs should be up to the contribution standard.
+  - Your code should be properly formatted and linted.
+  - Commit messages should follow the format `KEYWORD: detailed message ....`.
+  - Please do not include overly fragmented commits; amending you commit and force-pushing to your PR branch is accepted and encouraged.
+- Please be collaborative and open to others' comments and review.
+  - When submitting your PR and issues, make sure to include proper tags and milestones (if applicable).
+  - Please request review from relevant members and at least one maintainer for your PR.
+- Base your PRs on latest main branch if possible and make sure you look at the CI results.
+  Make sure you understand the purpose of using CI and address the problems it reports.
+- Include test fixtures if your change is beyond a refactoring.
+- Other unethical behaviors not adhering to [the Code of Conduct](CODE_OF_CONDUCT.md) is not allowed and will be taken proper action upon by maintainers.
+
+## Maintainers
+
+Maintainers are the collaborators that are either sponsored by PLCT or declared to be a maintainer by other maintainers' consensus.
+
+Current maintainers: @ice1000, @imkiva, @Glavo, @re-xyr
+
+Maintainers should:
+
+- Continuously contribute to Aya's prosperity.
+- Be open-minded and willing to accept and/or discuss different opinions.
+- Always work towards consensus.
+
+Maintainers' responsibility:
+
+- For any important decisions that may affect Aya's prospect and general development,
+  including major change in language goal, features and repository configuration,
+  _no irreversible actions should be done before **all** maintainers reach consensus on a detailed plan and collective consent of potential consequences_. (ref. #60)
+- For any important decisions or conflicts, maintainers' consensus is the final decision that cannot be rejected.
+- Maintainers have the responsibility of maintaining the community's ethics uncorrupted, per [the Code of Conduct](CODE_OF_CONDUCT.md).

.github/README.md

@@ -0,0 +1,119 @@
+[![actions]](https://github.com/aya-prover/aya-dev/actions/workflows/gradle-check.yaml)
+[![maven]][maven-repo]
+[![gitter]](https://gitter.im/aya-prover/community?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge)
+[![codecov]](https://codecov.io/gh/aya-prover/aya-dev)
+
+[**Website**](https://www.aya-prover.org) contains:
+
++ Development blogs which are written for general audience
++ [Installation](https://www.aya-prover.org/guide/install.html)
+  instructions (basically telling you what to download in [GitHub Releases])
++ [Tutorial for Haskellers](https://www.aya-prover.org/guide/haskeller-tutorial.html)
++ [Tutorial of extension types](https://www.aya-prover.org/guide/ext-types.html)
+
+Aya is under active development, so please expect bugs, usability or performance issues
+(please file issues or create threads in discussions!).
+
+## What to expect?
+
++ Dependent types, including pi-types, sigma types, indexed families, etc.
+  You could write a [type-safe interpreter][gadt].
++ Cartesian cubical type theory with generalized path types
+  similar to a "bounded" cubical subtype.
+  + Implementation prototype of De Morgan cubical: [Guest0x0].
+  + Demonstration of higher inductive types: [3-torus] (three-dimensional torus!!).
+  + Demonstration of [higher-inductive-inductive-recursive types][hiir].
++ Pattern matching with first-match semantics.
+  Checkout the [red-black tree][rbtree] (without deletion yet).
++ Overlapping and order-independent patterns. Very [useful][oop] in theorem proving.
++ A literate programming mode with inline code fragment support, inspired from Agda and [1lab].
+  You may preview the features (in Chinese)
+  [here](https://blog.imkiva.org/posts/intro-literate-aya.html).
++ Binary operators, with precedence specified by a partial ordering
+  (instead of a number like in Haskell or Agda)
+  which is useful for [equation reasoning][assoc].
++ A fairly good termination checker.
+  We adapted some code from Agda's implementation to accept
+  [more definitions][foetus] (which are rejected by, e.g. Arend).
++ Inference of type checking order. That is to say,
+  no syntax for forward-declarations is needed for [mutual recursions][mutual],
+  induction-recursion, or induction-induction.
++ See also stdlib candidates [style guide][stdlib-style]. We have a grand plan!
+
+See also [use as a library](#use-as-a-library).
+
+[GitHub Releases]: https://github.com/aya-prover/aya-dev/releases/tag/nightly-build
+[Java 21]: https://jdk.java.net/21
+[1lab]: https://1lab.dev
+
+## Contributing to Aya
+
+Since you need [Java 21] to set this project up, in case your choice
+of IDE is IntelliJ IDEA, version 2023.3 or higher is required.
+
++ Questions or concerns are welcomed in the discussion area.
+  We will try our best to answer your questions, but please be nice.
++ We welcome nitpicks on error reporting! Please let us know anything not perfect.
+  We have already implemented several user-suggested error messages.
++ Before contributing in any form, please read
+  [the contribution guideline](https://github.com/aya-prover/aya-dev/blob/master/.github/CONTRIBUTING.md) thoroughly
+  and make sure you understand your responsibilities.
++ Please follow [the Code of Conduct](https://github.com/aya-prover/aya-dev/blob/master/.github/CODE_OF_CONDUCT.md) to
+  ensure an inclusive and welcoming community atmosphere.
++ Ask [@ice1000] or simply create a ticket in the discussion to become an organization member.
+  + If you want to contribute, ask before doing anything.
+    We are reluctant to accept PRs that contradict our design goals.
+    We value your time and enthusiasm, so we don't want to close your PRs :)
+
+[@ice1000]: https://github.com/ice1000
+[actions]: https://github.com/aya-prover/aya-dev/actions/workflows/gradle-check.yaml/badge.svg
+[codecov]: https://img.shields.io/codecov/c/github/aya-prover/aya-dev?logo=codecov&logoColor=white
+[gitter]: https://img.shields.io/gitter/room/aya-prover/community?color=cyan&logo=gitter
+[maven]: https://img.shields.io/maven-central/v/org.aya-prover/base?logo=gradle
+[oop]: ../base/src/test/resources/success/common/src/Arith/Nat/Core.aya
+[gadt]: ../base/src/test/resources/success/src/TypeSafeNorm.aya
+[regularity]: ../base/src/test/resources/success/common/src/Paths.aya
+[funExt]: ../base/src/test/resources/success/common/src/Paths.aya
+[rbtree]: ../base/src/test/resources/success/common/src/Data/Tree/RedBlack/Direct.aya
+[3-torus]: ../base/src/test/resources/success/common/src/Spaces/Torus/T3.aya
+[hiir]: ../base/src/test/resources/success/common/src/TypeTheory/Thorsten.aya
+[assoc]: ../base/src/test/resources/success/src/Assoc.aya
+[foetus]: ../base/src/test/resources/success/src/FoetusLimitation.aya
+[mutual]: ../base/src/test/resources/success/src/Order.aya
+[maven-repo]: https://repo1.maven.org/maven2/org/aya-prover
+[Guest0x0]: https://github.com/ice1000/Guest0x0
+[stdlib-style]: ../base/src/test/resources/success/common
+
+## Use as a library
+
+It's indexed in [mvnrepository](https://mvnrepository.com/artifact/org.aya-prover),
+and here are some example build configurations:
+
+```xml
+<!-- Maven -->
+<dependency>
+    <groupId>org.aya-prover</groupId>
+    <artifactId>[project name]</artifactId>
+    <version>[latest version]</version>
+</dependency>
+```
+
+```groovy
+// Gradle
+implementation group: 'org.aya-prover', name: '[project name]', version: '[latest version]'
+```
+
++ `[project name]` specifies the subproject of Aya you want to use,
+  and the options are `pretty`, `base`, `cli-impl`, `parser`, etc.
+  + The type checker lives in `base` and `parser`.
+  + The generalized pretty printing framework is in `pretty`.
+  + The library system, literate mode, single-file type checker, and basic REPL are in `cli-impl`.
+  + The generalized tree builder, generalized termination checker,
+    and a bunch of other utilities (files, etc.) are in `tools`.
+  + The generalized binary operator parser, generalized mutable graph are
+    in `tools-kala` because they depend on a larger subset of the kala library.
+  + The command and argument parsing framework is in `tools-repl`.
+    It offers an implementation of jline3 parser based on Grammar-Kit and relevant facilities.
+  + The literate-markdown related infrastructure is in `tools-md`.
+    It offers commonmark extensions for literate mode of any language with a highlighter.
++ `[latest version]` is what you see on this badge ![maven].

.github/workflows/commit-check.sh

@@ -0,0 +1,24 @@
+#!/usr/bin/env bash
+
+#
+# Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+# Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+#
+
+set -eu -o pipefail
+
+git log --oneline --decorate --pretty=format:'%h:%s' origin/main.. | xargs -0 echo | while read line; do
+  IFS=':' read -r hash tag msg <<< "$line"
+  if [[ "$(echo $tag | tr -d [A-za-z0-9\#-])"x != ""x ]]; then
+    echo "In commit $hash, \`$tag\` is not a good commit tag"
+    exit 1
+  fi
+  if [[ ! "$msg" =~ ( ).+ ]]; then
+    echo "In commit $hash, commit message should have a space after \`:\` and not empty"
+    exit 2
+  fi
+  echo "Commit message of $hash is good"
+done
+
+exit 0
+

.github/workflows/commit-check.yaml

@@ -0,0 +1,16 @@
+name: commit message
+on:
+  pull_request:
+    branches: [main]
+  merge_group:
+    types: [checks_requested]
+jobs:
+  commit-check:
+    runs-on: ubuntu-20.04
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          fetch-depth: 0
+          ref: ${{ github.event.pull_request.head.sha }}
+      - name: Check git commit message
+        run: bash .github/workflows/commit-check.sh