rocq-prover / rocq-prover/stdlib

stdlib exports conflicting notations

Open
#4 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Dominant language
Rocq Prover
Stars
42
Forks
38
Avg merge
14h 6m
Merged PRs (30d)
3

Description

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

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Start with theories/All.v and reproduce the warnings listed there. Inspect the notation declarations in NaryFunctions, rtauto, vector, nsatz, ssrbool, datatypes, CEquivalence, Equivalence, setoid_ring.Algebra_syntax, setoids, EquivDec, and SetoidDec. Done means the conflicting or overridden notation warnings are resolved without breaking the affected scopes.

Written by the indexing model from the issue text.

Assessment

Domain
tooling
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Needs clarification
Newbie friendliness
35/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.