Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Porting to 8.15 #9

Closed
wants to merge 3 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/main.yml
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ jobs:
opam_file:
- 'coq-autosubst-ocaml.opam'
image:
- 'coqorg/coq:8.14.1-ocaml-4.14.1-flambda'
- 'coqorg/coq:8.15.2-ocaml-4.14.1-flambda'
fail-fast: false # don't stop jobs if one fails
steps:
- uses: actions/checkout@v2
Expand Down
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
- Maintainer:
- Yannick Forster ([**@yforster**](https://github.com/yforster))
- License: [MIT License](LICENSE)
- Compatible Coq versions: 8.14.0
- Compatible Coq versions: 8.15.2
- Related publication(s):
- Adrian Dapprich's [bachelor thesis](https://www.ps.uni-saarland.de/~dapprich/bachelor.php) (Advisor: Andrej Dudenhefner, Supervisor: Gert Smolka)

Expand Down
4 changes: 2 additions & 2 deletions case-studies/kathrin/coq/ARS.v
Original file line number Diff line number Diff line change
Expand Up @@ -65,8 +65,8 @@ Lemma star_img T1 T2 (f : T1 -> T2) (e1 : Rel T1) e2 :
(forall x y, e1 x y -> star e2 (f x) (f y)) ->
(forall x y, star e1 x y -> star e2 (f x) (f y)).
Proof.
intros. induction H0; eauto.
eapply star_trans with (y0 := f y); eauto.
intros ? x y H. induction H; eauto.
eapply star_trans with (y := f y); eauto.
Qed.

Lemma star_hom T1 T2 (f : T1 -> T2) (e1 : Rel T1) (e2 : Rel T2) :
Expand Down
4 changes: 2 additions & 2 deletions case-studies/kathrin/coq/Chapter10/POPLMark1.v
Original file line number Diff line number Diff line change
Expand Up @@ -290,7 +290,7 @@ Proof.
+ intros. asimpl.
unfold funcomp.
rewrite <- H'. now asimpl.
- eapply T_Tapp with (A0 := A⟨sigma⟩) (B0:=ren_ty (upRen_ty_ty sigma) B).
- eapply T_Tapp with (A := A⟨sigma⟩) (B :=ren_ty (upRen_ty_ty sigma) B).
asimpl in IHty.
eapply IHty; eauto.
eapply sub_weak; eauto.
Expand Down Expand Up @@ -324,7 +324,7 @@ Proof.
eapply context_renaming_lemma; eauto.
* intros. now asimpl.
* intros. now asimpl.
- eapply T_Tapp with (A0 := subst_ty sigma A) (B0:=B[up_ty_ty sigma]).
- eapply T_Tapp with (A := subst_ty sigma A) (B :=B[up_ty_ty sigma]).
asimpl in IHty. eapply IHty; eauto.
eapply sub_substitution; eauto.
now asimpl.
Expand Down
6 changes: 3 additions & 3 deletions case-studies/kathrin/coq/Chapter10/POPLMark21.v
Original file line number Diff line number Diff line change
Expand Up @@ -574,7 +574,7 @@ Proof.
unfold funcomp. rewrite <- H. now asimpl.
+ intros. asimpl.
unfold funcomp. rewrite <- H'. now asimpl.
- cbn. eapply T_Tapp with (A0 := A⟨xi⟩) .
- cbn. eapply T_Tapp with (A := A⟨xi⟩) .
Unshelve.
4: exact (ren_ty (upRen_ty_ty xi) B).
eapply IHty; eauto.
Expand All @@ -585,7 +585,7 @@ Proof.
eapply in_map_iff in H6. destruct H6 as ([j A']&?&?). inv H5.
eapply H3; eassumption.
- cbn. econstructor; eauto. now apply in_map.
- cbn. asimpl. apply letpat_ty with (A0 := A⟨xi⟩) (Gamma'0 := Gamma' >> ⟨xi⟩); eauto.
- cbn. asimpl. apply letpat_ty with (A := A⟨xi⟩) (Gamma' := Gamma' >> ⟨xi⟩); eauto.
+ unfold funcomp. substify.
eauto.
+ asimpl. eapply IHty2; eauto.
Expand Down Expand Up @@ -634,7 +634,7 @@ Proof.
eapply context_renaming_lemma; try eapply eq2.
* intros. now asimpl.
* intros. now asimpl.
- eapply T_Tapp with (A0 := subst_ty sigma A) (B0 := B[up_ty_ty sigma]).
- eapply T_Tapp with (A := subst_ty sigma A) (B := B[up_ty_ty sigma]).
asimpl in IHty. eapply IHty; eauto.
eapply sub_substitution; eauto.
now asimpl.
Expand Down
6 changes: 3 additions & 3 deletions case-studies/kathrin/coq/Chapter10/POPLMark22.v
Original file line number Diff line number Diff line change
Expand Up @@ -581,7 +581,7 @@ Proof.
unfold funcomp. rewrite <- H. now asimpl.
+ intros. asimpl.
unfold funcomp. rewrite <- H'. now asimpl.
- cbn. eapply T_Tapp with (A0 := A⟨xi⟩) (B0 := ren_ty (upRen_ty_ty xi) B).
- cbn. eapply T_Tapp with (A := A⟨xi⟩) (B := ren_ty (upRen_ty_ty xi) B).
asimpl in IHty. eapply IHty; eauto.
eapply sub_weak; eauto. now asimpl.
- econstructor; eauto.
Expand All @@ -590,7 +590,7 @@ Proof.
eapply in_map_iff in H6. destruct H6 as ([j A']&?&?). inv H5.
eapply H3; eassumption.
- cbn. econstructor; eauto. now apply in_map.
- cbn. asimpl. apply letpat_ty with (A0 := A⟨xi⟩) (Gamma'0 := Gamma' >> ⟨xi⟩); eauto.
- cbn. asimpl. apply letpat_ty with (A := A⟨xi⟩) (Gamma' := Gamma' >> ⟨xi⟩); eauto.
+ substify.
eauto.
+ asimpl.
Expand Down Expand Up @@ -638,7 +638,7 @@ Proof.
eapply context_renaming_lemma; try eapply eq2.
* intros. now asimpl.
* intros. now asimpl.
- eapply T_Tapp with (A0 := subst_ty sigma A) (B0 := subst_ty (up_ty_ty sigma) B).
- eapply T_Tapp with (A := subst_ty sigma A) (B := subst_ty (up_ty_ty sigma) B).
asimpl in IHty. eapply IHty; eauto.
eapply sub_substitution; eauto.
now asimpl.
Expand Down
2 changes: 1 addition & 1 deletion coq-autosubst-ocaml.opam
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ license: "MIT"

depends: [
"ocaml" { >= "4.09" & < "4.15" }
"coq" { >= "8.14.0" & < "8.15" }
"coq" { >= "8.15.0" & < "8.16" }
"angstrom" { >= "0.15.0" }
"dune" { >= "2.5" }
"ocamlgraph" { >= "2.0.0" }
Expand Down
2 changes: 1 addition & 1 deletion lib/automationGen.ml
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,7 @@ module NotationGen = struct

let level_ l = SetLevel l
let assoc_ a = SetAssoc a
let format_ fmt = SetFormat ("text", CAst.make fmt)
let format_ fmt = SetFormat (TextFormat (CAst.make fmt))
let only_print_ = SetOnlyPrinting

let to_substs x sorts = List.map (fun s -> sep x s) sorts
Expand Down
18 changes: 9 additions & 9 deletions lib/gallinaGen.ml
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ let app_ f xs =
let app1_ f x =
Constrexpr_ops.mkAppC (f, [x])
let appExpl_ n xs =
CAst.make @@ Constrexpr.CAppExpl ((None, qualid_ n, None), xs)
CAst.make @@ Constrexpr.CAppExpl ((qualid_ n, None), xs)
let app_ref ?(expl=false) s t =
if expl then appExpl_ s t
else app_ (ref_ s) t
Expand Down Expand Up @@ -135,16 +135,16 @@ let setup_coq () =
* future and this should work *)
let dummy_eq =
app_ (lambda_ [ binder_ [ "a"; "b" ] ] prop_) [ (ref_ "x"); (ref_ "y") ] in
let () = Metasyntax.add_notation ~local:false None (Global.env ()) dummy_eq
(CAst.make "x = y", [ Vernacexpr.SetLevel 70
; Vernacexpr.SetOnlyPrinting
; Vernacexpr.SetAssoc Gramlib.Gramext.NonA ])
let () = Metasyntax.add_notation ~infix:false ~local:false None (Global.env ()) dummy_eq
(CAst.make "x = y", [ CAst.make (Vernacexpr.SetLevel 70)
; CAst.make (Vernacexpr.SetOnlyPrinting)
; CAst.make (Vernacexpr.SetAssoc Gramlib.Gramext.NonA) ])
(Some scope) in
let dummy_arrow = forall1_ (binder1_ "A") (ref_ "B") in
let () = Metasyntax.add_notation ~local:false None (Global.env ()) dummy_arrow
(CAst.make "A -> B", [ Vernacexpr.SetLevel 70
; Vernacexpr.SetOnlyPrinting
; Vernacexpr.SetAssoc Gramlib.Gramext.RightA ])
let () = Metasyntax.add_notation ~infix:false ~local:false None (Global.env ()) dummy_arrow
(CAst.make "A -> B", [ CAst.make (Vernacexpr.SetLevel 70)
; CAst.make (Vernacexpr.SetOnlyPrinting)
; CAst.make (Vernacexpr.SetAssoc Gramlib.Gramext.RightA) ])
(Some scope) in
()

2 changes: 1 addition & 1 deletion lib/program.ml
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ let parse_args args =
("-no-static", Clear gen_static_files_r, "Don't put the static files like core.v, unscoped.v, etc. into the output directory.");
("-allfv", Set gen_allfv_r, "Generate allfv lemmas.");
("-fext", Set gen_fext_r, "Generate lemmas & tactics that use the functional extensionality axiom.");
("-p", String set_prelude, "Prepend the content of the given file front of the generated output.")
("-p", String set_prelude, "Prepend the content of the given file in front of the generated output.")
] in
(* The usage message should use the current program's name *)
let program_name = match Sys.argv.(0) with
Expand Down
12 changes: 6 additions & 6 deletions lib/vernacGen.ml
Original file line number Diff line number Diff line change
Expand Up @@ -72,20 +72,20 @@ let instance_ inst_name cbinders class_type ?(interactive=false) body =
then
Vernac [ CAst.make {
control=[];
attrs=[("global", Attributes.VernacFlagEmpty)] ;
attrs=[CAst.make ("global", Attributes.VernacFlagEmpty)] ;
expr=VernacInstance (name_decl_ inst_name, cbinders, class_type, None, Typeclasses.{ hint_priority = None; hint_pattern = None });
}
; control_of_expr (VernacExactProof body)
; control_of_expr (VernacEndProof (Proved (Opaque, None))) ]
else
Vernac [CAst.make {
control=[];
attrs=[("global", Attributes.VernacFlagEmpty)] ;
attrs=[CAst.make ("global", Attributes.VernacFlagEmpty)] ;
expr=VernacInstance (name_decl_ inst_name, cbinders, class_type, Some (false, body), Typeclasses.{ hint_priority = None; hint_pattern = None });
} ]

let notation_ notation modifiers ?scope body =
unit_of_vernacs [ VernacNotation (body, (CAst.make notation, modifiers), scope) ]
unit_of_vernacs [ VernacNotation (false, body, (CAst.make notation, List.map CAst.make modifiers), scope) ]

let clear_arguments_ name =
let qname = CAst.make (Constrexpr.AN (qualid_ name)) in
Expand All @@ -104,9 +104,9 @@ let impl_arguments_ name args =

(* TODO somehow the imported module is printed on a new line. looks like automatic line break issue *)
let import_ name =
unit_of_vernacs [ VernacImport (false, [ (qualid_ name, ImportAll) ]) ]
unit_of_vernacs [ VernacImport (false, None, [(qualid_ name, ImportAll) ]) ]
let export_ name =
unit_of_vernacs [ VernacImport (true, [ (qualid_ name, ImportAll) ]) ]
unit_of_vernacs [ VernacImport (true, None, [(qualid_ name, ImportAll) ]) ]

let module_ name contents =
List.concat [
Expand All @@ -122,7 +122,7 @@ let module_ name contents =
let setoid_opaque_hint version name =
let attrs = match version with
| S.LT813 -> []
| S.GE813 -> [("global", Attributes.VernacFlagEmpty)]
| S.GE813 -> [CAst.make ("global", Attributes.VernacFlagEmpty)]
in
Vernac [ CAst.make {
control=[];
Expand Down
4 changes: 2 additions & 2 deletions monadic/library/zipSeq.ml
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
module ZipSeqAlternative = struct
type 'a t = 'a Stdlib.Seq.t

let zip xs ys () =
let rec zip xs ys () =

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this rec is ambiguous: for Stdlib version < 4.14, Stdlib.Seq.zip is not defined hence the recursive call is used, but in versions >= 4.14 the function zip is defined in the lib and this rec is unused... And similar for drop below.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, it's been a source of confusion and back and forth issues… I am no OCaml expert, do you know how to disambiguate to give priority to the local recursively defined function? Or maybe we should drop (this part of) the monadic library, which seems to be stuck with 4.13?

let open Stdlib.Seq in
match (xs (), ys ()) with
| Cons (l1, ls1), Cons (l2, ls2) -> Cons ((l1, l2), zip ls1 ls2)
| _ -> Nil

let drop i xs =
let rec drop i xs =
let open Stdlib.Seq in
if i <= 0 then xs
else match xs () with Nil -> empty | Cons (_, ls) -> drop (i - 1) ls
Expand Down
Loading