stdlib exports conflicting notations
まだ誰も着手していません。
評価
- 難易度
- 4/5
- 見積もり時間
- 3〜5日
- 初心者へのやさしさ
- 35/100
- issue の種類
- バグ
- 明瞭さ
- 説明が足りない
- 活発さ
- 停滞
- 領域
- tooling
調査の方向性
theories/All.v から始め、そこに記載されている警告を再現してください。NaryFunctions、rtauto、vector、nsatz、ssrbool、datatypes、CEquivalence、Equivalence、setoid_ring.Algebra_syntax、setoids、EquivDec、SetoidDec の表記宣言を調査してください。影響を受ける scopes を壊すことなく、競合または上書きされた表記に関する警告が解消されれば完了です。
索引モデルが issue の本文から書いたものです。
説明
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notations "_ ^^ _" defined at level 30 with arguments constr
at next level, constr at level 30 and "_ ^^ _ --> _" defined at level 50
with arguments constr at next level, constr at next level
have incompatible prefixes. One of them will likely not work.
[notation-incompatible-prefix,parsing,default]
Zpower_alt infix vs some deprecated notation in NaryFunctions
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notation "[ _ ]" was already used.
[notation-overridden,parsing,default]
rtauto vs vector
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notation "[ _ ]" was already used.
[notation-overridden,parsing,default]
nsatz vs rtauto
File "./theories/All.v", line 3, characters 0-12361:
Warning: Overwriting previous delimiting key B in scope bool_scope
[overwriting-delimiting-key,parsing,default]
ssrbool vs datatypes
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notation "_ === _" was already used in scope equiv_scope.
[notation-overridden,parsing,default]
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notation "_ =/= _" was already used in scope equiv_scope.
[notation-overridden,parsing,default]
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notation "_ =~= _" was already used in scope equiv_scope.
[notation-overridden,parsing,default]
CEquivalence vs Equivalence
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notation "_ == _" was already used.
[notation-overridden,parsing,default]
setoid_ring.Algebra_syntax vs setoids
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notation "_ ==b _" was already used.
[notation-overridden,parsing,default]
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notation "_ <>b _" was already used.
[notation-overridden,parsing,default]
EquivDec vs SetoidDec (these 2 files are pretty similar, not sure why we have both)
Originally posted by @SkySkimmer in https://github.com/coq/coq/issues/19914#issuecomment-2545418807
- 主要言語
- Rocq Prover
- スター
- 46
- フォーク
- 39
- 平均マージ
- 4日 12時間
- マージ済み PR（30日）
- 5
環境構築
- Dockerfile・Docker Compose ファイルなし
- プルリクエストのテンプレートあり
- コントリビューションガイドを読む
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- issue 番号を参照したプルリクエストを送ります。
rocq-prover/stdlib のほかの issue
-
incl_dec and NoDup_dec should be Defined and not Qed再び着手できるかも このイシューのプルリクエストはマージされずにクローズされました。 オープン
難易度 1/5 1〜3時間 初心者へのやさしさ 65/100
rocq-prover/stdlib#25 ·
-
Reals: a constructive pi for the constructive Cauchy reals with a strong irrationality separation theorem (Leibniz series)対応中かも @hy7pc8gfmf-dotcom が 27 日前に担当しました。 オープン
難易度 5/5 1週間以上 初心者へのやさしさ 6/100
rocq-prover/stdlib#315 ·
-
Reals: escape-window separation engine for the constructive Cauchy reals (abstract irrationality criterion)対応中かも このイシューにリンクされたプルリクエストがオープン中、またはマージ済みです。 オープン
難易度 5/5 1週間以上 初心者へのやさしさ 35/100
rocq-prover/stdlib#312 ·
-
難易度 5/5 1週間以上 初心者へのやさしさ 25/100
rocq-prover/stdlib#293 ·
-
Inconsistent OPAM packaging of rocq-stdlib対応中かも このイシューにリンクされたプルリクエストがオープン中、またはマージ済みです。 オープン
難易度 4/5 3〜5日 初心者へのやさしさ 42/100
rocq-prover/stdlib#256 · コメント 4 件 · リアクション 3 件 ·
rocq-prover/stdlib の issue をすべて見る
似ている issue
-
難易度 2/5 1〜3時間 初心者へのやさしさ 78/100
メンテナーはふだん 1 日以内に返信
-
bug
難易度 2/5 1〜3時間 初心者へのやさしさ 76/100
open-constructs/cdk-terrain#558 ·
メンテナーはふだん 1 日以内に返信
-
T8: Ignore log filesオープンgood first issue
難易度 1/5 1時間未満 初心者へのやさしさ 95/100
ozaydincan/Workshop_Demo#18 ·
-
[Bug]: cua-driver skill fails Agent Skills frontmatter validation対応中かも @Mearman が今日担当しました。 オープン
難易度 2/5 1〜3時間 初心者へのやさしさ 76/100
メンテナーはふだん 1 日以内に返信
-
follow-up needs-triage S3: minor
難易度 2/5 1〜3時間 初心者へのやさしさ 72/100
manaflow-ai/cmux#36856 · コメント 1 件 ·
メンテナーはふだん 1 日以内に返信