Explicit Projection nodes in concrete syntax #14598
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
herbelin
added
kind: cleanup
herbelin
force-pushed
the
master+proj-nodes-in-concrete-syntax
branch
5 times, most recently
from
9a4de81
to
d46ec0b
Compare
|
Hey, I have detected that there were CI failures at commit d46ec0b without any failure in the test-suite. |
1 similar comment
|
Hey, I have detected that there were CI failures at commit d46ec0b without any failure in the test-suite. |
|
@coqbot CI minimize |
|
I have initiated minimization at commit d46ec0b for the suggested targets ci-argosy, ci-compcert as requested. |
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/argosy/src/Spec/Proc.v (from ci-argosy) (full log on GitHub Actions) Minimized Coq File (consider adding this file to the test-suite)(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-deprecated-native-compiler-option" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/argosy/src" "RecoveryRefinement" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/argosy/vendor/classes/src" "Classes" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/argosy/vendor/array/src" "Array" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/argosy/vendor/tactical/src" "Tactical" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "Proc" "-native-compiler" "ondemand") -*- *)
(* File reduced by coq-bug-finder from original input, then from 140 lines to 37 lines, then from 60 lines to 1007 lines, then from 1010 lines to 51 lines, then from 55 lines to 50 lines *)
(* coqc version 8.15+alpha compiled with OCaml 4.05.0
coqtop version 8.15+alpha *)
Set Implicit Arguments.
Definition relation A B T := A -> B -> T -> Prop.
Definition and_then {A B C} {T1 T2}
(r1: relation A B T1)
(r2: T1 -> relation B C T2) :
relation A C T2 :=
fun x z o2 => exists o1 y, r1 x y o1 /\ (r2 o1) y z o2.
Definition pure A T (o0:T) : relation A A T :=
fun x y o => x = y /\ o = o0.
Delimit Scope relation_scope with rel.
Open Scope relation_scope.
Notation "x <- p1 ; p2" := (and_then p1 (fun x => p2))
(at level 54, right associativity,
format "'[' x <- '[v ' p1 ']' ; ']' '/' p2")
: relation_scope.
Global Generalizable Variables T R Op State.
Inductive proc (Op: Type -> Type) (T : Type) : Type :=
| Call (op : Op T)
| Ret (v : T)
| Bind (T1 : Type) (p1 : proc Op T1) (p2 : T1 -> proc Op T).
Arguments Call {Op T}.
Arguments Ret {Op T} v.
Definition OpSemantics Op State := forall T, Op T -> relation State State T.
Definition CrashSemantics State := relation State State unit.
Record Dynamics Op State :=
{ step: OpSemantics Op State;
crash_step: CrashSemantics State; }.
Section Dynamics.
Context `(sem: Dynamics Op State).
Notation proc := (proc Op).
Notation step := sem.(step).
Fixpoint exec {T} (p: proc T) : relation State State T :=
match p with
| Ret v => pure v
| Call op => step op
| Bind p p' => v <- exec p; exec (p' v)
end.Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-deprecated-native-compiler-option" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/argosy/src" "RecoveryRefinement" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/argosy/vendor/classes/src" "Classes" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/argosy/vendor/array/src" "Array" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/argosy/vendor/tactical/src" "Tactical" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "Proc" "-native-compiler" "ondemand") -*- *)
(* File reduced by coq-bug-finder from original input, then from 140 lines to 37 lines, then from 60 lines to 1007 lines, then from 1010 lines to 51 lines, then from 55 lines to 49 lines *)
(* coqc version 8.15+alpha compiled with OCaml 4.05.0
coqtop version 8.15+alpha *)
Definition relation A B T := A -> B -> T -> Prop.
Definition and_then {A B C} {T1 T2}
(r1: relation A B T1)
(r2: T1 -> relation B C T2) :
relation A C T2 :=
fun x z o2 => exists o1 y, r1 x y o1 /\ (r2 o1) y z o2.
Definition pure A T (o0:T) : relation A A T :=
fun x y o => x = y /\ o = o0.
Delimit Scope relation_scope with rel.
Open Scope relation_scope.
Notation "x <- p1 ; p2" := (and_then p1 (fun x => p2))
(at level 54, right associativity,
format "'[' x <- '[v ' p1 ']' ; ']' '/' p2")
: relation_scope.
Global Generalizable Variables T R Op State.
Inductive proc (Op: Type -> Type) (T : Type) : Type :=
| Call (op : Op T)
| Ret (v : T)
| Bind (T1 : Type) (p1 : proc Op T1) (p2 : T1 -> proc Op T).
Arguments Call {Op T}.
Arguments Ret {Op T} v.
Definition OpSemantics Op State := forall T, Op T -> relation State State T.
Definition CrashSemantics State := relation State State unit.
Record Dynamics Op State :=
{ step: OpSemantics Op State;
crash_step: CrashSemantics State; }.
Section Dynamics.
Context `(sem: Dynamics Op State).
Notation proc := (proc Op).
Notation step := sem.(step).
Fixpoint exec {T} (p: proc T) : relation State State T :=
match p with
| Ret v => pure v
| Call op => step op
| Bind p p' => v <- exec p; exec (p' v)
end.Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 2.7MiB file on GitHub Actions Artifacts under
|
|
See also #6651. IIUC, this PR was reverted due to issues with backwards compatibility. |
This comment has been minimized.
This comment has been minimized.
Yes, I know well #6651 and I started from it. The differences are:
So shortly, the purpose of this PR is not per se to address a problem with primitive projections but to simply replace the existing encoding of projections in the Nevertheless, my main worry is not to overlap with what other developers are doing around projections. Had someone else the intention to resuscitate #6651? Was someone thinking that adding an explicit |
JasonGross
added a commit
to coq-community/run-coq-bug-minimizer
that referenced
this pull request
Jul 5, 2021
|
@coqbot ci minimize ci-compcert |
|
I am now running minimization at commit d46ec0b on requested target ci-compcert. I'll come back to you with the results once it's done. |
This comment has been minimized.
This comment has been minimized.
|
@JasonGross: for the record, I could compile the minimized Compcert file with a few changes:
|
herbelin
force-pushed
the
master+proj-nodes-in-concrete-syntax
branch
from
d46ec0b
to
db7b031
Compare
At least I believe it's a necessary change, but it must be performed as incrementally as possible. It's too easy to silently wreak havoc for users of primitive projections, so we must clearly delineate the potential effects on semantics that were not envisioned at the time of writing the patch. |
herbelin
force-pushed
the
master+proj-nodes-in-concrete-syntax
branch
4 times, most recently
from
e0beba2
to
5dbfc38
Compare
I moved the "feature" part in #14606. So, up to mistakes, this PR should now be restricted to only changing the In particular, in this PR, Note that the notation Added: There is also extra support for explicit universes in the |
herbelin
force-pushed
the
master+proj-nodes-in-concrete-syntax
branch
from
5dbfc38
to
b5c563c
Compare
ppedrot
approved these changes
Jul 21, 2021
herbelin
force-pushed
the
master+proj-nodes-in-concrete-syntax
branch
2 times, most recently
from
cd47482
to
5e3522e
Compare
github-actions
bot
added
needs: rebase
|
The overlay for coq-elpi is now OK IMO. (but you need to rebase this PR, since another PR with an overlay was merged meanwhile) |
herbelin
force-pushed
the
master+proj-nodes-in-concrete-syntax
branch
from
5e3522e
to
bbebaac
Compare
coqbot-app
bot
removed
the
needs: rebase
|
@herbelin can we try to get a clean CI? I don't remember if this was ever green, but if so it'd allow to merge quickly. |
herbelin
force-pushed
the
master+proj-nodes-in-concrete-syntax
branch
from
bbebaac
to
0f66f53
Compare
|
CI green. I'll leave a few more days for potential input before merging, but don't wait for too long if you want to comment here. |
github-actions
bot
added
the
needs: rebase
…b_term. This is an alternative to the encoding of projections in the CApp/CAppExpl nodes.
herbelin
force-pushed
the
master+proj-nodes-in-concrete-syntax
branch
from
0f66f53
to
f35ab48
Compare
coqbot-app
bot
removed
the
needs: rebase
jfehrle
reviewed
Jul 31, 2021
| @@ -9,6 +9,14 @@ | |||
|
|
|||
| - Renaming `LSet` into `Level.Set` and `LMap` into `Level.Map` | |||
|
|
|||
| ### Concrete syntax | |||
There was a problem hiding this comment.
The changelog entry should be created with dev/tools/make-changelog.sh rather than added directly here.
There was a problem hiding this comment.
These changes are about the OCaml API which don't go in the doc/changelog directory as far as I know.
There was a problem hiding this comment.
It would fit into the "misc" category. If you don't want to put it there, maybe use the title "OCaml API" or "OCaml API (internals)" instead of "Concrete syntax".
There was a problem hiding this comment.
My point is that users who are not plugin developers do not need to know about the changes in this PR as they are without visible effect on using Coq.
On the other side, the related #14640 is normally going to introduce changes of behavior and I agree that it will need a "user-level" change log.
Janno
reviewed
Aug 1, 2021
Co-authored-by: Jan-Oliver Kaiser <mail@janno-kaiser.de>
Co-authored-by: Jan-Oliver Kaiser <mail@janno-kaiser.de>
proux01
added a commit
to proux01/coq
that referenced
this pull request
Sep 1, 2021
ppedrot
added a commit
that referenced
this pull request
Sep 2, 2021
LasseBlaauwbroek
added a commit
to coq-tactician/coq-tactician
that referenced
this pull request
Oct 25, 2021
This was referenced Oct 26, 2021
Open
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Kind: infrastructure.
This PR changes the isproj-based encoding of
CApp/CAppExplto explicitCProj/GProj/NProjconstructors.There is also support for universes in the
r.(f)syntax.It is similar to #6651 but purely restricted to the change of representation. In particular, in this PR,
NProjbehaves likeNAppandGProjlikeGApp(for instance, reversibility of parsing as in #6764 works). Compared to #6651, it includes parameters in theCProj/GProj/NProjso as to cover the case of non-primitive projections too. Also, it implements appropriate code for these extra constructors (up to one exception in funind which I suspect should not occur).dev/doc/changes.mdNote: The PR originally included an improvement about using implicit arguments with the
r.(f)syntax though. It moved to #14606 on which it depended. #14606 itself evolved to also fix #4167.