Hacktoberfest 2026: những issue maintainer đã đánh dấu cho tháng Mười, đang mở và phù hợp người mới. Xem issue Hacktoberfest

rocq-prover/stdlib

Đăng nhập để theo dõi Xem trên GitHub

Stdlib for the Rocq Prover

rocq-prover/stdlib có thân thiện với người mới không?

Gần đây có quá ít pull request của người đóng góp bên ngoài gửi tới rocq-prover/stdlib để nói chúng được merge thường xuyên đến đâu. Hiện có 1 issue phù hợp với người mới đang mở.

Star
42
Fork
40
Issue cho người mới đang mở
1
Issue đã lập chỉ mục
88
Merge trung bình
20 giờ 23 phút
Pull request đã merge (30 ngày)
2
Ngôn ngữ chính
Rocq Prover
Giấy phép
LGPL-2.1
Lần push lên GitHub gần nhất
25/9/2026
Lập chỉ mục gần nhất
19/9/2026
Hướng dẫn đóng góp
Không có quy tắc ứng xử
Label cho người mới
Chưa lập chỉ mục label nào cho người mới

Cách đóng góp cho rocq-prover/stdlib

  1. Hãy đọc hướng dẫn đóng góp trước: nó cho biết maintainer muốn thay đổi được đề xuất, kiểm thử và review ra sao.
  2. Đóng góp của bạn sẽ được phát hành theo giấy phép LGPL-2.1 của dự án.
  3. Chọn issue phù hợp với người mới đang mở bên dưới và bình luận rằng bạn muốn làm nó trước khi bắt đầu.
Phù hợp cho người mới Tất cả
Đang mở Tất cả

Các issue có thể đã có người làm được xếp cuối danh sách. Sắp xếp tất cả theo ngày

  • Maintaining NaryFunctions
    Đang mở
    • Có gì không ổn?

    Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 25/100

    rocq-prover/stdlib#293 ·

  • deprecating List.nth in favor of List.nth_default
    Đang mở
    • Có gì không ổn?

    Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 25/100

    rocq-prover/stdlib#243 ·

  • Importing PeanoNat.Nat shadows eq definition
    Đang mở
    • Có gì không ổn?

    Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 25/100

    rocq-prover/stdlib#242 · 3 bình luận ·

  • Documentation could be automatically deployed
    Đang mở
    • Có gì không ổn?

    Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 25/100

    rocq-prover/stdlib#241 ·

  • Releasing? (Docker CI images do not support latest stdlib)
    Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100

    rocq-prover/stdlib#230 · 11 bình luận ·

  • Using dune when installing the package
    Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 42/100

    rocq-prover/stdlib#225 · 2 bình luận ·

  • Regression: Importing ZArith leads to setoid_rewrite performance degradation
    Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 42/100

    rocq-prover/stdlib#200 · 2 bình luận ·

  • same html title for all files (stdlib doc)
    Đang mở
    • Có gì không ổn?

    Độ khó 3/5 1-2 ngày Mức phù hợp với người mới 42/100

    rocq-prover/stdlib#195 · 2 bình luận ·

  • Github CI anomaly zoo
    Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 25/100

    rocq-prover/stdlib#168 · 4 bình luận ·

  • Design: connecting booleans to their meaning
    Đang mở
    • Có gì không ổn?

    Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 25/100

    rocq-prover/stdlib#165 · 1 reaction ·

  • GitHub CI queuing
    Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 25/100

    rocq-prover/stdlib#153 · 10 bình luận ·

  • Require status checks to pass before merging (for auto-merge, no policy change)
    Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 30/100

    rocq-prover/stdlib#148 · 3 bình luận ·

  • CI: is there a way to see CI-built HTML documentation for an unmerged PR?
    Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 25/100

    rocq-prover/stdlib#145 · 1 bình luận ·

  • CI jobs should explicitly set the `name` field
    Đang mở
    • Có gì không ổn?

    Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 55/100

    rocq-prover/stdlib#142 ·

  • "Cachix setup coq" failed on CI
    Đang mở
    • Có gì không ổn?

    Độ khó 3/5 1-2 ngày Mức phù hợp với người mới 25/100

    rocq-prover/stdlib#140 ·

  • `NoDup_dec` definition is opaque
    Đang mở
    • Có gì không ổn?

    Độ khó 1/5 Dưới một giờ Mức phù hợp với người mới 50/100

    rocq-prover/stdlib#125 ·

  • What is the merging policy for stdlib? (contributing.md is nonsense)
    Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100

    rocq-prover/stdlib#116 · 2 bình luận ·

  • Keep All.v in topological order
    Đang mở
    • Có gì không ổn?

    Độ khó 3/5 1-2 ngày Mức phù hợp với người mới 42/100

    rocq-prover/stdlib#106 · 1 bình luận ·

  • `int64` equivalent for `ExtrOcamlIntConv`
    Đang mở
    • Có gì không ổn?

    Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 25/100

    rocq-prover/stdlib#3 ·

  • stdlib exports conflicting notations
    Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100

    rocq-prover/stdlib#4 ·

  • Confusing warning: Using Vector.t is known to be technically difficult
    Đang mở
    • Có gì không ổn?

    Độ khó 3/5 1-2 ngày Mức phù hợp với người mới 35/100

    rocq-prover/stdlib#5 · 5 bình luận ·

  • ZifyBool overriding zify_post_hook is a bad idea
    Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 25/100

    rocq-prover/stdlib#6 ·

  • Hard to fix Stdlib arithmetic deprecations in 8.18 breaking many projects in 8.19
    Đang mở
    • Có gì không ổn?

    Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 25/100

    rocq-prover/stdlib#7 · 18 bình luận ·

  • `Scheme Equality for nat` + `Require Import Coq.Logic.Eqdep_dec.` breaks `inversion` ("Illegal application" at Qed)
    Đang mở
    • Có gì không ổn?

    Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 25/100

    rocq-prover/stdlib#8 ·

  • Bottlenecks in standard library
    Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100

    rocq-prover/stdlib#9 · 1 bình luận ·

  • List.rev is unexpectedly quadratic
    Đang mở
    • Có gì không ổn?

    Độ khó 1/5 Dưới một giờ Mức phù hợp với người mới 35/100

    rocq-prover/stdlib#10 · 3 bình luận ·

  • `ListNotations` breaks primitive array syntax
    Đang mở
    • Có gì không ổn?

    Độ khó 3/5 1-2 ngày Mức phù hợp với người mới 35/100

    rocq-prover/stdlib#11 · 8 bình luận ·

  • Import Nsatz redefines "0" and "1"
    Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100

    rocq-prover/stdlib#12 · 6 bình luận ·

  • Missing lemmas about Prop: absorbing or neutral elements for various operations
    Đang mở
    • Có gì không ổn?

    Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 45/100

    rocq-prover/stdlib#14 · 3 bình luận ·

  • Setoid rewriting hardcodes stdlib paths instead of relying on Register
    Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100

    rocq-prover/stdlib#15 · 1 bình luận ·

  • Conflicting use of "~=" in Coq.Program.Equality and Coq.Structures.Equalities
    Đang mở
    • Có gì không ổn?

    Độ khó 3/5 1-2 ngày Mức phù hợp với người mới 35/100

    rocq-prover/stdlib#16 ·

  • coqc infinite loop in type class resolution
    Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100

    rocq-prover/stdlib#17 · 8 bình luận ·

  • The Standard Library should not be adding transitivity and symmetry hints to `core`
    Có thể làm lại được Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 38/100

    rocq-prover/stdlib#18 · 3 bình luận ·

  • Dep_elim database not used?
    Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100

    rocq-prover/stdlib#20 · 1 bình luận ·

  • `Require Import Coq.Sorting.Permutation.` slows down `rewrite_strat` > 10x
    Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100

    rocq-prover/stdlib#21 · 7 bình luận ·

  • Strong natural induction should be simpler
    Đang mở
    • Có gì không ổn?

    Độ khó 3/5 1-2 ngày Mức phù hợp với người mới 45/100

    rocq-prover/stdlib#22 · 1 reaction ·

  • binary and octal number notations
    Đang mở
    • Có gì không ổn?

    Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 35/100

    rocq-prover/stdlib#23 · 1 bình luận · 1 reaction ·

  • Cannot pattern match on exist in program definitions
    Đang mở
    • Có gì không ổn?

    Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 25/100

    rocq-prover/stdlib#24 ·

  • incl_dec and NoDup_dec should be Defined and not Qed
    Có thể làm lại được Đang mở
    • Có gì không ổn?

    Độ khó 1/5 1-3 giờ Mức phù hợp với người mới 65/100

    rocq-prover/stdlib#25 ·

  • btauto should not modify core HintDb
    Đang mở
    • Có gì không ổn?

    Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 25/100

    rocq-prover/stdlib#27 · 4 bình luận ·

  • definition of field and ring theories excluded from standard library reference main page
    Đang mở
    • Có gì không ổn?

    Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 35/100

    rocq-prover/stdlib#28 · 3 bình luận · 1 reaction ·

  • Require Import Int63 breaks `Definition land := ...`
    Đang mở
    • Có gì không ổn?

    Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 20/100

    rocq-prover/stdlib#29 · 1 bình luận · 1 reaction ·

  • NoDup List Cut Function
    Đang mở
    • Có gì không ổn?

    Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100

    rocq-prover/stdlib#30 · 1 bình luận ·

  • Z.mod_mul_r and Z.rem_mul_r reversed
    Đang mở
    • Có gì không ổn?

    Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 45/100

    rocq-prover/stdlib#31 ·

  • Reals: Make "Rsqr x" and an alias for "x^2"
    Đang mở
    • Có gì không ổn?

    Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 25/100

    rocq-prover/stdlib#32 · 17 bình luận ·

  • ExtrOCamlInt63 contains an upper-case C in its name
    Đang mở
    • Có gì không ổn?

    Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 45/100

    rocq-prover/stdlib#33 · 10 bình luận ·

  • suprirsing hints leak
    Đang mở
    • Có gì không ổn?

    Độ khó 3/5 1-2 ngày Mức phù hợp với người mới 35/100

    rocq-prover/stdlib#34 · 4 bình luận ·

  • Naming conventions broken (cos/sin)
    Đang mở
    • Có gì không ổn?

    Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 45/100

    rocq-prover/stdlib#35 · 2 bình luận ·

  • Please add gprogress and grepeat and gtry and g+ and g[> tac.. ]
    Đang mở
    • Có gì không ổn?

    Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 20/100

    rocq-prover/stdlib#37 · 2 bình luận · 1 reaction ·

  • Declare `Hint Mode` for `Reflexive`, `Symmetric`, `Equivalence`, ...
    Đang mở
    • Có gì không ổn?

    Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 38/100

    rocq-prover/stdlib#38 · 9 bình luận ·

Nhận issue mới trong hộp thư của bạn

Bản tóm tắt ngắn những issue GitHub phù hợp với người mới.