From f8837cfe9702b3700fbb0e07e78bec9078b498c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Thu, 23 Nov 2023 09:27:28 +0100 Subject: [PATCH 1/9] Adapt w.r.t. coq/coq#18345. --- sertop/sercomp_stats.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sertop/sercomp_stats.ml b/sertop/sercomp_stats.ml index 9259be10..e70cddcb 100644 --- a/sertop/sercomp_stats.ml +++ b/sertop/sercomp_stats.ml @@ -63,7 +63,7 @@ let do_stats = proof_loc := None (* This is tricky.. *) (* This is Ltac := ... *) - | VernacSynterp (VernacExtend (("VernacDeclareTacticDefinition",_),_)) + | VernacSynterp (VernacExtend ({ Vernacexpr.ext_entry = "VernacDeclareTacticDefinition"; _ },_)) -> stats.proofs <- incS ?loc stats.proofs; | _ -> if Option.is_empty !proof_loc then stats.misc <- incS ?loc stats.misc From b3b3d8b2fceca5fc47859798c7c407261dce9ae3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 27 Nov 2023 10:59:19 +0100 Subject: [PATCH 2/9] Adapt to coq/coq#18331 (sort poly inductives) --- serlib/ser_declarations.ml | 4 ++++ serlib/ser_names.ml | 1 + serlib/ser_names.mli | 1 + serlib/ser_sorts.ml | 6 +++++- serlib/ser_sorts.mli | 1 + 5 files changed, 12 insertions(+), 1 deletion(-) diff --git a/serlib/ser_declarations.ml b/serlib/ser_declarations.ml index 114c4519..7fb58c3e 100644 --- a/serlib/ser_declarations.ml +++ b/serlib/ser_declarations.ml @@ -63,6 +63,10 @@ type inductive_arity = [%import: Declarations.inductive_arity] [@@deriving sexp,yojson,hash,compare] +type squash_info = + [%import: Declarations.squash_info] + [@@deriving sexp,yojson,hash,compare] + type one_inductive_body = [%import: Declarations.one_inductive_body] [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_names.ml b/serlib/ser_names.ml index a46a7ddf..82d2e70a 100644 --- a/serlib/ser_names.ml +++ b/serlib/ser_names.ml @@ -218,6 +218,7 @@ module Ind = struct end module Indset_env = Ser_cSet.Make(Indset_env)(Ind) +module Indmap_env = Ser_cMap.Make(Indmap_env)(Ind) type inductive = [%import: Names.inductive] diff --git a/serlib/ser_names.mli b/serlib/ser_names.mli index ba717c10..5fc08930 100644 --- a/serlib/ser_names.mli +++ b/serlib/ser_names.mli @@ -51,6 +51,7 @@ module Mindmap : Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Mindm module Mindmap_env : Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Mindmap_env.t module Indset_env : Ser_cSet.ExtS with type elt = inductive and type t = Indset_env.t +module Indmap_env : Ser_cMap.ExtS with type key = inductive and type 'a t = 'a Indmap_env.t type 'a tableKey = 'a Names.tableKey diff --git a/serlib/ser_sorts.ml b/serlib/ser_sorts.ml index ec0f5681..4a0a5f07 100644 --- a/serlib/ser_sorts.ml +++ b/serlib/ser_sorts.ml @@ -38,7 +38,11 @@ end module Quality = struct type constant = [%import: Sorts.Quality.constant] [@@deriving sexp,yojson,hash,compare] - type t = [%import: Sorts.Quality.t] [@@deriving sexp,yojson,hash,compare] + module Self = struct + type t = [%import: Sorts.Quality.t] [@@deriving sexp,yojson,hash,compare] + end + include Self + module Set = Ser_cSet.Make(Sorts.Quality.Set)(Self) end module PierceSpec = struct diff --git a/serlib/ser_sorts.mli b/serlib/ser_sorts.mli index f3396735..dbae2f9e 100644 --- a/serlib/ser_sorts.mli +++ b/serlib/ser_sorts.mli @@ -27,6 +27,7 @@ module Quality : sig type constant = Sorts.Quality.constant [@@deriving sexp,yojson,hash,compare] include SerType.SJHC with type t = Sorts.Quality.t + module Set : SerType.SJHC with type t = Sorts.Quality.Set.t end module QConstraints : SerType.SJHC with type t = Sorts.QConstraints.t From ad603db073816770c221933e69e5f2a85f100fff Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 16 Dec 2023 22:30:36 +0100 Subject: [PATCH 3/9] Adapt to #18229: nested_type is now recarg_type (no more "nested" mark). --- serlib/ser_declarations.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/serlib/ser_declarations.ml b/serlib/ser_declarations.ml index 7fb58c3e..2fd25b74 100644 --- a/serlib/ser_declarations.ml +++ b/serlib/ser_declarations.ml @@ -42,8 +42,8 @@ type ('a, 'b) declaration_arity = [%import: ('a, 'b) Declarations.declaration_arity] [@@deriving sexp,yojson,hash,compare] -type nested_type = - [%import: Declarations.nested_type] +type recarg_type = + [%import: Declarations.recarg_type] [@@deriving sexp,yojson,hash,compare] type recarg = From a935a9a4414c5df91170a307d78d1f2807eccb09 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 15 Dec 2023 14:04:55 +0100 Subject: [PATCH 4/9] Adapt to coq/coq#18143 (debug printing for relevances) --- serlib/ser_constrexpr.ml | 8 ++++++++ serlib/ser_glob_term.ml | 9 +++++++++ tests/sername/nat_add.out | 4 ++-- 3 files changed, 19 insertions(+), 2 deletions(-) diff --git a/serlib/ser_constrexpr.ml b/serlib/ser_constrexpr.ml index be70352d..da339975 100644 --- a/serlib/ser_constrexpr.ml +++ b/serlib/ser_constrexpr.ml @@ -52,6 +52,14 @@ type quality_expr = [%import: Constrexpr.quality_expr] [@@deriving sexp,yojson,hash,compare] +type relevance_expr = + [%import: Constrexpr.relevance_expr] + [@@deriving sexp,yojson,hash,compare] + +type relevance_info_expr = + [%import: Constrexpr.relevance_info_expr] + [@@deriving sexp,yojson,hash,compare] + type sort_expr = [%import: Constrexpr.sort_expr] [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_glob_term.ml b/serlib/ser_glob_term.ml index fea8f79c..46f70335 100644 --- a/serlib/ser_glob_term.ml +++ b/serlib/ser_glob_term.ml @@ -78,6 +78,10 @@ type glob_qvar = [%import: Glob_term.glob_qvar] [@@deriving sexp,yojson,hash,compare] +type glob_relevance = + [%import: Glob_term.glob_relevance] + [@@deriving sexp,yojson,hash,compare] + type glob_quality = [%import: Glob_term.glob_quality] [@@deriving sexp,yojson,hash,compare] @@ -114,6 +118,11 @@ type glob_fix_kind = [%import: Glob_term.glob_fix_kind] [@@deriving sexp,yojson,hash,compare] +type relevance_info = + [%import: Glob_term.relevance_info] + [@@deriving sexp,yojson,hash,compare] + + type glob_evar_kind = Evar_kinds.glob_evar_kind [@@deriving sexp,yojson,hash,compare] diff --git a/tests/sername/nat_add.out b/tests/sername/nat_add.out index a0051f28..205d108f 100644 --- a/tests/sername/nat_add.out +++ b/tests/sername/nat_add.out @@ -1,2 +1,2 @@ -Nat.add: "nat -> nat -> nat" (Prod((binder_name(Name(Id n)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()()))))(Prod((binder_name(Name(Id m)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()()))))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()())))))) ((v(GProd Anonymous Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))((v(GProd Anonymous Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))))(loc()))))(loc())) -Nat.mul: "nat -> nat -> nat" (Prod((binder_name(Name(Id n)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()()))))(Prod((binder_name(Name(Id m)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()()))))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()())))))) ((v(GProd Anonymous Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))((v(GProd Anonymous Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))))(loc()))))(loc())) +Nat.add: "nat -> nat -> nat" (Prod((binder_name(Name(Id n)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()()))))(Prod((binder_name(Name(Id m)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()()))))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()())))))) ((v(GProd Anonymous()Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))((v(GProd Anonymous()Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))))(loc()))))(loc())) +Nat.mul: "nat -> nat -> nat" (Prod((binder_name(Name(Id n)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()()))))(Prod((binder_name(Name(Id m)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()()))))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()())))))) ((v(GProd Anonymous()Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))((v(GProd Anonymous()Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))))(loc()))))(loc())) From 867efb771fd281db2a7c37bf84f84c763fd48f4e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 4 Jan 2024 00:14:37 +0000 Subject: [PATCH 5/9] Adapt to coq/coq#18094: rewrite strategies: fix The type constructor `Rewrite.strategy_ast` now expects 3 arguments (the third one is for bound fixpoint identifiers). --- serlib/plugins/ltac/ser_rewrite.ml | 4 ++-- serlib/plugins/ltac/ser_rewrite.mli | 2 +- serlib/plugins/ltac/ser_tacarg.ml | 6 +++--- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/serlib/plugins/ltac/ser_rewrite.ml b/serlib/plugins/ltac/ser_rewrite.ml index 5bb79e62..5a961a88 100644 --- a/serlib/plugins/ltac/ser_rewrite.ml +++ b/serlib/plugins/ltac/ser_rewrite.ml @@ -29,8 +29,8 @@ type nary_strategy = [%import: Rewrite.nary_strategy] [@@deriving sexp,hash,compare] -type ('a,'b) strategy_ast = - [%import: ('a,'b) Rewrite.strategy_ast] +type ('a,'b,'c) strategy_ast = + [%import: ('a,'b,'c) Rewrite.strategy_ast] [@@deriving sexp,hash,compare] type strategy = Rewrite.strategy diff --git a/serlib/plugins/ltac/ser_rewrite.mli b/serlib/plugins/ltac/ser_rewrite.mli index a30069de..94a72e9a 100644 --- a/serlib/plugins/ltac/ser_rewrite.mli +++ b/serlib/plugins/ltac/ser_rewrite.mli @@ -19,7 +19,7 @@ type unary_strategy = Rewrite.unary_strategy type binary_strategy = Rewrite.binary_strategy [@@deriving sexp, hash, compare] -type ('a,'b) strategy_ast = ('a,'b) Rewrite.strategy_ast +type ('a,'b,'c) strategy_ast = ('a,'b,'c) Rewrite.strategy_ast [@@deriving sexp, hash, compare] type strategy = Rewrite.strategy diff --git a/serlib/plugins/ltac/ser_tacarg.ml b/serlib/plugins/ltac/ser_tacarg.ml index c7bad3f6..dee6a84a 100644 --- a/serlib/plugins/ltac/ser_tacarg.ml +++ b/serlib/plugins/ltac/ser_tacarg.ml @@ -275,17 +275,17 @@ let wit_rewstrategy = Ltac_plugin.G_rewrite.wit_rewstrategy module GT2 = struct type raw = - [%import: Ltac_plugin.G_rewrite.raw_strategy] + [%import: Ltac_plugin.Tacexpr.raw_strategy] [@@deriving sexp,hash,compare] type glb = - [%import: Ltac_plugin.G_rewrite.glob_strategy] + [%import: Ltac_plugin.Tacexpr.glob_strategy] [@@deriving sexp,hash,compare] type top = Ltac_plugin.Rewrite.strategy [@@deriving sexp,hash,compare] end -(* (G_rewrite.raw_strategy, G_rewrite.glob_strategy, Rewrite.strategy) *) +(* (Tacexpr.raw_strategy, Tacexpr.glob_strategy, Rewrite.strategy) *) let ser_wit_rewstrategy = let module M = Ser_genarg.GS(GT2) in M.genser From 06093b0182389195835797070aae44e9909ff9ce Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Thu, 14 Dec 2023 17:33:23 +0100 Subject: [PATCH 6/9] Adapt to coq/coq#18327 (projection opacity) --- serlib/plugins/ltac/ser_tacexpr.ml | 29 ++++++++++++++--------------- serlib/ser_genredexpr.ml | 5 ++--- serlib/ser_names.ml | 8 +++++--- serlib/ser_names.mli | 2 ++ serlib/ser_tacred.ml | 24 ------------------------ 5 files changed, 23 insertions(+), 45 deletions(-) delete mode 100644 serlib/ser_tacred.ml diff --git a/serlib/plugins/ltac/ser_tacexpr.ml b/serlib/plugins/ltac/ser_tacexpr.ml index b56755ef..d8c73b59 100644 --- a/serlib/plugins/ltac/ser_tacexpr.ml +++ b/serlib/plugins/ltac/ser_tacexpr.ml @@ -44,7 +44,6 @@ module Goal_select = Ser_goal_select module Pattern = Ser_pattern module Constrexpr = Ser_constrexpr module Vernacexpr = Ser_vernacexpr -module Tacred = Ser_tacred module Tactypes = Ser_tactypes module Tactics = Ser_tactics module Equality = Ser_equality @@ -509,7 +508,7 @@ let rec glob_tactic_expr_of_sexp tac = Genintern.glob_constr_and_expr_of_sexp Genintern.glob_constr_and_expr_of_sexp Genintern.glob_constr_pattern_and_expr_of_sexp - (Locus.or_var_of_sexp (Genredexpr.and_short_name_of_sexp Tacred.evaluable_global_reference_of_sexp)) + (Locus.or_var_of_sexp (Genredexpr.and_short_name_of_sexp Names.Evaluable.t_of_sexp)) (Locus.or_var_of_sexp (Loc.located_of_sexp ltac_constant_of_sexp)) Names.lident_of_sexp glob_tactic_expr_of_sexp @@ -520,7 +519,7 @@ and glob_atomic_tactic_expr_of_sexp tac = Genintern.glob_constr_and_expr_of_sexp Genintern.glob_constr_and_expr_of_sexp Genintern.glob_constr_pattern_and_expr_of_sexp - (Locus.or_var_of_sexp (Genredexpr.and_short_name_of_sexp Tacred.evaluable_global_reference_of_sexp)) + (Locus.or_var_of_sexp (Genredexpr.and_short_name_of_sexp Names.Evaluable.t_of_sexp)) (Locus.or_var_of_sexp (Loc.located_of_sexp ltac_constant_of_sexp)) Names.lident_of_sexp glob_tactic_expr_of_sexp @@ -531,7 +530,7 @@ let rec sexp_of_glob_tactic_expr (tac : glob_tactic_expr) = Genintern.sexp_of_glob_constr_and_expr Genintern.sexp_of_glob_constr_and_expr Genintern.sexp_of_glob_constr_pattern_and_expr - (Locus.sexp_of_or_var (Genredexpr.sexp_of_and_short_name Tacred.sexp_of_evaluable_global_reference)) + (Locus.sexp_of_or_var (Genredexpr.sexp_of_and_short_name Names.Evaluable.sexp_of_t)) (Locus.sexp_of_or_var (Loc.sexp_of_located sexp_of_ltac_constant)) Names.sexp_of_lident sexp_of_glob_tactic_expr @@ -542,7 +541,7 @@ and sexp_of_glob_atomic_tactic_expr (tac : glob_atomic_tactic_expr) = Genintern.sexp_of_glob_constr_and_expr Genintern.sexp_of_glob_constr_and_expr Genintern.sexp_of_glob_constr_pattern_and_expr - (Locus.sexp_of_or_var (Genredexpr.sexp_of_and_short_name Tacred.sexp_of_evaluable_global_reference)) + (Locus.sexp_of_or_var (Genredexpr.sexp_of_and_short_name Names.Evaluable.sexp_of_t)) (Locus.sexp_of_or_var (Loc.sexp_of_located sexp_of_ltac_constant)) Names.sexp_of_lident sexp_of_glob_tactic_expr @@ -555,7 +554,7 @@ let rec glob_tactic_expr_of_yojson tac = Genintern.glob_constr_and_expr_of_yojson Genintern.glob_constr_and_expr_of_yojson Genintern.glob_constr_pattern_and_expr_of_yojson - (Locus.or_var_of_yojson (Genredexpr.and_short_name_of_yojson Tacred.evaluable_global_reference_of_yojson)) + (Locus.or_var_of_yojson (Genredexpr.and_short_name_of_yojson Names.Evaluable.of_yojson)) (Locus.or_var_of_yojson (Loc.located_of_yojson ltac_constant_of_yojson)) Names.lident_of_yojson glob_tactic_expr_of_yojson @@ -566,7 +565,7 @@ and glob_atomic_tactic_expr_of_yojson tac = Genintern.glob_constr_and_expr_of_yojson Genintern.glob_constr_and_expr_of_yojson Genintern.glob_constr_pattern_and_expr_of_yojson - (Locus.or_var_of_yojson (Genredexpr.and_short_name_of_yojson Tacred.evaluable_global_reference_of_yojson)) + (Locus.or_var_of_yojson (Genredexpr.and_short_name_of_yojson Names.Evaluable.of_yojson)) (Locus.or_var_of_yojson (Loc.located_of_yojson ltac_constant_of_yojson)) Names.lident_of_yojson glob_tactic_expr_of_yojson @@ -577,7 +576,7 @@ let rec glob_tactic_expr_to_yojson tac = Genintern.glob_constr_and_expr_to_yojson Genintern.glob_constr_and_expr_to_yojson Genintern.glob_constr_pattern_and_expr_to_yojson - (Locus.or_var_to_yojson (Genredexpr.and_short_name_to_yojson Tacred.evaluable_global_reference_to_yojson)) + (Locus.or_var_to_yojson (Genredexpr.and_short_name_to_yojson Names.Evaluable.to_yojson)) (Locus.or_var_to_yojson (Loc.located_to_yojson ltac_constant_to_yojson)) Names.lident_to_yojson glob_tactic_expr_to_yojson @@ -588,7 +587,7 @@ and glob_atomic_tactic_expr_to_yojson tac = Genintern.glob_constr_and_expr_to_yojson Genintern.glob_constr_and_expr_to_yojson Genintern.glob_constr_pattern_and_expr_to_yojson - (Locus.or_var_to_yojson (Genredexpr.and_short_name_to_yojson Tacred.evaluable_global_reference_to_yojson)) + (Locus.or_var_to_yojson (Genredexpr.and_short_name_to_yojson Names.Evaluable.to_yojson)) (Locus.or_var_to_yojson (Loc.located_to_yojson ltac_constant_to_yojson)) Names.lident_to_yojson glob_tactic_expr_to_yojson @@ -600,7 +599,7 @@ let rec hash_fold_glob_tactic_expr st tac = Genintern.hash_fold_glob_constr_and_expr Genintern.hash_fold_glob_constr_and_expr Genintern.hash_fold_glob_constr_pattern_and_expr - (Locus.hash_fold_or_var (Genredexpr.hash_fold_and_short_name Tacred.hash_fold_evaluable_global_reference)) + (Locus.hash_fold_or_var (Genredexpr.hash_fold_and_short_name Names.Evaluable.hash_fold_t)) (Locus.hash_fold_or_var (Loc.hash_fold_located hash_fold_ltac_constant)) Names.hash_fold_lident hash_fold_glob_tactic_expr @@ -611,7 +610,7 @@ and hash_fold_glob_atomic_tactic_expr st tac = Genintern.hash_fold_glob_constr_and_expr Genintern.hash_fold_glob_constr_and_expr Genintern.hash_fold_glob_constr_pattern_and_expr - (Locus.hash_fold_or_var (Genredexpr.hash_fold_and_short_name Tacred.hash_fold_evaluable_global_reference)) + (Locus.hash_fold_or_var (Genredexpr.hash_fold_and_short_name Names.Evaluable.hash_fold_t)) (Locus.hash_fold_or_var (Loc.hash_fold_located hash_fold_ltac_constant)) Names.hash_fold_lident hash_fold_glob_tactic_expr @@ -626,7 +625,7 @@ let rec compare_glob_tactic_expr tac = Genintern.compare_glob_constr_and_expr Genintern.compare_glob_constr_and_expr Genintern.compare_glob_constr_pattern_and_expr - (Locus.compare_or_var (Genredexpr.compare_and_short_name Tacred.compare_evaluable_global_reference)) + (Locus.compare_or_var (Genredexpr.compare_and_short_name Names.Evaluable.compare)) (Locus.compare_or_var (Loc.compare_located compare_ltac_constant)) Names.compare_lident compare_glob_tactic_expr @@ -637,7 +636,7 @@ and compare_glob_atomic_tactic_expr tac = Genintern.compare_glob_constr_and_expr Genintern.compare_glob_constr_and_expr Genintern.compare_glob_constr_pattern_and_expr - (Locus.compare_or_var (Genredexpr.compare_and_short_name Tacred.compare_evaluable_global_reference)) + (Locus.compare_or_var (Genredexpr.compare_and_short_name Names.Evaluable.compare)) (Locus.compare_or_var (Loc.compare_located compare_ltac_constant)) Names.compare_lident compare_glob_tactic_expr @@ -798,7 +797,7 @@ let atomic_tactic_expr_of_sexp tac = EConstr.t_of_sexp Genintern.glob_constr_and_expr_of_sexp Pattern.constr_pattern_of_sexp - Tacred.evaluable_global_reference_of_sexp + Names.Evaluable.t_of_sexp (Loc.located_of_sexp ltac_constant_of_sexp) Names.Id.t_of_sexp unit_of_sexp @@ -809,7 +808,7 @@ let sexp_of_atomic_tactic_expr tac = EConstr.sexp_of_t Genintern.sexp_of_glob_constr_and_expr Pattern.sexp_of_constr_pattern - Tacred.sexp_of_evaluable_global_reference + Names.Evaluable.sexp_of_t (Loc.sexp_of_located sexp_of_ltac_constant) Names.Id.sexp_of_t sexp_of_unit diff --git a/serlib/ser_genredexpr.ml b/serlib/ser_genredexpr.ml index 36585cbc..d3a39651 100644 --- a/serlib/ser_genredexpr.ml +++ b/serlib/ser_genredexpr.ml @@ -24,7 +24,6 @@ module Locus = Ser_locus module Libnames = Ser_libnames module Constrexpr = Ser_constrexpr module Genintern = Ser_genintern -module Tacred = Ser_tacred type 'a red_atom = [%import: 'a Genredexpr.red_atom] @@ -99,13 +98,13 @@ module A = struct type glb = (Ser_genintern.glob_constr_and_expr, - Ser_tacred.evaluable_global_reference and_short_name Ser_locus.or_var, + Ser_names.Evaluable.t and_short_name Ser_locus.or_var, Ser_genintern.glob_constr_pattern_and_expr) red_expr_gen [@@deriving sexp,yojson,hash,compare] type top = (Ser_eConstr.constr, - Ser_tacred.evaluable_global_reference, + Ser_names.Evaluable.t, Ser_pattern.constr_pattern) red_expr_gen [@@deriving sexp,yojson,hash,compare] end diff --git a/serlib/ser_names.ml b/serlib/ser_names.ml index 82d2e70a..6626ca73 100644 --- a/serlib/ser_names.ml +++ b/serlib/ser_names.ml @@ -267,9 +267,11 @@ type t = [%import: Names.GlobRef.t] end (* Evaluable global reference: public *) -(* type evaluable_global_reference = - * [%import: Names.evaluable_global_reference] - * [@@deriving sexp] *) +module Evaluable = struct + type t = + [%import: Names.Evaluable.t] + [@@deriving sexp,yojson,hash,compare] +end type lident = [%import: Names.lident] diff --git a/serlib/ser_names.mli b/serlib/ser_names.mli index 5fc08930..5db23584 100644 --- a/serlib/ser_names.mli +++ b/serlib/ser_names.mli @@ -74,6 +74,8 @@ end module GlobRef : SerType.SJHC with type t = Names.GlobRef.t +module Evaluable : SerType.SJHC with type t = Names.Evaluable.t + type lident = Names.lident [@@deriving sexp,yojson,hash,compare] type lname = Names.lname [@@deriving sexp,yojson,hash,compare] type lstring = Names.lstring [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_tacred.ml b/serlib/ser_tacred.ml deleted file mode 100644 index 4a0a0f4e..00000000 --- a/serlib/ser_tacred.ml +++ /dev/null @@ -1,24 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Date: Fri, 19 Jan 2024 17:27:31 +0100 Subject: [PATCH 7/9] [serlib] Expose some more functions related to Require's AST. --- CHANGES.md | 7 +- serlib/ser_vernacexpr.mli | 336 ++++++++++++++++++-------------------- 2 files changed, 162 insertions(+), 181 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index add23705..779a68ab 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,6 @@ ## unreleased - - [general] Cleanup old / unused code (@ejgallego, #) + - [general] Cleanup old / unused code (@ejgallego, #362) ## Version 0.18.1: @@ -14,6 +14,11 @@ - [serlib] Fix ltac2 plugin wrong piercing due to missing constructor (@ejgallego, reported by @quarkcool, #349). +## Version 0.17.2: + + - [serlib] Expose some more Ast functions required by coq-lsp's + auto-build support (@ejgallego, #383) + ## Version 0.17.1: - [sertop] Don't initialize `CoqworkmgrApi` (@ejgallego, #340) diff --git a/serlib/ser_vernacexpr.mli b/serlib/ser_vernacexpr.mli index 4efe7368..0be9968d 100644 --- a/serlib/ser_vernacexpr.mli +++ b/serlib/ser_vernacexpr.mli @@ -13,301 +13,277 @@ (* Status: Very Experimental *) (************************************************************************) -open Sexplib - type infix_flag = [%import: Vernacexpr.infix_flag] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] + +type opacity_flag = + [%import: Vernacexpr.opacity_flag] + [@@deriving sexp,yojson,hash,compare] type scope_name = [%import: Vernacexpr.scope_name] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type scope_delimiter = [%import: Vernacexpr.scope_delimiter] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type notation_format = [%import: Vernacexpr.notation_format] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type syntax_modifier = [%import: Vernacexpr.syntax_modifier] - [@@deriving sexp,yojson] - -type coercion_class = Vernacexpr.coercion_class -val coercion_class_of_sexp : Sexp.t -> coercion_class -val sexp_of_coercion_class : coercion_class -> Sexp.t - -(* type goal_identifier = Vernacexpr.goal_identifier - * val goal_identifier_of_sexp : Sexp.t -> goal_identifier - * val sexp_of_goal_identifier : goal_identifier -> Sexp.t *) - -type goal_reference = Vernacexpr.goal_reference -val goal_reference_of_sexp : Sexp.t -> goal_reference -val sexp_of_goal_reference : goal_reference -> Sexp.t - -type printable = Vernacexpr.printable -val printable_of_sexp : Sexp.t -> printable -val sexp_of_printable : printable -> Sexp.t - -type search_item = Vernacexpr.search_item -val search_item_of_sexp : Sexp.t -> search_item -val sexp_of_search_item : search_item -> Sexp.t - -type searchable = Vernacexpr.searchable -val searchable_of_sexp : Sexp.t -> searchable -val sexp_of_searchable : searchable -> Sexp.t - -type locatable = Vernacexpr.locatable -val locatable_of_sexp : Sexp.t -> locatable -val sexp_of_locatable : locatable -> Sexp.t - -type showable = Vernacexpr.showable -val showable_of_sexp : Sexp.t -> showable -val sexp_of_showable : showable -> Sexp.t - -type comment = Vernacexpr.comment -val comment_of_sexp : Sexp.t -> comment -val sexp_of_comment : comment -> Sexp.t - -type 'a search_restriction = 'a Vernacexpr.search_restriction -val search_restriction_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a search_restriction -val sexp_of_search_restriction : ('a -> Sexp.t) -> 'a search_restriction -> Sexp.t - -(* type rec_flag = Vernacexpr.rec_flag - * val rec_flag_of_sexp : Sexp.t -> rec_flag - * val sexp_of_rec_flag : rec_flag -> Sexp.t *) - -type verbose_flag = Vernacexpr.verbose_flag -val verbose_flag_of_sexp : Sexp.t -> verbose_flag -val sexp_of_verbose_flag : verbose_flag -> Sexp.t - -type coercion_flag = Vernacexpr.coercion_flag -val coercion_flag_of_sexp : Sexp.t -> coercion_flag -val sexp_of_coercion_flag : coercion_flag -> Sexp.t - -(* type inductive_flag = Vernacexpr.inductive_flag - * val inductive_flag_of_sexp : Sexp.t -> inductive_flag - * val sexp_of_inductive_flag : inductive_flag -> Sexp.t *) + [@@deriving sexp,yojson,hash,compare] -type instance_flag = Vernacexpr.instance_flag -val instance_flag_of_sexp : Sexp.t -> instance_flag -val sexp_of_instance_flag : instance_flag -> Sexp.t +type coercion_class = + [%import: Vernacexpr.coercion_class] + [@@deriving sexp,yojson,hash,compare] -type export_flag = Vernacexpr.export_flag -val export_flag_of_sexp : Sexp.t -> export_flag -val sexp_of_export_flag : export_flag -> Sexp.t +type goal_reference = + [%import: Vernacexpr.goal_reference] + [@@deriving sexp,yojson,hash,compare] -(* type onlyparsing_flag = Vernacexpr.onlyparsing_flag - * val onlyparsing_flag_of_sexp : Sexp.t -> onlyparsing_flag - * val sexp_of_onlyparsing_flag : onlyparsing_flag -> Sexp.t *) +type printable = + [%import: Vernacexpr.printable] + [@@deriving sexp,yojson,hash,compare] -type locality_flag = Vernacexpr.locality_flag -val locality_flag_of_sexp : Sexp.t -> locality_flag -val sexp_of_locality_flag : locality_flag -> Sexp.t +type glob_search_where = + [%import: Vernacexpr.glob_search_where] + [@@deriving sexp,yojson,hash,compare] -(* type obsolete_locality = Vernacexpr.obsolete_locality - * val obsolete_locality_of_sexp : Sexp.t -> obsolete_locality - * val sexp_of_obsolete_locality : obsolete_locality -> Sexp.t *) +type search_item = + [%import: Vernacexpr.search_item] + [@@deriving sexp,yojson,hash,compare] -(* type option_value = Vernacexpr.option_value - * val option_value_of_sexp : Sexp.t -> option_value - * val sexp_of_option_value : option_value -> Sexp.t *) +type search_request = + [%import: Vernacexpr.search_request] + [@@deriving sexp,yojson,hash,compare] -(* type option_ref_value = Vernacexpr.option_ref_value - * val option_ref_value_of_sexp : Sexp.t -> option_ref_value - * val sexp_of_option_ref_value : option_ref_value -> Sexp.t *) +type searchable = + [%import: Vernacexpr.searchable] + [@@deriving sexp,yojson,hash,compare] -(* type plident = Vernacexpr.plident - * val plident_of_sexp : Sexp.t -> plident - * val sexp_of_plident : plident -> Sexp.t *) +type locatable = + [%import: Vernacexpr.locatable] + [@@deriving sexp,yojson,hash,compare] -(* type sort_expr = Vernacexpr.sort_expr - * val sort_expr_of_sexp : Sexp.t -> sort_expr - * val sexp_of_sort_expr : sort_expr -> Sexp.t *) +type showable = + [%import: Vernacexpr.showable] + [@@deriving sexp,yojson,hash,compare] -type definition_expr = Vernacexpr.definition_expr -val definition_expr_of_sexp : Sexp.t -> definition_expr -val sexp_of_definition_expr : definition_expr -> Sexp.t +type comment = + [%import: Vernacexpr.comment] + [@@deriving sexp,yojson,hash,compare] -type fixpoint_expr = Vernacexpr.fixpoint_expr - [@@deriving sexp,hash,compare] +type 'a search_restriction = + [%import: 'a Vernacexpr.search_restriction] + [@@deriving sexp,yojson,hash,compare] -type cofixpoint_expr = Vernacexpr.cofixpoint_expr -val cofixpoint_expr_of_sexp : Sexp.t -> cofixpoint_expr -val sexp_of_cofixpoint_expr : cofixpoint_expr -> Sexp.t +type verbose_flag = + [%import: Vernacexpr.verbose_flag] + [@@deriving sexp,yojson,hash,compare] -type local_decl_expr = Vernacexpr.local_decl_expr -val local_decl_expr_of_sexp : Sexp.t -> local_decl_expr -val sexp_of_local_decl_expr : local_decl_expr -> Sexp.t +type coercion_flag = + [%import: Vernacexpr.coercion_flag] + [@@deriving sexp,yojson,hash,compare] -type inductive_kind = Vernacexpr.inductive_kind -val inductive_kind_of_sexp : Sexp.t -> inductive_kind -val sexp_of_inductive_kind : inductive_kind -> Sexp.t +type instance_flag = + [%import: Vernacexpr.instance_flag] + [@@deriving sexp,yojson,hash,compare] -type notation_declaration = Vernacexpr.notation_declaration -val notation_declaration_of_sexp : Sexp.t -> notation_declaration -val sexp_of_notation_declaration : notation_declaration -> Sexp.t +type export_flag = + [%import: Vernacexpr.export_flag] + [@@deriving sexp,yojson,hash,compare] -type simple_binder = Vernacexpr.simple_binder -val simple_binder_of_sexp : Sexp.t -> simple_binder -val sexp_of_simple_binder : simple_binder -> Sexp.t +type locality_flag = + [%import: Vernacexpr.locality_flag] + [@@deriving sexp,yojson,hash,compare] -type class_binder = Vernacexpr.class_binder +type definition_expr = + [%import: Vernacexpr.definition_expr] + [@@deriving sexp,yojson,hash,compare] -val class_binder_of_sexp : Sexp.t -> class_binder -val sexp_of_class_binder : class_binder -> Sexp.t +type notation_declaration = + [%import: Vernacexpr.notation_declaration] + [@@deriving sexp,yojson,hash,compare] -type 'a with_coercion = 'a Vernacexpr.with_coercion +type 'a fix_expr_gen = + [%import: 'a Vernacexpr.fix_expr_gen] + [@@deriving sexp,yojson,hash,compare] -val with_coercion_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a with_coercion -val sexp_of_with_coercion : ('a -> Sexp.t) -> 'a with_coercion -> Sexp.t +type fixpoint_expr = + [%import: Vernacexpr.fixpoint_expr] + [@@deriving sexp,yojson,hash,compare] -type constructor_expr = Vernacexpr.constructor_expr -val constructor_expr_of_sexp : Sexp.t -> constructor_expr -val sexp_of_constructor_expr : constructor_expr -> Sexp.t +type cofixpoint_expr = + [%import: Vernacexpr.cofixpoint_expr] + [@@deriving sexp,yojson,hash,compare] -type constructor_list_or_record_decl_expr = Vernacexpr.constructor_list_or_record_decl_expr +type local_decl_expr = + [%import: Vernacexpr.local_decl_expr] + [@@deriving sexp,yojson,hash,compare] -val constructor_list_or_record_decl_expr_of_sexp : - Sexp.t -> constructor_list_or_record_decl_expr -val sexp_of_constructor_list_or_record_decl_expr : - constructor_list_or_record_decl_expr -> Sexp.t +type inductive_kind = + [%import: Vernacexpr.inductive_kind] + [@@deriving sexp,yojson,hash,compare] -type inductive_expr = Vernacexpr.inductive_expr +type simple_binder = + [%import: Vernacexpr.simple_binder] + [@@deriving sexp,yojson,hash,compare] -val inductive_expr_of_sexp : Sexp.t -> inductive_expr -val sexp_of_inductive_expr : inductive_expr -> Sexp.t +type class_binder = + [%import: Vernacexpr.class_binder] + [@@deriving sexp,yojson,hash,compare] -type one_inductive_expr = Vernacexpr.one_inductive_expr +type 'a with_coercion = + [%import: 'a Vernacexpr.with_coercion] + [@@deriving sexp,yojson,hash,compare] -val one_inductive_expr_of_sexp : Sexp.t -> one_inductive_expr -val sexp_of_one_inductive_expr : one_inductive_expr -> Sexp.t +type 'a with_coercion_instance = + [%import: 'a Vernacexpr.with_coercion_instance] + [@@deriving sexp,yojson,hash,compare] -type proof_expr = Vernacexpr.proof_expr +type constructor_expr = + [%import: Vernacexpr.constructor_expr] + [@@deriving sexp,yojson,hash,compare] -val proof_expr_of_sexp : Sexp.t -> proof_expr -val sexp_of_proof_expr : proof_expr -> Sexp.t +type record_field_attr_unparsed = + [%import: Vernacexpr.record_field_attr_unparsed] + [@@deriving sexp,yojson,hash,compare] -(* type grammar_tactic_prod_item_expr = Vernacexpr.grammar_tactic_prod_item_expr *) -(* val grammar_tactic_prod_item_expr_of_sexp : Sexp.t -> grammar_tactic_prod_item_expr *) -(* val sexp_of_grammar_tactic_prod_item_expr : grammar_tactic_prod_item_expr -> Sexp.t *) +type constructor_list_or_record_decl_expr = + [%import: Vernacexpr.constructor_list_or_record_decl_expr] + [@@deriving sexp,yojson,hash,compare] -(* type syntax_modifier = Vernacexpr.syntax_modifier *) +type inductive_params_expr = + [%import: Vernacexpr.inductive_params_expr] + [@@deriving sexp,yojson,hash,compare] -(* val syntax_modifier_of_sexp : Sexp.t -> syntax_modifier *) -(* val sexp_of_syntax_modifier : syntax_modifier -> Sexp.t *) +type inductive_expr = + [%import: Vernacexpr.inductive_expr] + [@@deriving sexp,yojson,hash,compare] -type proof_end = Vernacexpr.proof_end -val proof_end_of_sexp : Sexp.t -> proof_end -val sexp_of_proof_end : proof_end -> Sexp.t +type one_inductive_expr = + [%import: Vernacexpr.one_inductive_expr] + [@@deriving sexp,yojson,hash,compare] -type scheme = Vernacexpr.scheme -val scheme_of_sexp : Sexp.t -> scheme -val sexp_of_scheme : scheme -> Sexp.t +type proof_expr = + [%import: Vernacexpr.proof_expr] + [@@deriving sexp,yojson,hash,compare] -type section_subset_expr = Vernacexpr.section_subset_expr -val section_subset_expr_of_sexp : Sexp.t -> section_subset_expr -val sexp_of_section_subset_expr : section_subset_expr -> Sexp.t +type proof_end = + [%import: Vernacexpr.proof_end] + [@@deriving sexp,yojson,hash,compare] -type extend_name = Vernacexpr.extend_name -val extend_name_of_sexp : Sexp.t -> extend_name -val sexp_of_extend_name : extend_name -> Sexp.t +type scheme_type = + [%import: Vernacexpr.scheme_type] + [@@deriving sexp,yojson,hash,compare] -type register_kind = Vernacexpr.register_kind -val register_kind_of_sexp : Sexp.t -> register_kind -val sexp_of_register_kind : register_kind -> Sexp.t +type scheme = + [%import: Vernacexpr.scheme] + [@@deriving sexp,yojson,hash,compare] -type module_ast_inl = Vernacexpr.module_ast_inl +type section_subset_expr = + [%import: Vernacexpr.section_subset_expr] + [@@deriving sexp,yojson,hash,compare] -val module_ast_inl_of_sexp : Sexp.t -> module_ast_inl -val sexp_of_module_ast_inl : module_ast_inl -> Sexp.t +type extend_name = + [%import: Vernacexpr.extend_name] + [@@deriving sexp,yojson,hash,compare] -type module_binder = Vernacexpr.module_binder +type register_kind = + [%import: Vernacexpr.register_kind] + [@@deriving sexp,yojson,hash,compare] -val module_binder_of_sexp : Sexp.t -> module_binder -val sexp_of_module_binder : module_binder -> Sexp.t +type module_ast_inl = + [%import: Vernacexpr.module_ast_inl] + [@@deriving sexp,yojson,hash,compare] type discharge = [%import: Vernacexpr.discharge] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type equality_scheme_type = [%import: Vernacexpr.equality_scheme_type] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type import_categories = [%import: Vernacexpr.import_categories] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type export_with_cats = [%import: Vernacexpr.export_with_cats] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] + +type module_binder = + [%import: Vernacexpr.module_binder] + [@@deriving sexp,yojson,hash,compare] type one_import_filter_name = [%import: Vernacexpr.one_import_filter_name] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type import_filter_expr = [%import: Vernacexpr.import_filter_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type hint_info_expr = [%import: Vernacexpr.hint_info_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type reference_or_constr = [%import: Vernacexpr.reference_or_constr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type hints_expr = [%import: Vernacexpr.hints_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type vernac_one_argument_status = [%import: Vernacexpr.vernac_one_argument_status] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type vernac_argument_status = [%import: Vernacexpr.vernac_argument_status] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type arguments_modifier = [%import: Vernacexpr.arguments_modifier] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type option_setting = [%import: Vernacexpr.option_setting] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type notation_enable_modifier = [%import: Vernacexpr.notation_enable_modifier] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson,hash,compare] type synterp_vernac_expr = [%import: Vernacexpr.synterp_vernac_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type synpure_vernac_expr = [%import: Vernacexpr.synpure_vernac_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type 'a vernac_expr_gen = [%import: 'a Vernacexpr.vernac_expr_gen] - [@@deriving sexp, yojson] + [@@deriving sexp,yojson,hash,compare] type control_flag = [%import: Vernacexpr.control_flag] - [@@deriving sexp, yojson] + [@@deriving sexp,yojson,hash,compare] type ('a, 'b) vernac_control_gen_r = [%import: ('a, 'b) Vernacexpr.vernac_control_gen_r] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type 'a vernac_control_gen = [%import: 'a Vernacexpr.vernac_control_gen] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type vernac_control = [%import: Vernacexpr.vernac_control] From 97edccb51a4132f34d9e16cca9370d4f00bc6b60 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Jan 2024 20:49:44 +0100 Subject: [PATCH 8/9] [ci] Remove obsolete pin on dune for Coq git build --- .github/workflows/ci.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index df73122e..40d889b9 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -84,7 +84,6 @@ jobs: if: ${{ matrix.coq-from-git }} run: | eval $(opam env) - opam pin add -k version dune 3.3.1 # First we update SERAPI_COQ_HOME for future steps as per https://docs.github.com/en/actions/reference/workflow-commands-for-github-actions#setting-an-environment-variable echo "SERAPI_COQ_HOME=$HOME/coq-$COQ_BRANCH/_build/install/default/lib/" >> $GITHUB_ENV # Update to coq-core some day From 2cf89c3e3cfd9a4f86abfbff36ce095f70b0a5fa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 23 Jan 2024 13:38:47 +0100 Subject: [PATCH 9/9] Adapt to coq/coq#18528 (profile_ltac moved to engine and renamed profile_tactic) --- serapi/serapi_protocol.ml | 4 ++-- serapi/serapi_protocol.mli | 2 +- .../ltac/ser_profile_ltac.ml => ser_profile_tactic.ml} | 2 +- .../ltac/ser_profile_ltac.mli => ser_profile_tactic.mli} | 4 +--- sertop/sertop_ser.ml | 2 +- 5 files changed, 6 insertions(+), 8 deletions(-) rename serlib/{plugins/ltac/ser_profile_ltac.ml => ser_profile_tactic.ml} (97%) rename serlib/{plugins/ltac/ser_profile_ltac.mli => ser_profile_tactic.mli} (95%) diff --git a/serapi/serapi_protocol.ml b/serapi/serapi_protocol.ml index c75671d0..a0c8d8e3 100644 --- a/serapi/serapi_protocol.ml +++ b/serapi/serapi_protocol.ml @@ -130,7 +130,7 @@ type coq_object = | CoqGlobRef of Names.GlobRef.t | CoqGlobRefExt of Globnames.extended_global_reference | CoqImplicit of Impargs.implicits_list - | CoqProfData of Profile_ltac.treenode + | CoqProfData of Profile_tactic.treenode | CoqNotation of Constrexpr.notation | CoqUnparsing of Ppextend.notation_printing_rules * Notation_gram.notation_grammar | CoqGoal of Constr.t Serapi_goals.reified_goal Serapi_goals.ser_goals @@ -600,7 +600,7 @@ let obj_query ~doc ~pstate ~env (opt : query_opt) (cmd : query_cmd) : coq_object | Tactics prefix -> List.map (fun (i,t) -> CoqTactic(i,t)) @@ QueryUtil.query_tactics prefix | Locate id -> List.map (fun qid -> CoqQualId qid) @@ QueryUtil.locate id | Implicits id -> List.map (fun ii -> CoqImplicit ii ) @@ QueryUtil.implicits id - | ProfileData -> [CoqProfData (Profile_ltac.get_local_profiling_results ())] + | ProfileData -> [CoqProfData (Profile_tactic.get_local_profiling_results ())] | Proof -> QueryUtil.get_proof ~pstate | Unparsing ntn -> (* Unfortunately this will produce an anomaly if the notation is not found... * To keep protocol promises we need to special wrap it. diff --git a/serapi/serapi_protocol.mli b/serapi/serapi_protocol.mli index 036e93d4..ebc9aa29 100644 --- a/serapi/serapi_protocol.mli +++ b/serapi/serapi_protocol.mli @@ -215,7 +215,7 @@ type coq_object = (** "Extended Global Reference", as they can contain syntactic definitions too *) | CoqImplicit of Impargs.implicits_list (** Implicit status for a constant *) - | CoqProfData of Profile_ltac.treenode + | CoqProfData of Profile_tactic.treenode (** Ltac Profiler data *) | CoqNotation of Constrexpr.notation (** Representation of a notation (usually a string) *) diff --git a/serlib/plugins/ltac/ser_profile_ltac.ml b/serlib/ser_profile_tactic.ml similarity index 97% rename from serlib/plugins/ltac/ser_profile_ltac.ml rename to serlib/ser_profile_tactic.ml index cb325573..c2e75ee6 100644 --- a/serlib/plugins/ltac/ser_profile_ltac.ml +++ b/serlib/ser_profile_tactic.ml @@ -33,7 +33,7 @@ let sexp_of_cstring_map f m = sexp_of_list s_f l type treenode = - [%import: Ltac_plugin.Profile_ltac.treenode + [%import: Profile_tactic.treenode [@with CString.Map.t := cstring_map; CString.Map.key := string ]] diff --git a/serlib/plugins/ltac/ser_profile_ltac.mli b/serlib/ser_profile_tactic.mli similarity index 95% rename from serlib/plugins/ltac/ser_profile_ltac.mli rename to serlib/ser_profile_tactic.mli index 2dc8b7eb..4966b41e 100644 --- a/serlib/plugins/ltac/ser_profile_ltac.mli +++ b/serlib/ser_profile_tactic.mli @@ -15,9 +15,7 @@ open Sexplib -open Ltac_plugin - -type treenode = Profile_ltac.treenode +type treenode = Profile_tactic.treenode val treenode_of_sexp : Sexp.t -> treenode val sexp_of_treenode : treenode -> Sexp.t diff --git a/sertop/sertop_ser.ml b/sertop/sertop_ser.ml index 8d3ce762..fb73d540 100644 --- a/sertop/sertop_ser.ml +++ b/sertop/sertop_ser.ml @@ -100,6 +100,7 @@ module Notation_gram = Ser_notation_gram module Genarg = Ser_genarg module Loadpath = Ser_loadpath module Printer = Ser_printer +module Profile_tactic = Ser_profile_tactic (* Alias fails due to the [@@default in protocol] *) (* module Stm = Ser_stm *) @@ -107,7 +108,6 @@ module Ser_stm = Ser_stm module Ltac_plugin = struct module Tacenv = Serlib_ltac.Ser_tacenv - module Profile_ltac = Serlib_ltac.Ser_profile_ltac module Tacexpr = Serlib_ltac.Ser_tacexpr end