Test PR related to Issue 228

[DmxLarchey]

See #228

[DmxLarchey]

The change of priority here (or else in file theories/MinskyMachines/MMenv/env.v) results in messing with the SSR syntax for rewrite, see eg file

coq-library-undecidability/theories/MinskyMachines/Deciders/MM_2_HALTING_dec.v

Line 53 in 33c2231

by rewrite [LHS](vec_head_tail v) [in LHS](vec_head_tail (vec_tail v)) [in LHS](vec_0_nil (vec_tail (vec_tail v))).

[mrhaandi]

Is it due to unscoped, global, top-level notations? If so, is it much work to change that to opt-in notations (a common design practice for modular code)?

[DmxLarchey]

I modified the code to have a module vec_notations but it created some issues, see below. @mrhaandi does it suit you, and are the corrections it implied satisfactory for you ?

[DmxLarchey]

The last warning issue remaining is related to
https://github.com/DmxLarchey/coq-library-undecidability/blob/7b03998b700bd304d8e0480881d0cb6f8f57e078/theories/MinskyMachines/MM2.v#L45

Reserved Notation "i '//' r '⇢' s" (at level 70, no associativity).
Reserved Notation "P '//' r '→' s" (at level 70, no associativity).
Reserved Notation "P '//' r '↠' s" (at level 70, no associativity).
Reserved Notation "P '//' r ↓" (at level 70, no associativity).

where Coq/Rocq asks for the reserved notation _ // _ ↓ to be put at level 1 (instead of 70), because it ends with a terminal symbol. However, doing so has the side effect of preempting other notations like _ // _ ⇢ _ which do not end with a terminal symbol. Hence, if they are not also at level 1, this mainly forbids the parsing of the other notations.

The reason I did choose level 70 for these is logical: these are Prop atoms and this level is nice for those kinds of terms.

@mrhaandi I do not know how to handle this at the moment?.

[DmxLarchey]

The last commit 10478ab solves the issue of left/right bi-closed notations that should be at level 0 according to Coq/Rocq. These had no side effects at all, so a straightforward correction.

[mrhaandi]

@DmxLarchey Is it correct that the last remaining issue is:

File "./Shared/Libs/DLW/Code/sss.v", line 25, characters 0-65:
Warning: Postfix notations (i.e. starting with a nonterminal symbol and
ending with a terminal symbol) should usually be at level 1 (default).
[postfix-notation-not-level-1,parsing,default]

[DmxLarchey]

@mrhaandi Yes this is correct except that the very same issue also pops up in:

coq-library-undecidability/theories/MinskyMachines/MM2.v

Lines 45 to 48 in 70dfc56

	Reserved Notation "i '//' r '⇢' s" (at level 70, no associativity).
	Reserved Notation "P '//' r '→' s" (at level 70, no associativity).
	Reserved Notation "P '//' r '↠' s" (at level 70, no associativity).
	Reserved Notation "P '//' r ↓" (at level 70, no associativity).

One possibility could be to modify the notation for "P terminates on input t" to something like P ↓ t but it would be quite dissimilar to the other forms P // ....

[mrhaandi]

If the final one is too ugly / bothersome to fix, we can for the near future use the same local warning suppression as the Coq standard library:
https://github.com/coq/coq/blob/c1d8bee3b89b2fc9ba6c76f472983e0f2d194f75/theories/ssr/ssreflect.v#L98

[DmxLarchey]

Thx for the advice @mrhaandi !!

[DmxLarchey]

@mrhaandi and @yforster If you are ok, I can merge this PR corresponding to issue #228

[mrhaandi]

If you are ok, I can merge this PR corresponding to issue #228

Feel free to merge.
If you like, you can also inspect the -notation-incompatible-prefix warnings in your code (which currently are also suppressed) as part of another PR.

[DmxLarchey]

you can also inspect the -notation-incompatible-prefix warnings in your code (which currently are also suppressed) as part of another PR.

@mrhaandi task completed in PR #230