Open Source Contributions

I love helping improving this excellent world.

Contributing to opensource projects is a part of my life. This is also an effective way to learn programming languages that I am not familiar with.

That does not mean I do not submit typo-fixing pull requests. Instead, I usually submit pull requests like that, but I do not call this “contributions” and I do not list them here as well.

There are 76 contributions listed here in total.

Overview

Repo	Language	Status
arend	Java
intellij-arend	Kotlin
hstacks	Arend
arend	Java
intellij-arend	Kotlin
arend	Java
intellij-arend	Kotlin
arend	Java
intellij-arend	Kotlin
arend-lib	Arend
arend	Java
agda	Haskell, JavaScript
arend	Java
arend-lib	Arend
arend	Java
miniagda	Happy
intellij-arend	Kotlin
arend	Gradle Kotlin DSL
intellij-arend	Java
arend	Java
arend	Java
arend	Java
arend	Java
arend	Groovy
arend-lib	Arend
intellij-arend	Kotlin
intellij-arend	Kotlin
arend	Java
arend	Java
intellij-arend	Kotlin
mirai	Kotlin
arend	Java
intellij-arend	Kotlin
intellij-arend	Kotlin
arend-lib	Arend
arend	Java
arend	Java, Kotlin
arend	Java
linguist	tmLanguage
rust-analyzer	Rust
rust-analyzer	Rust
TeXiFy-IDEA	Kotlin	$label=$
TeXiFy-IDEA	Kotlin	$label=$
intellij-rust	Kotlin
protobuf-build	Rust
intellij-rust	Kotlin
katex	JavaScript
raft-rs	Rust
shields	JavaScript
intellij-haskell	Scala
intellij-haskell	Scala
cubical	Agda
cubical	Agda
cubical	Agda
kvproto	Rust
intellij-haskell	Scala
protobuf-build	Rust
grpc-rs	Rust
grpc-rs	Rust
intellij-haskell	Scala
intellij-haskell	Scala
intellij-haskell	Scala
agda	Haskell
agda	Haskell
agda	Haskell
imgui	C++
intellij-emmylua	Groovy, Kotlin
djinni	Java
imgui	C++
intellij-solidity	Kotlin
intellij-sdk-docs	Markdown
intellij-sdk-docs	Markdown
shields	JavaScript
llvmsharp	C#
a8translate	Java, Kotlin
tk	Ruby

ruby/tk#8

pull request in Ruby.

Backport request
A StackOverflow question
An abandoned bug report
Fixed a fatal bug, provided a monkey patch solution for the StackOverflow asker

pingerone/a8translate#1

pull request in Java, Kotlin.

The JetBrains IDE Plugin
The original JetBrains IDE Plugin
Add icon, refactor using Kotlin, add local caching and case insensitiveness

microsoft/llvmsharp#58

pull request in C#.

The project doesn't work on Travis CI since Sep 2, 2015
Migrate sample projects according to the newest LLVMSharp API and .Net Core 2.0
Fix Travis CI deployment

badges/shields#1164

pull request in JavaScript.

A related issue
Added a new badge (with corresponding tests): JetBrains Plugin version

jetbrains/intellij-sdk-docs#75

pull request in Markdown.

Created instructions for SdkType, tell plugin developers how to create custom “SDK”

jetbrains/intellij-sdk-docs#87

pull request in Markdown.

Improve SDK descriptions,
add Gradle Kotlin DSL introductions,
migrate some https://-based links to upsource:///

intellij-solidity/intellij-solidity#69

pull request in Kotlin.

A related issue
Fixed compilation errors under IDEA 2018.1,
migrate toolchain versions,
support "constructor" syntax,
added corresponding parser unit test

ocornut/imgui#1827

pull request in C++.

imgui Java binding
Make subsequent window creation possible

dropbox/djinni#363

pull request in Java.

Fix IntelliJ IDEA plugin compatibility,
Add brace matcher and highlightings for keywords

emmylua/intellij-emmylua#181

pull request in Groovy, Kotlin.

Fix build.gradle non-Windows compatibility,
Add bug reporter

ocornut/imgui#2088

pull request in C++.

Remove unnecesasry device invalidation and creation

agda/agda#3313

pull request in Haskell.

Related issue:
Implemented a feature request about HTML-backend of Agda, by introducing a new command-line flag and modifying the code generation process

agda/agda#3367

pull request in Haskell.

Related issue:
Support automatically determine output file extension by adding a command line option and modify the internal AST representation

agda/agda#3384

pull request in Haskell.

Related issue:
Update code generation for reStructuredText backend by wrapping all HTML contents inside a raw directive

rikvdkleij/intellij-haskell#330

pull request in Scala.

Related issue comment
Add syntax highlighting for soft keywords (contextual keywords) by adding an annotator

rikvdkleij/intellij-haskell#331

pull request in Scala.

Add live template contexts and some default live templates for pragmas and global declarations

rikvdkleij/intellij-haskell#334

pull request in Scala.

Related issue:
Improve pragma, function name highlighting by improving the annotator added in my previous PR, improve color settings page, move configuration section

pingcap/grpc-rs#238

pull request in Rust.

Eliminate twice memory copies when sending data, achieving zero-copy

pingcap/grpc-rs#222

pull request in Rust.

Reduce one memory copy when receiving data, achieving zero-copy

tikv/protobuf-build#2

pull request in Rust.

Support suppressing the generation of certain functions

rikvdkleij/intellij-haskell#387

pull request in Scala.

Fixed issue:
Implement a brand new pragma parser, fixed a bunch of issues

pingcap/kvproto#358

pull request in Rust.

Rewrite a shell script with rust codes (which is type safe and faster)

agda/cubical#57

pull request in Agda.

Add coinductive natural number and its properties (like infinity plus one is still infinity, bisimulation on coinductive naturals and coinductive proof principle)

agda/cubical#27

pull request in Agda.

Added basic operations (suc, pred) of higher-inductively defined integer and an equality relation on it

agda/cubical#32

pull request in Agda.

Added basic operations (even, odd) of coinductive infinite stream and proved an equality relation on it

rikvdkleij/intellij-haskell#349

pull request in Scala.

Support alex files (Haskell lexer generator), add completion, rename adn goto definition for alex lexer rules

rikvdkleij/intellij-haskell#358

pull request in Scala.

Support language injection for String literals

badges/shields#3295

pull request in JavaScript.

Enhance status badge for PRs in GithubIssueDetail by showing “merged” and “rejected” as detail for pull requeste

pingcap/raft-rs#201

pull request in Rust.

Replace the Protobuf library “rust-protobuf” with “prost”

katex/katex#1953

pull request in JavaScript.

Added support for double-square curly braces, using LaTeX command \lBrace and \rBrace

intellij-rust/intellij-rust#3745

pull request in Kotlin.

Added support for code folding for macro_rules! definitions, macro definitions and macro clauses

tikv/protobuf-build#7

pull request in Rust.

Support optionally generate protobuf wrappers

intellij-rust/intellij-rust#3759

pull request in Kotlin.

Support folding the r# prefix in raw-identifiers

Hannah-Sten/TeXiFy-IDEA#935

$label=$ pull request in Kotlin.

Some bug fixes, reduce nullability assertions

Hannah-Sten/TeXiFy-IDEA#932

$label=$ pull request in Kotlin.

Added some { pin=1 } or { pin=2 } to proper BNF rules to improve parsing performance and fault tolerance.

rust-analyzer/rust-analyzer#1924

pull request in Rust.

A related issue
Support resolution and completion for Self type reference in enums, traits and unions.

rust-analyzer/rust-analyzer#2474

pull request in Rust.

Address a FIXME, prepare for local items resolution.

github/linguist#4777

pull request in tmLanguage.

Support Arend language’s syntax highlighting on GitHub.

jetbrains/arend#110

pull request in Java.

Add infrastructure for accessing corresponded subexpression in isomorphic concrete and core terms.

jetbrains/arend#112

pull request in Java, Kotlin.

Handle version comparison properly & unify code generation.

jetbrains/arend#133

pull request in Java.

A related issue
Fix the bug where projecting the zero-th element of a sigma inhabitant.

jetbrains/arend-lib#9

pull request in Arend.

Define Torus, prove its equivalence to two 1-spheres, and prove Omega Torus is equivalent to two integers.

jetbrains/intellij-arend#97

pull request in Kotlin.

Add action to show the type of a selected expression.

jetbrains/intellij-arend#98

pull request in Kotlin.

Add option to control the pretty-printing options in the “show expression type” action.

jetbrains/arend#146

pull request in Java.

Take binding names into account when showing type if expressions, say, show the type of bindings if a binding is selected.

mamoe/mirai#85

pull request in Kotlin.

Replace a hand-written list class’ cliche operations with a single serious asSequence and invocations to its utilities.

jetbrains/intellij-arend#120

pull request in Kotlin.

A related issue
Support schema-based completion & validation for arend.yaml, support path-based completion.

jetbrains/arend#152

pull request in Java.

A continued work of 110, but for definitions.

jetbrains/arend#155

pull request in Java.

A continued work of 152, but for instance declarations, pattern matching clauses and \cowith declarations.

jetbrains/intellij-arend#134

pull request in Kotlin.

Normalize the selected expression in background.

jetbrains/intellij-arend#137

pull request in Kotlin.

A related issue
Added intention action that replaces an expression with its normal form.

jetbrains/arend-lib#13

pull request in Arend.

Define Set-Truncation and its eliminators (A lemma in HoTT Book). Closed because it’s actually a specialization of an existing construct.

jetbrains/arend#162

pull request in Groovy.

Make the GenerateVersionTask gradle task incremental.

jetbrains/arend#158

pull request in Java.

A continued work of 155, but for case-expressions.

jetbrains/arend#166

pull request in Java.

A related issue
A continued work of 158, but for let-clauses’ result type when they’re pi-type.

jetbrains/arend#167

pull request in Java.

A related issue
A continued work of 166, but for class-call expressions.

jetbrains/arend#175

pull request in Java.

A continued work of 167, but added error messages when the action failed.

jetbrains/intellij-arend#156

pull request in Java.

Related issues:
Add a button that controls whether to normalize the pop-up expression or not.

jetbrains/arend#177

pull request in Gradle Kotlin DSL.

Related issues:
Modularize Arend. This also introduce extra flexibility in the future. Say, when we want a literate programming mode/documentation generator/linting tool for Arend, we can add ‘em as another gradle subproject.

jetbrains/intellij-arend#157

pull request in Kotlin.

Use gradle composite build to connect to modularized Arend.

andreasabel/miniagda#7

pull request in Happy.

Update docs to demonstrate latest Cabal commands, remove unused rules during parser generation.

jetbrains/arend#199

pull request in Java.

Related issues:
Implement the partially applied syntax.

jetbrains/arend-lib#17

pull request in Arend.

Related issue in Arend:
Use the partially applied syntax in the standard library extensively.

jetbrains/arend#204

pull request in Java.

Implement the partially applied syntax for \case \elim functions. This is more complicated than other partially applied syntaxes.

agda/agda#4535

pull request in Haskell, JavaScript.

Prior discussion: https://twitter.com/i/status/1241631880388194304
Implement a feature from Haddock that highlights all occurrences of some symbols. It’s the first possible “find usages” in Agda.

jetbrains/arend#210

pull request in Java.

Related issue in Arend:
Implement a general abstraction for REPLs and provide two console implementations. One is a plain REPL like python’s, one has jline3-based completion.

jetbrains/arend-lib#19

pull request in Arend.

Define BinNat and its properties. These proofs are ported from its original cubicaltt version.

jetbrains/intellij-arend#188

pull request in Kotlin.

Related pull request in Arend:
Implement in-IDE REPL for Arend.

jetbrains/arend#232

pull request in Java.

Related issue:
Implement string literals in Arend.

jetbrains/intellij-arend#207

pull request in Kotlin.

Related issue in Arend:
Implement string literals in intellij-arend.

jetbrains/arend#254

pull request in Java.

Related issue:
Implement “definable metas” in Arend (hygiene macros).

jetbrains/intellij-arend#223

pull request in Kotlin.

Related issue in Arend:
Implement “definable metas” in intellij-arend (hygiene macros).

jetbrains/arend#262

pull request in Java.

Related issue:
Implement API for desugaring numbers in pattern matchings.

tonyxty/hstacks#1

pull request in Arend.

Help proving transitivity of Yoneda embedding.

jetbrains/intellij-arend#236

pull request in Kotlin.

Related issue:
Improve TypedHandler to avoid duplicating the closing braces }.

jetbrains/arend#271

pull request in Java.

Related issue in intellij-arend:
Implement REPL actions to modify pretty printing flags, and use YAML instead of properties to store REPL configurations.