From 2c3ffa44414840ae51508508175d296004f12038 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Sun, 4 Dec 2022 00:01:37 +0100 Subject: [PATCH 01/35] Adapt w.r.t. coq/coq#16933. --- src/coq_elpi_HOAS.ml | 2 +- src/coq_elpi_builtins.ml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 79d853dc2..3b1a9866a 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -1728,7 +1728,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals match E.look ~depth t with | E.App(s,p,[]) when sortc == s -> let state, u, gsl = sort.API.Conversion.readback ~depth state p in - state, EC.mkSort u, gsl + state, EC.mkSort (EC.ESorts.make u), gsl (* constants *) | E.App(c,d,[]) when globalc == c -> let state, gr = in_coq_gref ~depth ~origin:t ~failsafe:coq_ctx.options.failsafe state d in diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index dc3cd5a91..4c879a033 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -3023,14 +3023,14 @@ Universe constraints are put in the constraint store.|})))), let sigma, s = Typing.sort_of proof_context.env sigma ty in match es with | Data es -> - let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Reduction.CUMUL (EConstr.mkSort s) (EConstr.mkSort es) in + let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Reduction.CUMUL (EConstr.mkSort s) (EConstr.mkSort (EConstr.ESorts.make es)) in let state, assignments = set_current_sigma ~depth state sigma in state, !: es +! B.mkOK, assignments | NoData -> let flags = Evarconv.default_flags_of TransparentState.full in let sigma = Evarconv.solve_unif_constraints_with_heuristics ~flags ~with_ho:true proof_context.env sigma in let state, assignments = set_current_sigma ~depth state sigma in - state, !: s +! B.mkOK, assignments + state, !: (EConstr.ESorts.kind sigma s) +! B.mkOK, assignments with Pretype_errors.PretypeError (env, sigma, err) -> match diag with | Data B.OK -> From e64e4c7e9278d120b462a92a64f07ed798dc8ed0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 7 Dec 2022 16:14:37 +0100 Subject: [PATCH 02/35] Adapt to coq/coq#16938 (staged options) --- src/coq_elpi_builtins.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 1aacc920d..07aa80268 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -923,14 +923,14 @@ let cache_goption_declaration (depr,key,value) = let open Goptions in match value with | BoolValue x -> - let _ : unit -> bool = Goptions.declare_bool_option_and_ref ~key ~value:x ~depr in + let _ : unit -> bool = Goptions.declare_bool_option_and_ref ~stage:Interp ~key ~value:x ~depr in () | IntValue x -> - let _ : unit -> int option = Goptions.declare_intopt_option_and_ref ~key ~depr in + let _ : unit -> int option = Goptions.declare_intopt_option_and_ref ~stage:Interp ~key ~depr in Goptions.set_int_option_value key x; () | StringOptValue x -> - let _ : unit -> string option = Goptions.declare_stringopt_option_and_ref ~key ~depr in + let _ : unit -> string option = Goptions.declare_stringopt_option_and_ref ~stage:Interp ~key ~depr in Option.iter (Goptions.set_string_option_value key) x; () | StringValue _ -> assert false From a615da82cdea00345c1373d332ccf8b9f5e78a39 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Sun, 18 Dec 2022 22:16:45 +0100 Subject: [PATCH 03/35] Adapt w.r.t. coq/coq#17007. --- src/coq_elpi_HOAS.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 3b1a9866a..f71dc3309 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -3378,7 +3378,7 @@ let rec in_elpi_module_item ~depth path state (name, item) = and functor_params x = let open Declarations in match x with - | MoreFunctor(_,{ mod_type_alg = Some (NoFunctor (MEident mod_mp)) },rest) -> mod_mp :: functor_params rest + | MoreFunctor(_,{ mod_type_alg = Some (MENoFunctor (MEident mod_mp)) },rest) -> mod_mp :: functor_params rest | _ -> [] (* XXX non trivial functors, eg P : X with type a = nat, are badly described (no params) *) and in_elpi_module : 'a. depth:int -> API.Data.state -> 'a Declarations.generic_module_body -> module_item list = From 9d2c0de82e4922468cf6560e8a525d28e7f4188d Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Fri, 30 Dec 2022 18:38:18 +0100 Subject: [PATCH 04/35] Adapt to coq/coq#17038 (drop -rectypes flag as coq_makefile default) --- Makefile.coq.local | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile.coq.local b/Makefile.coq.local index de6e205d3..26196d9c9 100644 --- a/Makefile.coq.local +++ b/Makefile.coq.local @@ -1,5 +1,5 @@ CAMLPKGS+= -package elpi,stdlib-shims -CAMLFLAGS+= -bin-annot -g +CAMLFLAGS+= -rectypes -bin-annot -g OCAMLWARN+=-warn-error -32 theories/elpi.vo: $(wildcard elpi/*.elpi) From c40c7a9fb9d7649833d0f5ba9e97c8e89a2b1ddd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Sat, 31 Dec 2022 17:01:09 +0100 Subject: [PATCH 05/35] cache_abbrev_for_tac: use GADT instead of Obj.magic and rectypes --- Makefile.coq.local | 2 +- src/coq_elpi_builtins.ml | 17 +++++++++-------- 2 files changed, 10 insertions(+), 9 deletions(-) diff --git a/Makefile.coq.local b/Makefile.coq.local index 26196d9c9..de6e205d3 100644 --- a/Makefile.coq.local +++ b/Makefile.coq.local @@ -1,5 +1,5 @@ CAMLPKGS+= -package elpi,stdlib-shims -CAMLFLAGS+= -rectypes -bin-annot -g +CAMLFLAGS+= -bin-annot -g OCAMLWARN+=-warn-error -32 theories/elpi.vo: $(wildcard elpi/*.elpi) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 07aa80268..cef28e052 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -859,12 +859,13 @@ type tac_abbrev = { tac_fixed_args : Coq_elpi_arg_HOAS.Tac.glob list; } +type ('a,'d) gbpmp = Gbpmp : ('d, _, 'b, Loc.t -> 'd) Pcoq.Rule.t * ('a -> 'b) -> ('a,'d) gbpmp -let rec gbpmp = fun f -> function - | [x] -> Pcoq.Rule.next Pcoq.Rule.stop (Pcoq.Symbol.token (Tok.PIDENT(Some x))), (fun a _ -> f a) +let rec gbpmp f = function + | [x] -> Gbpmp (Pcoq.Rule.next Pcoq.Rule.stop (Pcoq.Symbol.token (Tok.PIDENT(Some x))), (fun a _ -> f a)) | x :: xs -> - let r, f = gbpmp f xs in - Pcoq.Rule.next r (Pcoq.Symbol.token (Tok.PFIELD (Some x))), (fun a _ -> f a) + let Gbpmp (r, f) = gbpmp f xs in + Gbpmp (Pcoq.Rule.next r (Pcoq.Symbol.token (Tok.PFIELD (Some x))), (fun a _ -> f a)) | [] -> assert false let cache_abbrev_for_tac { abbrev_name; tac_name = tacname; tac_fixed_args = more_args } = @@ -894,12 +895,12 @@ let cache_abbrev_for_tac { abbrev_name; tac_name = tacname; tac_fixed_args = mor let args = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Coq_elpi_arg_syntax.wit_elpi_tactic_arg)) (more_args @ args) in (TacML (elpi_tac_entry, [TacGeneric(None, tacname); TacGeneric(None, args)])) in CAst.make @@ Constrexpr.CHole (None, Namegen.IntroAnonymous, Some (Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) (CAst.make tac))) in - let rule, action = gbpmp (Obj.magic action) (List.rev abbrev_name) in + let Gbpmp (rule, action) = gbpmp action (List.rev abbrev_name) in Pcoq.grammar_extend Pcoq.Constr.term (Pcoq.Fresh (Gramlib.Gramext.Before "10", - [ (None, None, [ Pcoq.Production.make - (Pcoq.Rule.next (Obj.magic rule) (Pcoq.Symbol.list0 (Pcoq.Symbol.nterm Pcoq.Constr.arg))) - (Obj.magic action) + [ (None, None, [ Pcoq.Production.make + (Pcoq.Rule.next rule (Pcoq.Symbol.list0 (Pcoq.Symbol.nterm Pcoq.Constr.arg))) + action ])])) let subst_abbrev_for_tac (subst, { abbrev_name; tac_name; tac_fixed_args }) = { From 45396de82124ce8e68f54134872371d581709dd0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 4 Jan 2023 10:51:04 +0100 Subject: [PATCH 06/35] Adapt w.r.t. coq/coq#17053. --- src/coq_elpi_HOAS.ml | 15 ++++++++------- src/coq_elpi_builtins.ml | 2 +- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index f71dc3309..7688ea5bb 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -1212,7 +1212,8 @@ let restrict_coq_context live_db state { proof; proof_len; local; name2db; env; let info_of_evar ~env ~sigma ~section k = let open Context.Named in - let info = Evarutil.nf_evar_info sigma (Evd.find sigma k) in + let EvarInfo evi = Evd.find sigma k in + let info = Evarutil.nf_evar_info sigma evi in let filtered_hyps = Evd.evar_filtered_hyps info in let ctx = EC.named_context_of_val filtered_hyps in let ctx = ctx |> CList.filter (fun x -> @@ -1495,7 +1496,7 @@ let body_of_constant state c inst_opt = S.update_return engine state (fun x -> | None -> x, (None, None)) |> (fun (x,(y,z)) -> x,y,z) let evar_arity k state = - let info = Evd.find (S.get engine state).sigma k in + let EvarInfo info = Evd.find (S.get engine state).sigma k in let filtered_hyps = Evd.evar_filtered_hyps info in List.length (Environ.named_context_of_val filtered_hyps) @@ -2142,7 +2143,7 @@ let customtac2query sigma goals loc text ~depth:calldepth state = | [] | _ :: _ :: _ -> CErrors.user_err Pp.(str "elpi query can only be used on one goal") | [goal] -> - let info = Evd.find sigma goal in + let EvarInfo info = Evd.find sigma goal in let env = get_global_env state in let env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env in if not (Evd.is_undefined sigma goal) then @@ -2299,9 +2300,9 @@ let get_declared_goals all_goals constraints state assignments pp_ctx = *) let rec reachable1 sigma root acc = - let info = Evd.find sigma root in - let res = if Evd.evar_body info == Evd.Evar_empty then Evar.Set.add root acc else acc in - let res = Evar.Set.union res @@ Evarutil.filtered_undefined_evars_of_evar_info sigma (Evd.find sigma root) in + let EvarInfo info = Evd.find sigma root in + let res = match Evd.evar_body info with Evd.Evar_empty -> Evar.Set.add root acc | Evd.Evar_defined _ -> acc in + let res = Evar.Set.union res @@ Evarutil.filtered_undefined_evars_of_evar_info sigma info in if Evar.Set.equal res acc then acc else reachable sigma res res and reachable sigma roots acc = Evar.Set.fold (reachable1 sigma) roots acc @@ -2347,7 +2348,7 @@ let set_current_sigma ~depth state sigma = let state = set_sigma state sigma in let state, assignments, decls, to_remove_coq, to_remove_elpi = UVMap.fold (fun k elpi_raw_evk elpi_evk solution (state, assignments, decls, to_remove_coq, to_remove_elpi as acc) -> - let info = Evd.find sigma k in + let EvarInfo info = Evd.find sigma k in match Evd.evar_body info with | Evd.Evar_empty -> acc | Evd.Evar_defined c -> diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index cef28e052..39f01512d 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -3371,7 +3371,7 @@ fold_left over the terms, letin body comes before the type). let free_evars = let cache = Evarutil.create_undefined_evars_cache () in let map ev = - let evi = Evd.find sigma ev in + let EvarInfo evi = Evd.find sigma ev in let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in (ev, fevs) in From 15e895a9bf08ff84ca1d5132f995d7d23c0b7289 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 7 Dec 2022 15:45:01 +0100 Subject: [PATCH 07/35] Adapt w.r.t. coq/coq#16903. --- src/coq_elpi_HOAS.ml | 5 +++-- src/coq_elpi_builtins.ml | 4 ++-- src/coq_elpi_glob_quotation.ml | 2 +- 3 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index f71dc3309..4ed839bfe 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -172,7 +172,8 @@ let sort = | Sorts.Type _ -> Format.fprintf fmt "Type" | Sorts.Set -> Format.fprintf fmt "Set" | Sorts.Prop -> Format.fprintf fmt "Prop" - | Sorts.SProp -> Format.fprintf fmt "SProp"); + | Sorts.SProp -> Format.fprintf fmt "SProp" + | Sorts.QSort _ -> Format.fprintf fmt "Type"); constructors = [ K("prop","impredicative sort of propositions",N, B Sorts.prop, @@ -900,7 +901,7 @@ let force_level_of_universe state u = let purge_algebraic_univs_sort state s = let sigma = (S.get engine state).sigma in match EConstr.ESorts.kind sigma s with - | Sorts.Type u -> + | Sorts.Type u | Sorts.QSort (_ , u) -> let state, _, _, s = force_level_of_universe state u in state, s | x -> state, x diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index cef28e052..77d7a12f9 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -150,7 +150,7 @@ let mk_algebraic_super x = Sorts.super x let univ_super state u v = let state, u = match u with | Sorts.Set | Sorts.Prop | Sorts.SProp -> state, u - | Sorts.Type ul -> + | Sorts.Type ul | Sorts.QSort (_, ul) -> if Univ.Universe.is_level ul then state, u else let state, (_,w) = new_univ_level_variable state in @@ -1469,7 +1469,7 @@ regarded as not non-informative).|})), match indbo.Declarations.mind_kelim with | (Sorts.InSProp | Sorts.InProp) -> raise No_clause | Sorts.InSet when Environ.is_impredicative_set env -> raise No_clause - | (Sorts.InSet | Sorts.InType) -> () + | (Sorts.InSet | Sorts.InType | Sorts.InQSort) -> () )), DocAbove); diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index de0256fbf..9f7e871ca 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/coq_elpi_glob_quotation.ml @@ -159,7 +159,7 @@ let rec gterm2lp ~depth state x = incr type_gen; let state, s = API.RawQuery.mk_Arg state ~name:(Printf.sprintf "type_%d" !type_gen) ~args:[] in state, in_elpi_flex_sort s - | GSort(UNamed u) -> + | GSort(UNamed (None, u)) -> let env = get_global_env state in in_elpi_sort ~depth state (sort_name env (get_sigma state) u) | GSort(_) -> nYI "(glob)HOAS for Type@{i j}" From 5454ea0401ce945fb6ecb5cf17f33030a1084d36 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 12 Jan 2023 15:13:09 +0100 Subject: [PATCH 08/35] Adapt to coq/coq#17098 (functional grammar state) --- src/coq_elpi_arg_syntax.mlg | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/coq_elpi_arg_syntax.mlg b/src/coq_elpi_arg_syntax.mlg index ab571549f..a74f87191 100644 --- a/src/coq_elpi_arg_syntax.mlg +++ b/src/coq_elpi_arg_syntax.mlg @@ -62,18 +62,18 @@ let pr_fp _ _ _ (_,x) = U.pr_qualified_name x let pp_elpi_loc _ _ _ (l : Loc.t) = Pp.mt () let the_qname = ref "" -let any_qname strm = +let any_qname kwstate strm = let re = Str.regexp "[A-Za-z][A-Za-z0-9]*\\(\\.?[A-Za-z][A-Za-z0-9]*\\)*" in - match LStream.peek strm with + match LStream.peek kwstate strm with | Some (Tok.KEYWORD sym) when Str.string_match re sym 0 -> let pos = LStream.count strm in let _, ep = Loc.unloc (LStream.get_loc pos strm) in - LStream.junk strm; - begin match LStream.peek strm with + LStream.junk kwstate strm; + begin match LStream.peek kwstate strm with | Some (Tok.IDENT id) -> let bp, _ = Loc.unloc (LStream.get_loc (pos+1) strm) in if Int.equal ep bp then - (LStream.junk strm; the_qname := sym ^ id) + (LStream.junk kwstate strm; the_qname := sym ^ id) else the_qname := sym | _ -> the_qname := sym @@ -137,9 +137,9 @@ let coq_kwd_or_symbol = Pcoq.Entry.create "elpi:kwd_or_symbol" let opt2list = function None -> [] | Some l -> l let the_kwd = ref "" -let any_kwd strm = - match LStream.peek strm with - | Some (Tok.KEYWORD sym) when sym <> "." -> LStream.junk strm; the_kwd := sym +let any_kwd kwstate strm = + match LStream.peek kwstate strm with + | Some (Tok.KEYWORD sym) when sym <> "." -> LStream.junk kwstate strm; the_kwd := sym | _ -> raise Stream.Failure let any_kwd = Pcoq.Entry.(of_parser "any_symbols_or_kwd" { parser_fun = any_kwd }) From 27cfb66c2721e23fbc35045a1e01cf633cdc5b28 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 16 Sep 2020 06:50:48 +0200 Subject: [PATCH 09/35] This is to adapt to coq/coq#13025 (refined logic of levels in custom notations). There is now a new specific type "notation_subentry_level" for remembering the level or absence of explicit level of the variables of a grammar rule. The type "notation_entry_level" still exists but is only for characterizing the level (and custom entry name) in which a rule lives. --- src/coq_elpi_builtins.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 0332ad6a2..3efc7bf8b 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -2849,7 +2849,7 @@ Supported attributes: { nenv with Notation_term.ninterp_var_type = Id.Map.add id (Notation_term.NtnInternTypeAny None) nenv.Notation_term.ninterp_var_type }, - (id, ((Constrexpr.InConstrEntrySomeLevel,([],[])),Notation_term.NtnTypeConstr)) :: vars in + (id, ((Constrexpr.(InConstrEntry,(LevelSome,None)),([],[])),Notation_term.NtnTypeConstr)) :: vars in let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum(name,ty)) env in aux vars nenv env (n-1) t | _ -> From 315029e1b23d32b4d4450a0cba56a7bcc61ee4cf Mon Sep 17 00:00:00 2001 From: Ramkumar Ramachandra Date: Fri, 13 Jan 2023 15:34:20 +0100 Subject: [PATCH 10/35] arg_syntax: replace Pcoq.Entry.create with Pcoq.Entry.make We are removing the deprecated Pcoq.Entry.create. See coq/coq#17065. --- src/coq_elpi_arg_syntax.mlg | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/coq_elpi_arg_syntax.mlg b/src/coq_elpi_arg_syntax.mlg index ab571549f..632aaa4bb 100644 --- a/src/coq_elpi_arg_syntax.mlg +++ b/src/coq_elpi_arg_syntax.mlg @@ -100,9 +100,9 @@ END { -let telescope = Pcoq.Entry.create "elpi:telescope" -let colon_sort = Pcoq.Entry.create "elpi:colon_sort" -let colon_constr = Pcoq.Entry.create "elpi:colon_constr" +let telescope = Pcoq.Entry.make "elpi:telescope" +let colon_sort = Pcoq.Entry.make "elpi:colon_sort" +let colon_constr = Pcoq.Entry.make "elpi:colon_constr" let any_attribute : Attributes.vernac_flags Attributes.attribute = Attributes.make_attribute (fun x -> [],x) From 449107758a7208e7b4fe56658be51634e7a5c369 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 16 Jan 2023 15:08:39 +0100 Subject: [PATCH 11/35] Adapt to coq/coq#17096 (detype isgoal argument is optional) `false` is the default --- src/coq_elpi_utils.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/coq_elpi_utils.ml b/src/coq_elpi_utils.ml index 0db82e6f2..7f0951370 100644 --- a/src/coq_elpi_utils.ml +++ b/src/coq_elpi_utils.ml @@ -223,11 +223,11 @@ let detype ?(keepunivs=false) env sigma t = if keepunivs then Flags.with_option Constrextern.print_universes else (fun f x -> f x) in let gbody = - options (Detyping.detype Detyping.Now false Names.Id.Set.empty env sigma) t in + options (Detyping.detype Detyping.Now Names.Id.Set.empty env sigma) t in fix_detype gbody let detype_closed_glob env sigma closure = - let gbody = Detyping.detype_closed_glob false Names.Id.Set.empty env sigma closure in + let gbody = Detyping.detype_closed_glob Names.Id.Set.empty env sigma closure in fix_detype gbody type qualified_name = string list From dad217bd345197660f04bbf8ec3e19f6aceff848 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Mon, 30 Jan 2023 10:56:59 +0100 Subject: [PATCH 12/35] Adapt w.r.t. coq/coq#17170. This assumes that info_of_evar is only ever called on undefined evars, but I am not really confident this is the case. The test-suite goes through, though. --- src/coq_elpi_HOAS.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 97cc9adbd..51b493212 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -1213,7 +1213,7 @@ let restrict_coq_context live_db state { proof; proof_len; local; name2db; env; let info_of_evar ~env ~sigma ~section k = let open Context.Named in - let EvarInfo evi = Evd.find sigma k in + let evi = Evd.find_undefined sigma k in let info = Evarutil.nf_evar_info sigma evi in let filtered_hyps = Evd.evar_filtered_hyps info in let ctx = EC.named_context_of_val filtered_hyps in From 0d15ed3bfb1f76f3b33086c9dfea0447141addea Mon Sep 17 00:00:00 2001 From: Ramkumar Ramachandra Date: Fri, 13 Jan 2023 15:34:20 +0100 Subject: [PATCH 13/35] arg_syntax: replace Pcoq.Entry.create with Pcoq.Entry.make We are removing the deprecated Pcoq.Entry.create. See coq/coq#17065. This patch removes one more instance of Pcoq.Entry.create. --- src/coq_elpi_arg_syntax.mlg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq_elpi_arg_syntax.mlg b/src/coq_elpi_arg_syntax.mlg index 0cbaa4282..0892c8461 100644 --- a/src/coq_elpi_arg_syntax.mlg +++ b/src/coq_elpi_arg_syntax.mlg @@ -132,7 +132,7 @@ let validate_attributes a flags = ignore_unknown_attributes extra; raw_args -let coq_kwd_or_symbol = Pcoq.Entry.create "elpi:kwd_or_symbol" +let coq_kwd_or_symbol = Pcoq.Entry.make "elpi:kwd_or_symbol" let opt2list = function None -> [] | Some l -> l From 4cea82acd393dd3af0490e701f2eefad46087efe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 6 Feb 2023 16:45:49 +0100 Subject: [PATCH 14/35] Adapt to coq/coq#17177 (universe printing API change) --- src/coq_elpi_HOAS.ml | 10 +++++----- src/coq_elpi_builtins.ml | 4 ++-- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 51b493212..a655c5375 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -67,7 +67,7 @@ let pre_engine : coq_engine S.component option ref = ref None module UnivOrd = struct type t = Univ.Universe.t let compare = Univ.Universe.compare - let show x = Pp.string_of_ppcmds (Univ.Universe.pr x) + let show x = Pp.string_of_ppcmds (Univ.Universe.pr UnivNames.pr_with_global_universes x) let pp fmt x = Format.fprintf fmt "%s" (show x) end module UnivSet = U.Set.Make(UnivOrd) @@ -85,8 +85,8 @@ module UnivLevelMap = U.Map.Make(UnivLevelOrd) module UM = F.Map(struct type t = Univ.Universe.t let compare = Univ.Universe.compare - let show x = Pp.string_of_ppcmds @@ Univ.Universe.pr x - let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (Univ.Universe.pr x) + let show x = Pp.string_of_ppcmds @@ Univ.Universe.pr UnivNames.pr_with_global_universes x + let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (Univ.Universe.pr UnivNames.pr_with_global_universes x) end) let um = S.declare ~name:"coq-elpi:evar-univ-map" @@ -111,7 +111,7 @@ let add_universe_constraint state c = | UGraph.UniverseInconsistency p -> Feedback.msg_debug (UGraph.explain_universe_inconsistency - UnivNames.(pr_with_global_universes empty_binders) p); + UnivNames.pr_with_global_universes p); raise API.BuiltInPredicate.No_clause | Evd.UniversesDiffer | UState.UniversesDiffer -> Feedback.msg_debug Pp.(str"UniversesDiffer"); @@ -138,7 +138,7 @@ let isuniv, univout, (univ : Univ.Universe.t API.Conversion.t) = CD.name = "univ"; doc = "universe level (algebraic: max, +1, univ.variable)"; pp = (fun fmt x -> - let s = Pp.string_of_ppcmds (Univ.Universe.pr x) in + let s = Pp.string_of_ppcmds (Univ.Universe.pr UnivNames.pr_with_global_universes x) in Format.fprintf fmt "«%s»" s); compare = Univ.Universe.compare; hash = Univ.Universe.hash; diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 0332ad6a2..15ae41bf4 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -134,7 +134,7 @@ let warn_if_contains_univ_levels ~depth t = let univs = aux ~depth [] t in if univs <> [] then err Pp.(strbrk "The hypothetical clause contains terms of type univ which are not global, you should abstract them out or replace them by global ones: " ++ - prlist_with_sep spc Univ.Universe.pr univs) + prlist_with_sep spc (Univ.Universe.pr UnivNames.pr_with_global_universes) univs) ;; let bool = B.bool @@ -1089,7 +1089,7 @@ let unify_instances_gref gr ui1 ui2 diag env state cmp_constr_universes = | _ -> let msg = UGraph.explain_universe_inconsistency - UnivNames.(pr_with_global_universes empty_binders) p in + UnivNames.pr_with_global_universes p in state, !: (B.mkERROR (Pp.string_of_ppcmds msg)), [] let gref_set, gref_set_decl = B.ocaml_set_conv ~name:"coq.gref.set" gref (module GRSet) From 79f7fbc00996153efbb8df2bae17469200a23575 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 8 Feb 2023 13:58:10 +0100 Subject: [PATCH 15/35] Adapt to coq/coq#17220 (genargs are not holes) --- src/coq_elpi_arg_HOAS.ml | 2 +- src/coq_elpi_builtins.ml | 10 +++++----- src/coq_elpi_glob_quotation.ml | 10 +++++----- src/coq_elpi_utils.ml | 2 +- src/coq_elpi_vernacular_syntax.mlg | 2 +- 5 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml index b2b4dec84..974ce46cb 100644 --- a/src/coq_elpi_arg_HOAS.ml +++ b/src/coq_elpi_arg_HOAS.ml @@ -300,7 +300,7 @@ let raw_indt_decl_to_glob glob_sign ({ finiteness; name; parameters; non_uniform { finiteness; name = (space, name); arity; params; nuparams; nuparams_given; constructors; univpoly } let intern_indt_decl glob_sign (it : raw_indt_decl) = glob_sign, it -let expr_hole = CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous,None) +let expr_hole = CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous) let raw_context_decl_to_glob glob_sign fields = let _intern_env, fields = intern_global_context ~intern_env:Constrintern.empty_internalization_env glob_sign fields in diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 0332ad6a2..ce5bce03d 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -95,7 +95,7 @@ let pr_econstr_env options env sigma t = let expr = Constrextern.extern_constr env sigma t in let expr = let rec aux () ({ CAst.v } as orig) = match v with - | Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous,None) + | Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous) | _ -> Constrexpr_ops.map_constr_expr_with_binders (fun _ () -> ()) aux () orig in if options.hoas_holes = Some Heuristic then aux () expr else expr in Ppconstr.pr_constr_expr_n env sigma options.pplevel expr) @@ -885,7 +885,7 @@ let cache_abbrev_for_tac { abbrev_name; tac_name = tacname; tac_fixed_args = mor | Coq_elpi_arg_HOAS.Tac.Term (t,_) -> let expr = Constrextern.extern_glob_constr Constrextern.empty_extern_env t in let rec aux () ({ CAst.v } as orig) = match v with - | Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous,None) + | Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous) | _ -> Constrexpr_ops.map_constr_expr_with_binders (fun _ () -> ()) aux () orig in Coq_elpi_arg_HOAS.Tac.Term (aux () expr) | _ -> assert false) in @@ -894,7 +894,7 @@ let cache_abbrev_for_tac { abbrev_name; tac_name = tacname; tac_fixed_args = mor let args = args |> List.map (fun (arg,_) -> Coq_elpi_arg_HOAS.Tac.Term(arg)) in let args = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Coq_elpi_arg_syntax.wit_elpi_tactic_arg)) (more_args @ args) in (TacML (elpi_tac_entry, [TacGeneric(None, tacname); TacGeneric(None, args)])) in - CAst.make @@ Constrexpr.CHole (None, Namegen.IntroAnonymous, Some (Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) (CAst.make tac))) in + CAst.make @@ Constrexpr.CGenarg (Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) (CAst.make tac)) in let Gbpmp (rule, action) = gbpmp action (List.rev abbrev_name) in Pcoq.grammar_extend Pcoq.Constr.term (Pcoq.Fresh (Gramlib.Gramext.Before "10", @@ -2894,7 +2894,7 @@ Supported attributes: let binders, vars = List.split (CList.init nargs (fun i -> let name = Coq_elpi_glob_quotation.mk_restricted_name i in let lname = CAst.make @@ Name.Name (Id.of_string name) in - CLocalAssum([lname],Default Glob_term.Explicit, CAst.make @@ CHole(None,Namegen.IntroAnonymous,None)), + CLocalAssum([lname],Default Glob_term.Explicit, CAst.make @@ CHole(None,Namegen.IntroAnonymous)), (CAst.make @@ CRef(Libnames.qualid_of_string name,None), None))) in let eta = CAst.(make @@ CLambdaN(binders,make @@ CApp(make @@ CRef(Libnames.qualid_of_string (KerName.to_string sd),None),vars))) in let sigma = get_sigma state in @@ -2924,7 +2924,7 @@ Supported attributes: let binders, vars = List.split (CList.init nargs (fun i -> let name = Coq_elpi_glob_quotation.mk_restricted_name i in let lname = CAst.make @@ Name.Name (Id.of_string name) in - CLocalAssum([lname],Default Glob_term.Explicit, CAst.make @@ CHole(None,Namegen.IntroAnonymous,None)), + CLocalAssum([lname],Default Glob_term.Explicit, CAst.make @@ CHole(None,Namegen.IntroAnonymous)), (CAst.make @@ CRef(Libnames.qualid_of_string name,None), None))) in let eta = CAst.(make @@ CLambdaN(binders,make @@ CApp(make @@ CRef(Libnames.qualid_of_string (KerName.to_string sd),None),vars))) in let sigma = get_sigma state in diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index 9f7e871ca..3f3481eee 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/coq_elpi_glob_quotation.ml @@ -185,7 +185,7 @@ let rec gterm2lp ~depth state x = let state, t, () = under_ctx name ty (Some bo) (nogls gterm2lp) ~depth state t in state, in_elpi_let name bo ty t - | GHole(_,_,Some arg) when !is_elpi_code arg -> + | GGenarg arg when !is_elpi_code arg -> let loc, text = !get_elpi_code arg in let s, x = Q.lp ~depth state loc text in let s, x = @@ -199,7 +199,7 @@ let rec gterm2lp ~depth state x = in (* Format.eprintf "unquote: %a\n" (Elpi_API.Extend.Pp.term depth) x; *) s, x - | GHole(_,_,Some arg) when !is_elpi_code_appArg arg -> + | GGenarg arg when !is_elpi_code_appArg arg -> begin match !get_elpi_code_appArg arg with | _, [] -> assert false | loc, hd :: vars -> @@ -213,7 +213,9 @@ let rec gterm2lp ~depth state x = state, mkApp ~depth hd args end - | GHole (_,_,None) -> + | GGenarg _ -> nYI "(glob)HOAS for GGenarg" + + | GHole _ -> let state, uv = F.Elpi.make state in let ctx, _ = Option.default (upcast @@ mk_coq_context ~options:(default_options ()) state, []) (get_ctx state) in let args = @@ -225,8 +227,6 @@ let rec gterm2lp ~depth state x = in state, E.mkUnifVar uv ~args state - | GHole _ -> nYI "(glob)HOAS for GHole" - | GCast(t,_,c_ty) -> let state, t = gterm2lp ~depth state t in let state, c_ty = gterm2lp ~depth state c_ty in diff --git a/src/coq_elpi_utils.ml b/src/coq_elpi_utils.ml index 7f0951370..af662e34d 100644 --- a/src/coq_elpi_utils.ml +++ b/src/coq_elpi_utils.ml @@ -71,7 +71,7 @@ let safe_destApp sigma t = let mkGHole = DAst.make - (Glob_term.GHole(Evar_kinds.InternalHole,Namegen.IntroAnonymous,None)) + (Glob_term.GHole(Evar_kinds.InternalHole,Namegen.IntroAnonymous)) let mkApp ~depth t l = match l with diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg index 748c54eca..da7e894c9 100644 --- a/src/coq_elpi_vernacular_syntax.mlg +++ b/src/coq_elpi_vernacular_syntax.mlg @@ -71,7 +71,7 @@ GRAMMAR EXTEND Gram then Genarg.in_gen (Genarg.rawwit wit_elpi_code) (strip_curly loc s) else Genarg.in_gen (Genarg.rawwit wit_elpi_code) (Coq_elpi_utils.of_coq_loc loc,s) in CAst.make ~loc - (Constrexpr.CHole (None, Namegen.IntroAnonymous, Some arg)) } ] + (Constrexpr.CGenarg arg) } ] ] ; END From c169f11370f063b81902dcfe56caedaa0a8bd212 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 21 Feb 2023 15:06:23 +0100 Subject: [PATCH 16/35] Adapt to coq/coq#17265 (fix find_map type) --- src/coq_elpi_HOAS.ml | 4 ++-- src/coq_elpi_glob_quotation.ml | 6 ++++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index a655c5375..ee95e0701 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -1548,7 +1548,7 @@ let pp_cst fmt { E.goal = (depth,concl); context } = (P.term depth) concl let find_evar var csts = - csts |> CList.find_map (fun ({ E.goal = (depth,concl); context } as cst) -> + csts |> CList.find_map_exn (fun ({ E.goal = (depth,concl); context } as cst) -> match E.look ~depth concl with | E.App(c,x,[ty;rx]) when c == evarc -> begin match E.look ~depth x, E.look ~depth rx with @@ -1594,7 +1594,7 @@ let rec dblset_of_canonical_ctx ~depth acc = function str(pp2string (P.term depth) x)) let find_evar_decl var csts = - csts |> CList.find_map (fun ({ E.goal = (depth,concl); context } as cst) -> + csts |> CList.find_map_exn (fun ({ E.goal = (depth,concl); context } as cst) -> match E.look ~depth concl with | E.App(c,x,[ty;rx]) when c == evarc -> begin match E.look ~depth x, E.look ~depth rx with diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index 3f3481eee..03929c4cd 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/coq_elpi_glob_quotation.ml @@ -333,11 +333,13 @@ let rec gterm2lp ~depth state x = assert(List.length def <= 1); let bs = CList.init no_constructors (fun i -> let cno = i + 1 in - try CList.find_map (function + match CList.find_map (function | `Case((_,n as k),vars,bo) when n = cno -> Some (k,vars,bo) | `Case _ -> None | `Def _ -> assert false) bs - with Not_found -> + with + | Some v -> v + | None -> match def with | [`Def bo] -> let missing_k = ind,cno in From 139e95e463b0ab151e1cec345ab49c8cfa974f8f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 24 Feb 2023 14:59:16 +0100 Subject: [PATCH 17/35] Adapt to coq/coq#17283 (More careful handling of possibly universe polymorphic globrefs) --- src/coq_elpi_builtins.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index d71c3b377..279e3a19d 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -2515,7 +2515,7 @@ Supported attributes: Out(list tc_instance, "Db", Read(global,"reads all instances of the given class GR"))), (fun gr _ ~depth { env } _ state -> - !: (Typeclasses.instances env (get_sigma state) gr))), + !: (Typeclasses.instances_exn env (get_sigma state) gr))), DocAbove); MLCode(Pred("coq.TC.class?", From b0e1e3ac89cacdc2c8f95516a3b7bddbbaac08e8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 24 Feb 2023 15:00:03 +0100 Subject: [PATCH 18/35] gitignore generated Makefile.examples --- .gitignore | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 931c52330..4ab97311f 100644 --- a/.gitignore +++ b/.gitignore @@ -37,5 +37,7 @@ Makefile.coq.conf .merlin Makefile.test.coq Makefile.test.coq.conf +Makefile.examples.coq +Makefile.examples.coq.conf -META \ No newline at end of file +META From a17569f174a355a678e66b1916a75dc2e4188cf2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 4 Dec 2022 16:50:16 +0100 Subject: [PATCH 19/35] Adapt to Coq PR #16935: asking for a strict check when not specified. --- src/coq_elpi_vernacular.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index c890fdccc..846a57c23 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -691,7 +691,7 @@ let run_program loc name ~atts args = let env = Global.env () in let sigma = Evd.from_env env in let args = args - |> List.map (Coq_elpi_arg_HOAS.Cmd.glob (Genintern.empty_glob_sign env)) + |> List.map (Coq_elpi_arg_HOAS.Cmd.glob (Genintern.empty_glob_sign ~strict:true env)) |> List.map (Coq_elpi_arg_HOAS.Cmd.interp (Ltac_plugin.Tacinterp.default_ist ()) env sigma) in let query ~depth state = From 796717381099675b4ea217879e833fa35146005e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= Date: Mon, 27 Mar 2023 13:39:10 +0200 Subject: [PATCH 20/35] Activate backtrace on exceptions --- Makefile.coq.local | 1 + 1 file changed, 1 insertion(+) diff --git a/Makefile.coq.local b/Makefile.coq.local index de6e205d3..ae2d441fc 100644 --- a/Makefile.coq.local +++ b/Makefile.coq.local @@ -1,6 +1,7 @@ CAMLPKGS+= -package elpi,stdlib-shims CAMLFLAGS+= -bin-annot -g OCAMLWARN+=-warn-error -32 +COQEXTRAFLAGS=-bt theories/elpi.vo: $(wildcard elpi/*.elpi) From e4b162fecb8b4c35e29d068bf87e6d3253b634c1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= Date: Mon, 27 Mar 2023 13:39:27 +0200 Subject: [PATCH 21/35] Adapt to Coq's https://github.com/coq/coq/pull/17331 --- src/coq_elpi_arg_syntax.mlg | 2 +- src/coq_elpi_builtins.ml | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/coq_elpi_arg_syntax.mlg b/src/coq_elpi_arg_syntax.mlg index 0892c8461..ab23d09e9 100644 --- a/src/coq_elpi_arg_syntax.mlg +++ b/src/coq_elpi_arg_syntax.mlg @@ -280,7 +280,7 @@ ARGUMENT EXTEND ltac_attributes Ltac_plugin.Tacinterp.interp_ltac_var (Ltac_plugin.Tacinterp.Value.cast (Genarg.topwit wit_attributes)) ist None (CAst.make id) | _ -> assert false } GLOBALIZED BY { fun gsig t -> fst @@ Ltac_plugin.Tacintern.intern_constr gsig t } - SUBSTITUTED BY { Detyping.subst_glob_constr (Global.env()) } + SUBSTITUTED BY { fun x -> Detyping.subst_glob_constr (Global.env()) x } RAW_PRINTED BY { fun _ _ _ -> Ppconstr.pr_constr_expr env sigma } GLOB_PRINTED BY { fun _ _ _ -> Printer.pr_glob_constr_env env sigma } | [ ident(v) ] -> { (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string v,None)) } diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 279e3a19d..a5c05d296 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -3420,15 +3420,15 @@ fold_left over the terms, letin body comes before the type). Unsafe.tclSETGOALS [with_empty_state goal] <*> tactic in let _, pv = init sigma [] in let (), pv, _, _ = - let vernac_state = Vernacstate.freeze_interp_state ~marshallable:false in + let vernac_state = Vernacstate.freeze_full_state ~marshallable:false in try let rc = apply ~name:(Id.of_string "elpi") ~poly:false proof_context.env focused_tac pv in - let pstate = Vernacstate.Stm.pstate (Vernacstate.freeze_interp_state ~marshallable:false) in + let pstate = Vernacstate.Stm.pstate (Vernacstate.freeze_full_state ~marshallable:false) in let vernac_state = Vernacstate.Stm.set_pstate vernac_state pstate in - Vernacstate.unfreeze_interp_state vernac_state; + Vernacstate.unfreeze_full_state vernac_state; rc with e when CErrors.noncritical e -> - Vernacstate.unfreeze_interp_state vernac_state; + Vernacstate.unfreeze_full_state vernac_state; Feedback.msg_debug (CErrors.print e); raise Pred.No_clause in From 760dc44b5d5e11854d6706e6d9e6cdca5043d407 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 3 Apr 2023 12:07:38 +0200 Subject: [PATCH 22/35] Adapt to coq/coq#17453 (Reduction->Conversion) --- src/coq_elpi_builtins.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 279e3a19d..f95842344 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -1054,12 +1054,12 @@ let unify_instances_gref gr ui1 ui2 diag env state cmp_constr_universes = | IndRef ind -> let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in let univs = Declareops.inductive_polymorphic_context mib in - Reduction.inductive_cumulativity_arguments (mib,snd ind), Univ.AbstractContext.size univs + Conversion.inductive_cumulativity_arguments (mib,snd ind), Univ.AbstractContext.size univs | ConstructRef (ind,kno) -> let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in let univs = Declareops.inductive_polymorphic_context mib in - Reduction.constructor_cumulativity_arguments (mib,snd ind,kno), Univ.AbstractContext.size univs + Conversion.constructor_cumulativity_arguments (mib,snd ind,kno), Univ.AbstractContext.size univs in let l1 = Univ.Instance.length ui1 in let l2 = Univ.Instance.length ui2 in @@ -2992,7 +2992,7 @@ Universe constraints are put in the constraint store.|})))), let sigma, ty = Typing.type_of proof_context.env sigma t in match ety with | Data ety -> - let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Reduction.CUMUL ty ety in + let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL ty ety in let state, assignments = set_current_sigma ~depth state sigma in state, !: ety +! B.mkOK, assignments | NoData -> @@ -3024,7 +3024,7 @@ Universe constraints are put in the constraint store.|})))), let sigma, s = Typing.sort_of proof_context.env sigma ty in match es with | Data es -> - let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Reduction.CUMUL (EConstr.mkSort s) (EConstr.mkSort (EConstr.ESorts.make es)) in + let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL (EConstr.mkSort s) (EConstr.mkSort (EConstr.ESorts.make es)) in let state, assignments = set_current_sigma ~depth state sigma in state, !: es +! B.mkOK, assignments | NoData -> @@ -3050,7 +3050,7 @@ Universe constraints are put in the constraint store.|})))), (fun a b diag ~depth proof_context _ state -> let sigma = get_sigma state in try - let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Reduction.CONV a b in + let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CONV a b in let state, assignments = set_current_sigma ~depth state sigma in state, !: B.mkOK, assignments with Pretype_errors.PretypeError (env, sigma, err) -> @@ -3071,7 +3071,7 @@ Universe constraints are put in the constraint store.|})))), (fun a b diag ~depth proof_context _ state -> let sigma = get_sigma state in try - let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Reduction.CUMUL a b in + let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL a b in let state, assignments = set_current_sigma ~depth state sigma in state, !: B.mkOK, assignments with Pretype_errors.PretypeError (env, sigma, err) -> @@ -3116,7 +3116,7 @@ Supported attributes: let state, assignments = set_current_sigma ~depth state sigma in state, ?: None +! uj_val +! B.mkOK, assignments | `NoUnify ety -> - let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Reduction.CUMUL uj_type ety in + let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL uj_type ety in let state, assignments = set_current_sigma ~depth state sigma in state, ?: None +! uj_val +! B.mkOK, assignments with Pretype_errors.PretypeError (env, sigma, err) -> From 9f48d8b35306e9b50824eb5f7443b9fa76a67d9f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 27 Apr 2023 13:16:35 +0200 Subject: [PATCH 23/35] Adapt to coq/coq#16890 (Classes.existing_instance takes globref not qualid) --- src/coq_elpi_builtins.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index cfc6c14f4..d4377ee38 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -2565,9 +2565,7 @@ Supported attributes: (fun gr priority ~depth { options } _ -> grab_global_env "coq.TC.declare-instance" (fun state -> let global = if options.local = Some false then Hints.SuperGlobal else Hints.Local in let hint_priority = Some priority in - let qualid = - Nametab.shortest_qualid_of_global Names.Id.Set.empty gr in - Classes.existing_instance global qualid + Classes.existing_instance global gr (Some { Hints.empty_hint_info with Typeclasses.hint_priority }); state, (), []))), DocAbove); From 2d877be09e4496dd9f104331125ba418e7c4fd5c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 15 May 2023 14:01:59 +0200 Subject: [PATCH 24/35] Adapt to coq/coq#17605 (summary doesn't use marshallable argument when freezing) --- src/coq_elpi_builtins.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 3fb6aa3c5..9d52888a2 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -3486,10 +3486,10 @@ fold_left over the terms, letin body comes before the type). Unsafe.tclSETGOALS [with_empty_state goal] <*> tactic in let _, pv = init sigma [] in let (), pv, _, _ = - let vernac_state = Vernacstate.freeze_full_state ~marshallable:false in + let vernac_state = Vernacstate.freeze_full_state () in try let rc = apply ~name:(Id.of_string "elpi") ~poly:false proof_context.env focused_tac pv in - let pstate = Vernacstate.Stm.pstate (Vernacstate.freeze_full_state ~marshallable:false) in + let pstate = Vernacstate.Stm.pstate (Vernacstate.freeze_full_state ()) in let vernac_state = Vernacstate.Stm.set_pstate vernac_state pstate in Vernacstate.unfreeze_full_state vernac_state; rc From d3b8b2b733307461112dc0590f97d0840d822d86 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 15 May 2023 16:49:30 +0200 Subject: [PATCH 25/35] Support backtracking over exported commands Fix #452 Requires https://github.com/coq/coq/pull/17616 --- src/coq_elpi_vernacular.ml | 46 +++++++++++++++++++++----------------- 1 file changed, 25 insertions(+), 21 deletions(-) diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index 9814f06c0..d58fe4a9b 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -850,27 +850,31 @@ let loc_merge l1 l2 = let cache_program (nature,p,p_str) = match nature with | Command _ -> - Vernacextend.vernac_extend - ~command:("Elpi"^p_str) - ~classifier:(fun _ -> Vernacextend.(VtSideff ([], VtNow))) - ?entry:None - [ Vernacextend.TyML - (false, - Vernacextend.TyNonTerminal - (Extend.TUentry - (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_loc), - Vernacextend.TyTerminal - (p_str, - Vernacextend.TyNonTerminal - (Extend.TUlist0 - (Extend.TUentry (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_cmd_arg)) - ,Vernacextend.TyNonTerminal - (Extend.TUentry (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_loc), - Vernacextend.TyNil)))), - (fun loc0 args loc1 ?loc ~atts () -> Vernacextend.vtdefault (fun () -> - run_program (Option.default (loc_merge loc0 loc1) loc) p ~atts args)), - None) - ] + let ext = + Vernacextend.declare_dynamic_vernac_extend + ~command:("Elpi"^p_str) + ?entry:None + ~depr:false + + (fun _loc0 _args _loc1 -> (Vernacextend.VtSideff ([], VtNow))) + + (Vernacextend.TyNonTerminal + (Extend.TUentry + (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_loc), + Vernacextend.TyTerminal + (p_str, + Vernacextend.TyNonTerminal + (Extend.TUlist0 + (Extend.TUentry (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_cmd_arg)) + ,Vernacextend.TyNonTerminal + (Extend.TUentry (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_loc), + Vernacextend.TyNil))))) + + (fun loc0 args loc1 ?loc ~atts () -> Vernacextend.vtdefault (fun () -> + run_program (Option.default (loc_merge loc0 loc1) loc) p ~atts args)) + in + Egramml.extend_vernac_command_grammar ~undoable:true ext + | Tactic -> Coq_elpi_builtins.cache_tac_abbrev p | Program _ -> From 81dc186cce0b957cf14a9ceda69900f63bd48798 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 22 May 2023 13:51:46 +0200 Subject: [PATCH 26/35] Adapt to coq/coq#17585 (revised warning API) --- src/coq_elpi_HOAS.ml | 2 +- src/coq_elpi_builtins.ml | 20 +++++++++++++++----- src/coq_elpi_utils.ml | 8 +++++++- src/coq_elpi_utils.mli | 3 +++ src/coq_elpi_vernacular_syntax.mlg | 14 ++++++++------ 5 files changed, 34 insertions(+), 13 deletions(-) diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index d1af9f2a9..7e43059da 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -2596,7 +2596,7 @@ let readback_arity ~depth coq_ctx constraints state t = let inference_nonuniform_params_off = CWarnings.create ~name:"elpi.unsupported-nonuniform-parameters-inference" - ~category:"elpi" Pp.(fun () -> + ~category:Coq_elpi_utils.elpi_cat Pp.(fun () -> strbrk"Inference of non-uniform parameters is not available in Elpi, please use the explicit | mark in the inductive declaration or Set Uniform Inductive Parameters") let restricted_sigma_of s state = diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 3fb6aa3c5..bee3fbd7a 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -703,7 +703,7 @@ let attribute_value = let open API.AlgebraicData in let open CConv in declare { let attribute = attribute attribute_value -let warning = CWarnings.create ~name:"lib" ~category:"elpi" Pp.str +let warning = CWarnings.create ~name:"lib" ~category:elpi_cat Pp.str let keep x = (x = Pred.Keep) @@ -835,7 +835,7 @@ let ppboxes = let open Conv in let open Pp in let open API.AlgebraicData in decl let warn_deprecated_add_axiom = CWarnings.create ~name:"elpi.add-const-for-axiom-or-sectionvar" - ~category:"elpi.deprecated" + ~category:elpi_depr_cat Pp.(fun () -> strbrk ("elpi: Using coq.env.add-const for declaring axioms or " ^ "section variables is deprecated. Use coq.env.add-axiom or " ^ @@ -1248,8 +1248,18 @@ let coq_builtins = Prints a warning message with a Name and Category which can be used to silence this warning or turn it into an error. See coqc -w command line option|}))), - (fun category name args ~depth _hyps _constraints state -> - let warning = CWarnings.create ~name ~category Pp.str in + (fun category_name name args ~depth _hyps _constraints state -> + let category = match CWarnings.get_category category_name with + | There c -> c + | OtherType -> CErrors.anomaly Pp.(str category_name ++ str "is a warning, not a warning category.") + | NotThere -> CWarnings.create_category ~from:[elpi_cat] ~name:category_name () + in + let w = match CWarnings.get_warning name with + | There w -> w + | OtherType -> CErrors.anomaly Pp.(str name ++ str " is a warning category, not a warning.") + | NotThere -> CWarnings.create_warning ~from:[category] ~name () + in + let warning = CWarnings.create_in w Pp.str in let pp = pp ~depth in let loc, args = if args = [] then None, args @@ -1261,7 +1271,7 @@ line option|}))), | _ -> None, x :: args in let txt = pp2string (P.list ~boxed:true pp " ") args in - if coq_warning_cache category name loc txt then warning ?loc txt; + if coq_warning_cache category_name name loc txt then warning ?loc txt; state, ())), DocAbove); diff --git a/src/coq_elpi_utils.ml b/src/coq_elpi_utils.ml index af662e34d..40ba51266 100644 --- a/src/coq_elpi_utils.ml +++ b/src/coq_elpi_utils.ml @@ -43,10 +43,16 @@ let feedback_fmt_write, feedback_fmt_flush = Feedback.msg_notice Pp.(str s); Buffer.clear b) +let elpi_cat = CWarnings.create_category ~name:"elpi" () +let elpi_depr_cat = + CWarnings.create_category + ~from:[elpi_cat;CWarnings.CoreCategories.deprecated] + ~name:"elpi.deprecated" () + let () = API.Setup.set_error (fun ?loc s -> err ?loc Pp.(str s)) let () = API.Setup.set_anomaly (fun ?loc s -> err ?loc Pp.(str s)) let () = API.Setup.set_type_error (fun ?loc s -> err ?loc Pp.(str s)) -let warn = CWarnings.create ~name:"runtime" ~category:"elpi" Pp.str +let warn = CWarnings.create ~name:"runtime" ~category:elpi_cat Pp.str let () = API.Setup.set_warn (fun ?loc x -> warn ?loc:(Option.map to_coq_loc loc) x) let () = API.Setup.set_std_formatter (Format.make_formatter feedback_fmt_write feedback_fmt_flush) let () = API.Setup.set_err_formatter (Format.make_formatter feedback_fmt_write feedback_fmt_flush) diff --git a/src/coq_elpi_utils.mli b/src/coq_elpi_utils.mli index 21c5a46b6..c5ae6efe8 100644 --- a/src/coq_elpi_utils.mli +++ b/src/coq_elpi_utils.mli @@ -6,6 +6,9 @@ val to_coq_loc : Elpi.API.Ast.Loc.t -> Loc.t val of_coq_loc : Loc.t -> Elpi.API.Ast.Loc.t +val elpi_cat : CWarnings.category +val elpi_depr_cat : CWarnings.category + val err : ?loc:Elpi.API.Ast.Loc.t -> Pp.t -> 'a exception LtacFail of int * Pp.t val ltac_fail_err : ?loc:Elpi.API.Ast.Loc.t -> int -> Pp.t -> 'a diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg index da7e894c9..fdbe84a33 100644 --- a/src/coq_elpi_vernacular_syntax.mlg +++ b/src/coq_elpi_vernacular_syntax.mlg @@ -50,12 +50,14 @@ let rec inlogpath q = function | [] -> [] | x :: xs -> ("coq://" ^ Libnames.string_of_qualid q ^ "/" ^ x) :: inlogpath q xs -let warning_legacy_accumulate = - CWarnings.create ~name:"elpi.accumulate-syntax" ~category:"elpi.deprecated" (fun () -> - Pp.strbrk "The syntax 'Elpi Accumulate File \"path\"' is deprecated, use 'Elpi Accumulate File \"path\" From logpath'") -let warning_legacy_accumulate2 = - CWarnings.create ~name:"elpi.accumulate-syntax" ~category:"elpi.deprecated" (fun () -> - Pp.strbrk "The syntax 'Elpi Accumulate File \"path\" From logpath' is deprecated, use 'From logpath Extra Dependency \"path\" as name. Elpi Accumulate File name.'") +let warning_legacy_accumulate_gen = + CWarnings.create ~name:"elpi.accumulate-syntax" ~category:Coq_elpi_utils.elpi_depr_cat (fun has_from -> + if has_from then + Pp.strbrk "The syntax 'Elpi Accumulate File \"path\"' is deprecated, use 'Elpi Accumulate File \"path\" From logpath'" + else Pp.strbrk "The syntax 'Elpi Accumulate File \"path\" From logpath' is deprecated, use 'From logpath Extra Dependency \"path\" as name. Elpi Accumulate File name.'") + +let warning_legacy_accumulate ?loc () = warning_legacy_accumulate_gen ?loc true +let warning_legacy_accumulate2 ?loc () = warning_legacy_accumulate_gen ?loc false } GRAMMAR EXTEND Gram From 2dc6e0b1584c49f7e18607ea418c1fab412ccffa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 2 Jun 2023 12:23:18 +0200 Subject: [PATCH 27/35] Adapt to coq/coq#17664 (goptions use Deprecation.t option instead of bool) Changing the API elpi exposes is left to future work. --- src/coq_elpi_builtins.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index e5da65151..4e9c7154c 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -940,17 +940,16 @@ let cache_tac_abbrev qualid = cache_abbrev_for_tac { let cache_goption_declaration (depr,key,value) = let open Goptions in + let depr = if depr then Some (Deprecation.make ~note:"elpi" ()) else None in match value with | BoolValue x -> - let _ : unit -> bool = Goptions.declare_bool_option_and_ref ~stage:Interp ~key ~value:x ~depr in + let _ : bool Goptions.getter = Goptions.declare_bool_option_and_ref ~key ~value:x ?depr () in () | IntValue x -> - let _ : unit -> int option = Goptions.declare_intopt_option_and_ref ~stage:Interp ~key ~depr in - Goptions.set_int_option_value key x; + let _ : int option Goptions.getter = Goptions.declare_intopt_option_and_ref ~stage:Interp ~key ?depr ~value:x () in () | StringOptValue x -> - let _ : unit -> string option = Goptions.declare_stringopt_option_and_ref ~stage:Interp ~key ~depr in - Option.iter (Goptions.set_string_option_value key) x; + let _ : string option Goptions.getter = Goptions.declare_stringopt_option_and_ref ~stage:Interp ~key ?depr ~value:x () in () | StringValue _ -> assert false @@ -3567,7 +3566,7 @@ fold_left over the terms, letin body comes before the type). (fun name _ ~depth -> let table = Goptions.get_tables () in match Goptions.OptionMap.find_opt name table with - | Some { Goptions.opt_depr = x; _ } -> !: x + | Some { Goptions.opt_depr = x; _ } -> !: (Option.has_some x) | None -> raise No_clause)), DocAbove); From 509b06cf0e674c187bfa3c5298bd7b721f9358a7 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 9 Jun 2023 17:53:46 +0200 Subject: [PATCH 28/35] Adapt to https://github.com/coq/coq/pull/17716 --- Changelog.md | 6 ++++++ coq-builtin.elpi | 9 ++++----- elpi/coq-HOAS.elpi | 1 - src/coq_elpi_HOAS.ml | 3 --- src/coq_elpi_HOAS.mli | 1 - src/coq_elpi_builtins.ml | 5 ++--- tests/test_API_TC_CS.v | 4 ++-- tests/test_API_env.v | 2 +- 8 files changed, 15 insertions(+), 16 deletions(-) diff --git a/Changelog.md b/Changelog.md index 9d81e5507..aa513ff3b 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,5 +1,11 @@ # Changelog +## UNRELEASED + +### API: +- Removed option `@nonuniform!` as it disappears from Coq + (c.f. https://github.com/coq/coq/pull/17716 ) + ## [1.17.1] - 09/03/2023 Requires Elpi 1.16.5 and Coq 8.17. diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 3fa442dbf..4b4d3642e 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -355,7 +355,6 @@ macro @global! :- get-option "coq:locality" "global". macro @local! :- get-option "coq:locality" "local". macro @primitive! :- get-option "coq:primitive" tt. % primitive records -macro @nonuniform! :- get-option "coq:nonuniform" tt. % coercions macro @reversible! :- get-option "coq:reversible" tt. % coercions macro @uinstance! I :- get-option "coq:uinstance" I. % universe instance @@ -1446,13 +1445,13 @@ external pred coq.reduction.lazy.bi-norm i:term, o:term. % - @redflags! (default coq.redflags.all) external pred coq.reduction.cbv.norm i:term, o:term. -% [coq.reduction.vm.norm T Ty Tred] Puts T in normal form using [vm_compute]'s -% machinery. Its type Ty can be omitted (but is recomputed) +% [coq.reduction.vm.norm T Ty Tred] Puts T in normal form using +% [vm_compute]'s machinery. Its type Ty can be omitted (but is recomputed) external pred coq.reduction.vm.norm i:term, i:term, o:term. % [coq.reduction.native.norm T Ty Tred] Puts T in normal form using -% [native_compute]'s machinery. Its type Ty can be omitted (but is recomputed). -% Falls back to vm.norm if native compilation is not available. +% [native_compute]'s machinery. Its type Ty can be omitted (but is +% recomputed). Falls back to vm.norm if native compilation is not available. external pred coq.reduction.native.norm i:term, i:term, o:term. % [coq.reduction.native.available?] Is native compilation available on this diff --git a/elpi/coq-HOAS.elpi b/elpi/coq-HOAS.elpi index 0265992bf..87a6f251a 100644 --- a/elpi/coq-HOAS.elpi +++ b/elpi/coq-HOAS.elpi @@ -340,7 +340,6 @@ macro @global! :- get-option "coq:locality" "global". macro @local! :- get-option "coq:locality" "local". macro @primitive! :- get-option "coq:primitive" tt. % primitive records -macro @nonuniform! :- get-option "coq:nonuniform" tt. % coercions macro @reversible! :- get-option "coq:reversible" tt. % coercions macro @uinstance! I :- get-option "coq:uinstance" I. % universe instance diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 7e43059da..475bd27d6 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -340,7 +340,6 @@ type options = { inline : Declaremods.inline; uinstance : uinstanceoption; universe_decl : universe_decl_option; - nonuniform : bool option; reversible : bool option; keepunivs : bool option; redflags : CClosure.RedFlags.reds option; @@ -359,7 +358,6 @@ let default_options () = { inline = Declaremods.NoInline; uinstance = NoInstance; universe_decl = NotUniversePolymorphic; - nonuniform = None; reversible = None; keepunivs = None; redflags = None; @@ -1128,7 +1126,6 @@ let get_options ~depth hyps state = inline = get_module_inline_option "coq:inline"; uinstance = get_uinstance_option "coq:uinstance"; universe_decl = get_universe_decl (); - nonuniform = get_bool_option "coq:nonuniform"; reversible = get_bool_option "coq:reversible"; keepunivs = get_bool_option "coq:keepunivs"; redflags = get_redflags_option (); diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli index 7aee54b44..005ecc90d 100644 --- a/src/coq_elpi_HOAS.mli +++ b/src/coq_elpi_HOAS.mli @@ -43,7 +43,6 @@ type options = { inline : Declaremods.inline; uinstance : uinstanceoption; universe_decl : universe_decl_option; - nonuniform : bool option; reversible : bool option; keepunivs : bool option; redflags : CClosure.RedFlags.reds option; diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index e2c4088b0..ef01f79a2 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -2617,15 +2617,14 @@ NParams can always be omitted, since it is inferred. (fun (gr, _, source, target) ~depth { options } _ -> grab_global_env "coq.coercion.declare" (fun state -> let local = options.local <> Some false in let poly = false in - let nonuniform = options.nonuniform = Some true in let reversible = options.reversible = Some true in begin match source, target with | B.Given source, B.Given target -> let source = ComCoercion.class_of_global source in ComCoercion.try_add_new_coercion_with_target gr ~local ~poly - ~nonuniform ~reversible ~source ~target + ~reversible ~source ~target | _, _ -> - ComCoercion.try_add_new_coercion gr ~local ~poly ~nonuniform ~reversible + ComCoercion.try_add_new_coercion gr ~local ~poly ~reversible end; state, (), []))), DocAbove); diff --git a/tests/test_API_TC_CS.v b/tests/test_API_TC_CS.v index 8fda5598f..ac45723e2 100644 --- a/tests/test_API_TC_CS.v +++ b/tests/test_API_TC_CS.v @@ -112,8 +112,8 @@ Elpi Query lp:{{coq.coercion.db L}}. Axiom C3 : nat -> Type. Axiom nuc : forall x, C1 -> C3 x. -Set Warnings "+uniform-inheritance". -Elpi Query lp:{{ @nonuniform! => @reversible! => coq.coercion.declare (coercion {coq.locate "nuc"} _ _ _) }}. +Set Warnings "-uniform-inheritance". +Elpi Query lp:{{ @reversible! => coq.coercion.declare (coercion {coq.locate "nuc"} _ _ _) }}. About nuc. diff --git a/tests/test_API_env.v b/tests/test_API_env.v index b07c046b6..341b55fee 100644 --- a/tests/test_API_env.v +++ b/tests/test_API_env.v @@ -281,7 +281,7 @@ Elpi Query lp:{{ }}. -#[nonuniform] Coercion f2 : r1 >-> eq. +#[warning="-uniform-inheritance"] Coercion f2 : r1 >-> eq. Elpi Query lp:{{ From 78b48d223f736d7a2d3bc9a0eb739310b6e201dc Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 25 Jun 2023 23:31:50 +0200 Subject: [PATCH 29/35] Adapt to coq/coq#17754 --- src/coq_elpi_arg_HOAS.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml index 974ce46cb..54db82582 100644 --- a/src/coq_elpi_arg_HOAS.ml +++ b/src/coq_elpi_arg_HOAS.ml @@ -205,7 +205,7 @@ let univpoly_of ~poly ~cumulative = if notations != [] then CErrors.user_err Pp.(str "notations not supported"); let name = [Names.Id.to_string name.CAst.v] in let constructors = - List.map (function (Vernacexpr.(NoCoercion,NoInstance),c) -> c + List.map (function (Vernacexpr.(_,NoCoercion,NoInstance),c) -> c | _ -> CErrors.user_err Pp.(str "coercion and instance flags not supported")) constructors in let { template; udecl; cumulative; poly; finite } = flags in From 4e2d6acf1bd86779c41ea0033ef5fbb336a9847d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 28 Jul 2023 22:35:45 +0200 Subject: [PATCH 30/35] fix compilation against 8.18 --- src/coq_elpi_HOAS.ml | 28 ++++++++++++++-------------- src/coq_elpi_builtins.ml | 4 ++-- src/coq_elpi_programs.ml | 7 ++----- src/coq_elpi_vernacular.ml | 10 +++------- 4 files changed, 21 insertions(+), 28 deletions(-) diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index d1a2a6df7..8c65bd859 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -75,7 +75,7 @@ module UnivMap = U.Map.Make(UnivOrd) module UnivLevelOrd = struct type t = Univ.Level.t let compare = Univ.Level.compare - let show x = Pp.string_of_ppcmds (Univ.Level.pr x) + let show x = Pp.string_of_ppcmds (UnivNames.pr_with_global_universes x) let pp fmt x = Format.fprintf fmt "%s" (show x) end module UnivLevelSet = U.Set.Make(UnivLevelOrd) @@ -207,7 +207,7 @@ let universe_level_variable = CD.name = "univ.variable"; doc = "universe level variable"; pp = (fun fmt x -> - let s = Pp.string_of_ppcmds (Univ.Level.pr x) in + let s = Pp.string_of_ppcmds (UnivNames.pr_with_global_universes x) in Format.fprintf fmt "«%s»" s); compare = Univ.Level.compare; hash = Univ.Level.hash; @@ -477,7 +477,7 @@ let uinstancein, isuinstance, uinstanceout, uinstance = CD.name = "univ-instance"; doc = "Universes level instance for a universe-polymoprhic constant"; pp = (fun fmt x -> - let s = Pp.string_of_ppcmds (Univ.Instance.pr Univ.Level.pr x) in + let s = Pp.string_of_ppcmds (Univ.Instance.pr UnivNames.pr_with_global_universes x) in Format.fprintf fmt "«%s»" s); compare = (fun x y -> CArray.compare Univ.Level.compare (Univ.Instance.to_array x) (Univ.Instance.to_array y)); @@ -1643,8 +1643,8 @@ module UIM = F.Map(struct type t = Univ.Instance.t let compare i1 i2 = CArray.compare Univ.Level.compare (Univ.Instance.to_array i1) (Univ.Instance.to_array i2) - let show x = Pp.string_of_ppcmds @@ Univ.Instance.pr Univ.Level.pr x - let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (Univ.Instance.pr Univ.Level.pr x) + let show x = Pp.string_of_ppcmds @@ Univ.Instance.pr UnivNames.pr_with_global_universes x + let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (Univ.Instance.pr UnivNames.pr_with_global_universes x) end) let uim = S.declare ~name:"coq-elpi:evar-univ-instance-map" @@ -1777,9 +1777,9 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals let state, gr = in_coq_gref ~depth ~origin:t ~failsafe:coq_ctx.options.failsafe state d in begin match gr with | G.VarRef x -> state, EC.mkVar x, [] - | G.ConstRef x -> state, EC.mkConst x, [] - | G.ConstructRef x -> state, EC.mkConstruct x, [] - | G.IndRef x -> state, EC.mkInd x, [] + | G.ConstRef x -> state, EC.UnsafeMonomorphic.mkConst x, [] + | G.ConstructRef x -> state, EC.UnsafeMonomorphic.mkConstruct x, [] + | G.IndRef x -> state, EC.UnsafeMonomorphic.mkInd x, [] end | E.App(c,d,[i]) when pglobalc == c -> let state, gr, i, gls = @@ -1879,7 +1879,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals | _ -> assert false end Sorts.Relevant C.LetStyle in let b = List.hd bt in - let l, _ = EC.decompose_lam (get_sigma state) b in + let l, _ = EC.decompose_lambda (get_sigma state) b in let ci_pp_info = { unknown_ind_cinfo.Constr.ci_pp_info with Constr.cstr_tags = [| List.map (fun _ -> false) l |] } in { unknown_ind_cinfo with Constr.ci_pp_info} in @@ -1915,7 +1915,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals begin match v with | Uint63 i -> state, EC.mkInt i, gls | Float64 f -> state, EC.mkFloat f, gls - | Projection p -> state, EC.mkConst (Names.Projection.constant p), gls + | Projection p -> state, EC.UnsafeMonomorphic.mkConst (Names.Projection.constant p), gls end (* evar *) @@ -3134,7 +3134,7 @@ let inductive_decl2lp ~depth coq_ctx constraints state (mutind,uinst,(mind,ind), let sigma = get_sigma state in let drop_nparams_from_term n x = let x = EConstr.of_constr x in - let ctx, sort = EConstr.decompose_prod_assum sigma x in + let ctx, sort = EConstr.decompose_prod_decls sigma x in let ctx = drop_nparams_from_ctx n ctx in EConstr.it_mkProd_or_LetIn sort ctx in let decl = @@ -3147,7 +3147,7 @@ let inductive_decl2lp ~depth coq_ctx constraints state (mutind,uinst,(mind,ind), Term.it_mkProd_or_LetIn x ctx |> Inductive.abstract_constructor_type_relatively_to_inductive_types_context ntyps mutind in let nonexpimplsno = List.length (nonexpimpls impls) in - let ctx, typ = Term.decompose_prod_n_assum (max allparamsno nonexpimplsno) x in + let ctx, typ = Term.decompose_prod_n_decls (max allparamsno nonexpimplsno) x in let ctx = EConstr.of_rel_context ctx in let typ = EConstr.of_constr typ in let ctx = safe_combine2_impls ctx impls ~default2:Glob_term.Explicit in @@ -3301,7 +3301,7 @@ let record_entry2lp ~depth coq_ctx constraints state ~loose_udecl e = let kid = List.hd ind.mind_entry_consnames in let fieldsno = List.length record.proj_flags in - let kctx, _ = Term.decompose_prod_assum @@ List.hd ind.mind_entry_lc in + let kctx, _ = Term.decompose_prod_decls @@ List.hd ind.mind_entry_lc in let kctx = EConstr.of_rel_context kctx in if (List.length kctx != fieldsno) then CErrors.anomaly Pp.(str"record fields number != projections"); @@ -3403,7 +3403,7 @@ let lp2skeleton ~depth coq_ctx constraints state t = let gt = let is_GRef_hole x = match DAst.get x with - | Glob_term.GRef(r,None) -> Names.GlobRef.equal r (Coqlib.lib_ref "elpi.hole") + | Glob_term.GRef(r,None) -> Environ.QGlobRef.equal coq_ctx.env r (Coqlib.lib_ref "elpi.hole") | _ -> false in let rec map x = match DAst.get x with | Glob_term.GEvar _ -> mkGHole diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 8af7adf72..8e9c74e0a 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -149,7 +149,7 @@ let err_if_contains_alg_univ ~depth t = begin match Univ.Universe.level u with | None -> err Pp.(strbrk "The hypothetical clause contains terms of type univ which are not global, you should abstract them out or replace them by global ones: " ++ - Univ.Universe.pr u) + Univ.Universe.pr UnivNames.pr_with_global_universes u) | _ -> Univ.Universe.Set.add u acc end | x -> Coq_elpi_utils.fold_elpi_term aux acc ~depth x @@ -2056,7 +2056,7 @@ Supported attributes: let is_implicit = List.map (fun _ -> []) names in let open Entries in let k_ty = List.(hd (hd me.mind_entry_inds).mind_entry_lc) in - let fields_as_relctx = Term.prod_assum k_ty in + let fields_as_relctx = Term.prod_decls k_ty in let projections = Record.Internal.declare_projections ind ~kind:Decls.Definition (uentry, ubinders) diff --git a/src/coq_elpi_programs.ml b/src/coq_elpi_programs.ml index d65b011fe..9ce389a97 100644 --- a/src/coq_elpi_programs.ml +++ b/src/coq_elpi_programs.ml @@ -14,8 +14,8 @@ let debug_vars = Summary.ref ~name:"elpi-debug" EC.StrSet.empty let cc_flags () = { EC.default_flags with EC.defined_variables = !debug_vars } -let source_cache1 = Summary.Local.ref ~name:"elpi-units1" Names.KNmap.empty -let source_cache2 = Summary.Local.ref ~name:"elpi-units2" CString.Map.empty +let source_cache1 = Summary.ref ~local:true ~name:"elpi-units1" Names.KNmap.empty +let source_cache2 = Summary.ref ~local:true ~name:"elpi-units2" CString.Map.empty let last_kn = ref None @@ -23,7 +23,6 @@ let in_source : Names.Id.t -> string option * EC.compilation_unit * EC.flags -> let open Libobject in let cache ((_,kn), (hash,u,cf)) = last_kn := Some kn; - let open Summary.Local in source_cache1 := Names.KNmap.add kn (u,cf) !source_cache1; hash |> Option.iter (fun hash -> source_cache2 := CString.Map.add hash kn !source_cache2); in @@ -46,7 +45,6 @@ let intern_unit (hash,u,flags) = last_kn := None; Lib.add_leaf (in_source id (hash,u,flags)); let kn = Option.get !last_kn in - let open Summary.Local in let u,_ = Names.KNmap.find kn !source_cache1 in kn,u @@ -61,7 +59,6 @@ let unit_from_ast ~elpi ~flags h ast = CErrors.user_err ?loc Pp.(str (Option.default "" @@ Option.map API.Ast.Loc.show oloc) ++ cut () ++ str msg) let unit_from_file ~elpi x : cunit = - let open Summary.Local in let flags = cc_flags () in let hash = Digest.(to_hex @@ file (EP.resolve_file ~elpi ~unit:x ())) in try diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index 7b55be128..a6f12af88 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -55,33 +55,30 @@ let bound_steps n = (* Units are marshalable, but programs are not *) -let compiler_cache_code = Summary.Local.ref +let compiler_cache_code = Summary.ref ~local:true ~name:"elpi-compiler-cache-code" Int.Map.empty -let compiler_cache_chunk = Summary.Local.ref +let compiler_cache_chunk = Summary.ref ~local:true ~name:"elpi-compiler-cache-chunk" Int.Map.empty -let programs_tip = Summary.Local.ref +let programs_tip = Summary.ref ~local:true ~name:"elpi-compiler-cache-gc" SLMap.empty (* lookup/cache for hash h shifted over base b *) let lookup b h src r cmp = - let open Summary.Local in let h = combine_hash b h in let p, src' = Int.Map.find h !r in if cmp src src' then p else assert false let cache b h prog src r = - let open Summary.Local in let h = combine_hash b h in r := Int.Map.add h (prog,src) !r; prog let uncache b h r = - let open Summary.Local in let h = combine_hash b h in r := Int.Map.remove h !r @@ -100,7 +97,6 @@ let recache_chunk b h1 h2 p src = cache_chunk b h2 p src let get_and_compile name = - let open Summary.Local in let src = code name in let prog = let rec compile_code src = From dfe4a8de8306d99bf44af843fe9373b02314a2d8 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 28 Jun 2023 15:11:33 +0200 Subject: [PATCH 31/35] Add coercion app --- Changelog.md | 5 +++ Makefile | 2 +- README.md | 4 ++- _CoqProject | 1 + apps/coercion/Makefile | 40 ++++++++++++++++++++++++ apps/coercion/README.md | 25 +++++++++++++++ apps/coercion/_CoqProject | 9 ++++++ apps/coercion/_CoqProject.test | 10 ++++++ apps/coercion/tests/test_coercion.v | 34 ++++++++++++++++++++ apps/coercion/tests/test_coercion_load.v | 3 ++ apps/coercion/theories/coercion.v | 19 +++++++++++ src/coq_elpi_arg_HOAS.ml | 5 +++ src/coq_elpi_arg_HOAS.mli | 10 ++++++ src/coq_elpi_vernacular.ml | 40 +++++++++++++++++++++++- src/coq_elpi_vernacular.mli | 1 + src/coq_elpi_vernacular_syntax.mlg | 4 +++ 16 files changed, 209 insertions(+), 3 deletions(-) create mode 100644 apps/coercion/Makefile create mode 100644 apps/coercion/README.md create mode 100644 apps/coercion/_CoqProject create mode 100644 apps/coercion/_CoqProject.test create mode 100644 apps/coercion/tests/test_coercion.v create mode 100644 apps/coercion/tests/test_coercion_load.v create mode 100644 apps/coercion/theories/coercion.v diff --git a/Changelog.md b/Changelog.md index ca025b611..cb28294ef 100644 --- a/Changelog.md +++ b/Changelog.md @@ -62,6 +62,11 @@ Requires Elpi 1.16.5 and Coq 8.17. - `derive Inductive i {A}` now sets `A` implicit status globally - `lock Definition f {A}` now sets `A` implicit status globally +### APPS +- New `coercion` app providing `coercion` predicate + to program coercions (requires appropriate version of Coq + with coercion hook https://github.com/coq/coq/pull/17794 ) + ## [1.17.1] - 09/03/2023 Requires Elpi 1.16.5 and Coq 8.17. diff --git a/Makefile b/Makefile index f10353683..8455c470a 100644 --- a/Makefile +++ b/Makefile @@ -21,7 +21,7 @@ export ELPIDIR DEPS=$(ELPIDIR)/elpi.cmxa $(ELPIDIR)/elpi.cma -APPS=$(addprefix apps/, derive eltac NES locker) +APPS=$(addprefix apps/, derive eltac NES locker coercion) ifeq "$(COQ_ELPI_ALREADY_INSTALLED)" "" DOCDEP=build diff --git a/README.md b/README.md index ddb40ed50..bcb537507 100644 --- a/README.md +++ b/README.md @@ -152,7 +152,9 @@ all the dependencies installed first (see [coq-elpi.opam](coq-elpi.opam)). - [Dx](https://gitlab.univ-lille.fr/samuel.hym/dx) uses elpi to generate an intermediate representation of Coq terms, to be later tranformed into C. - +- [Coercion](apps/coercion) enable to program coercions in Elpi. + It comes bundled with Coq-Elpi. + ### Quick Reference In order to load Coq-Elpi use `From elpi Require Import elpi`. diff --git a/_CoqProject b/_CoqProject index 13c179c0a..1e0d91b72 100644 --- a/_CoqProject +++ b/_CoqProject @@ -17,6 +17,7 @@ -R apps/eltac/theories elpi.apps.eltac -R apps/eltac/tests elpi.apps.eltac.tests -R apps/eltac/examples elpi.apps.eltac.examples +-R apps/coercion/theories elpi.apps.coercion theories/elpi.v theories/wip/memoization.v diff --git a/apps/coercion/Makefile b/apps/coercion/Makefile new file mode 100644 index 000000000..9b84ee407 --- /dev/null +++ b/apps/coercion/Makefile @@ -0,0 +1,40 @@ +# detection of coq +ifeq "$(COQBIN)" "" +COQBIN := $(shell which coqc >/dev/null 2>&1 && dirname `which coqc`) +endif +ifeq "$(COQBIN)" "" +$(error Coq not found, make sure it is installed in your PATH or set COQBIN) +else +$(info Using coq found in $(COQBIN), from COQBIN or PATH) +endif +export COQBIN := $(COQBIN)/ + +all: build test + +build: Makefile.coq + @$(MAKE) --no-print-directory -f Makefile.coq + +test: Makefile.test.coq + @$(MAKE) --no-print-directory -f Makefile.test.coq + +theories/%.vo: force + @$(MAKE) --no-print-directory -f Makefile.coq $@ +tests/%.vo: force build Makefile.test.coq + @$(MAKE) --no-print-directory -f Makefile.test.coq $@ +examples/%.vo: force build Makefile.test.coq + @$(MAKE) --no-print-directory -f Makefile.test.coq $@ + +Makefile.coq Makefile.coq.conf: _CoqProject + @$(COQBIN)/coq_makefile -f _CoqProject -o Makefile.coq + @$(MAKE) --no-print-directory -f Makefile.coq .merlin +Makefile.test.coq Makefile.test.coq.conf: _CoqProject.test + @$(COQBIN)/coq_makefile -f _CoqProject.test -o Makefile.test.coq + +clean: Makefile.coq Makefile.test.coq + @$(MAKE) -f Makefile.coq $@ + @$(MAKE) -f Makefile.test.coq $@ + +.PHONY: force all build test + +install: + @$(MAKE) -f Makefile.coq $@ diff --git a/apps/coercion/README.md b/apps/coercion/README.md new file mode 100644 index 000000000..049f647f3 --- /dev/null +++ b/apps/coercion/README.md @@ -0,0 +1,25 @@ +# Coercion + +The `coercion` predicate enables to program Coq coercions in Elpi. + +## Example of `coercion` + +```coq +From elpi.apps Require Import coercion. + +Elpi Accumulate Coercion lp:{{ + +coercion _ {{ true }} {{ bool }} {{ Prop }} {{ True }}. +coercion _ {{ false }} {{ bool }} {{ Prop }} {{ False }}. + +}}. +Elpi Typecheck Coercion. + +Check true : Prop. +Check false : Prop. +``` + +## Requirements + +Appropriate version of Coq with support for coercion hooks +https://github.com/coq/coq/pull/17794 diff --git a/apps/coercion/_CoqProject b/apps/coercion/_CoqProject new file mode 100644 index 000000000..4de7cb8dc --- /dev/null +++ b/apps/coercion/_CoqProject @@ -0,0 +1,9 @@ +# Hack to see Coq-Elpi even if it is not installed yet +-Q ../../theories elpi +-I ../../src +-docroot elpi.apps + +-R theories elpi.apps +-R elpi elpi.apps.coercion + +theories/coercion.v diff --git a/apps/coercion/_CoqProject.test b/apps/coercion/_CoqProject.test new file mode 100644 index 000000000..e3c5855b0 --- /dev/null +++ b/apps/coercion/_CoqProject.test @@ -0,0 +1,10 @@ +# Hack to see Coq-Elpi even if it is not installed yet +-Q ../../theories elpi +-I ../../src +-docroot elpi.apps + +-R theories elpi.apps +-R tests elpi.apps.coercion.tests + +tests/test_coercion.v +tests/test_coercion_load.v diff --git a/apps/coercion/tests/test_coercion.v b/apps/coercion/tests/test_coercion.v new file mode 100644 index 000000000..76f75527e --- /dev/null +++ b/apps/coercion/tests/test_coercion.v @@ -0,0 +1,34 @@ +From elpi.apps Require Import coercion. + +Elpi Accumulate Coercion lp:{{ + +coercion _ {{ true }} {{ bool }} {{ Prop }} {{ True }}. +coercion _ {{ false }} {{ bool }} {{ Prop }} {{ False }}. + +}}. +Elpi Typecheck Coercion. + +Check true : Prop. +Check false : Prop. + +Parameter ringType : Type. +Parameter ringType_sort : ringType -> Type. +Parameter natmul : forall (R : ringType) (n : nat), (ringType_sort R). + +Elpi Accumulate Coercion lp:{{ + +coercion _ N {{ nat }} {{ ringType_sort lp:R }} {{ natmul lp:R lp:N }} :- + coq.typecheck R {{ ringType }} ok. + +}}. +Elpi Typecheck Coercion. + +Section TestNatMul. + +Variable R : ringType. +Variable n : nat. + +Check natmul R n : ringType_sort R. +Check n : ringType_sort R. + +End TestNatMul. diff --git a/apps/coercion/tests/test_coercion_load.v b/apps/coercion/tests/test_coercion_load.v new file mode 100644 index 000000000..67e55fa18 --- /dev/null +++ b/apps/coercion/tests/test_coercion_load.v @@ -0,0 +1,3 @@ +Require Import test_coercion. + +Check true : Prop. diff --git a/apps/coercion/theories/coercion.v b/apps/coercion/theories/coercion.v new file mode 100644 index 000000000..97647c255 --- /dev/null +++ b/apps/coercion/theories/coercion.v @@ -0,0 +1,19 @@ +From elpi Require Import elpi. + +Elpi Tactic Coercion. +Elpi Accumulate lp:{{ + +% predicate [coercion Ctx V Inferred Expected Res] used to add new coercion, with +% - [Ctx] is the context +% - [V] is the value to be coerced +% - [Inferred] is the type of [V] +% - [Expected] is the type [V] should be coerced to +% - [Res] is the result (of type [Expected]) +% Be careful not to trigger coercion as this may loop. +pred coercion i:goal-ctx, i:term, i:term, i:term, o:term. + +solve (goal Ctx _ Ty Sol [trm V, trm VTy]) _ :- coercion Ctx V VTy Ty Sol. + +}}. +Elpi Typecheck. +Elpi AddCoercionHook Coercion. diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml index 54db82582..83875d7f1 100644 --- a/src/coq_elpi_arg_HOAS.ml +++ b/src/coq_elpi_arg_HOAS.ml @@ -684,6 +684,11 @@ let in_elpi_term_arg ~depth state coq_ctx hyps sigma ist glob_or_expr = let state, t = Coq_elpi_glob_quotation.gterm2lp ~depth state g in state, E.mkApp trmc t [], [] +let in_elpi_tac_econstr ~depth ?calldepth coq_ctx hyps sigma state x = + let state, gls0 = set_current_sigma ~depth state sigma in + let state, t, gls1 = Coq_elpi_HOAS.constr2lp ~depth ?calldepth coq_ctx E.no_constraints state x in + state, [E.mkApp trmc t []], gls0 @ gls1 + let in_elpi_elab_term_arg ~depth ?calldepth state coq_ctx hyps sigma ist glob_or_expr = let sigma, t = Ltac_plugin.Tacinterp.interp_open_constr_with_classes ist coq_ctx.env sigma glob_or_expr in let state, gls0 = set_current_sigma ~depth state sigma in diff --git a/src/coq_elpi_arg_HOAS.mli b/src/coq_elpi_arg_HOAS.mli index 56d3901b8..09a08a4c6 100644 --- a/src/coq_elpi_arg_HOAS.mli +++ b/src/coq_elpi_arg_HOAS.mli @@ -95,6 +95,16 @@ val in_elpi_tac : Tac.top -> Elpi.API.State.t * term list * Elpi.API.Conversion.extra_goals +(* for coercions *) +val in_elpi_tac_econstr : + depth:int -> ?calldepth:int -> + Coq_elpi_HOAS.full Coq_elpi_HOAS.coq_context -> + Coq_elpi_HOAS.hyp list -> + Evd.evar_map -> + Elpi.API.State.t -> + EConstr.t -> + Elpi.API.State.t * term list * Elpi.API.Conversion.extra_goals + (* for commands *) val in_elpi_cmd : depth:int -> ?calldepth:int -> diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index a6f12af88..304e15940 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -501,4 +501,42 @@ let skip ~atts:(skip,only) f x = in if exec then f x else () - +let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected = + let loc = API.Ast.Loc.initial "(unknown)" in + let atts = [] in + let sigma, goal = Evarutil.new_evar env sigma expected in + let goal_evar, _ = EConstr.destEvar sigma goal in + let query ~depth state = + let state, (loc, q), gls = + Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve [v; inferred]) + ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth state in + let state, qatts = atts2impl loc ~depth state atts q in + let state = API.State.set Coq_elpi_builtins.tactic_mode state true in + state, (loc, qatts), gls + in + let cprogram, _ = get_and_compile program in + match run ~static_check:false cprogram (`Fun query) with + | API.Execute.Success solution -> + let gls = Evar.Set.singleton goal_evar in + let sigma, _, _ = Coq_elpi_HOAS.solution2evd sigma solution gls in + if Evd.is_defined sigma goal_evar then Some (sigma, goal) else None + | API.Execute.NoMoreSteps + | API.Execute.Failure -> None + | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None + +let add_coercion_hook = + let coercion_hook_program = Summary.ref ~name:"elpi-coercion" None in + let coercion_hook env sigma ~flags v ~inferred ~expected = + match !coercion_hook_program with + | None -> None + | Some h -> elpi_coercion_hook h env sigma ~flags v ~inferred ~expected in + let name = "elpi-coercion" in + Coercion.register_hook ~name coercion_hook; + let inCoercion = + let cache program = + coercion_hook_program := Some program; + Coercion.activate_hook ~name in + let open Libobject in + declare_object + @@ superglobal_object_nodischarge "ELPI-COERCION" ~cache ~subst:None in + fun program -> Lib.add_leaf (inCoercion program) diff --git a/src/coq_elpi_vernacular.mli b/src/coq_elpi_vernacular.mli index bfd44adad..995814856 100644 --- a/src/coq_elpi_vernacular.mli +++ b/src/coq_elpi_vernacular.mli @@ -44,3 +44,4 @@ val run_in_tactic : ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> Ge val export_command : qualified_name -> unit +val add_coercion_hook : Coq_elpi_utils.qualified_name -> unit diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg index fdbe84a33..42c52978b 100644 --- a/src/coq_elpi_vernacular_syntax.mlg +++ b/src/coq_elpi_vernacular_syntax.mlg @@ -209,6 +209,10 @@ VERNAC COMMAND EXTEND Elpi CLASSIFIED AS SIDEFF let () = ignore_unknown_attributes atts in EV.load_tactic s } +| #[ atts = any_attribute ] [ "Elpi" "AddCoercionHook" qualified_name(p) ] -> { + let () = ignore_unknown_attributes atts in + Coq_elpi_vernacular.add_coercion_hook (snd p) } + END VERNAC COMMAND EXTEND ElpiRun CLASSIFIED BY { fun _ -> Vernacextend.(VtSideff ([], VtNow)) } From 102b7790f7ba7cb1610eab8cb9c3d95a9667f854 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 30 Jul 2023 15:19:07 +0200 Subject: [PATCH 32/35] fix ci --- .github/workflows/main.yml | 2 +- .github/workflows/nix-action-coq-8.17.yml | 1278 --------------------- 2 files changed, 1 insertion(+), 1279 deletions(-) delete mode 100644 .github/workflows/nix-action-coq-8.17.yml diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 35f958b78..8de5871a4 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -16,7 +16,7 @@ jobs: strategy: matrix: coq_version: - - 'dev' + - '8.18' ocaml_version: - '4.09-flambda' - '4.13-flambda' diff --git a/.github/workflows/nix-action-coq-8.17.yml b/.github/workflows/nix-action-coq-8.17.yml deleted file mode 100644 index 1c46b950d..000000000 --- a/.github/workflows/nix-action-coq-8.17.yml +++ /dev/null @@ -1,1278 +0,0 @@ -jobs: - addition-chains: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-algebra - - mathcomp-fingroup - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target addition-chains - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"addition-chains\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: paramcoq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "paramcoq" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "addition-chains" - category-theory: - needs: - - coq - - mathcomp-ssreflect - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target category-theory - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"category-theory\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: equations' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "equations" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "category-theory" - coq: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - coq-elpi: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target coq-elpi - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"coq-elpi\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq-elpi" - coquelicot: - needs: - - coq - - mathcomp-ssreflect - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target coquelicot - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"coquelicot\" \\\n --dry-run 2>&1 >\ - \ /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coquelicot" - hierarchy-builder: - needs: - - coq - - coq-elpi - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target hierarchy-builder - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"hierarchy-builder\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq-elpi' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq-elpi" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "hierarchy-builder" - interval: - needs: - - coq - - coquelicot - - mathcomp-ssreflect - - mathcomp-fingroup - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target interval - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"interval\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: bignums' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "bignums" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coquelicot' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coquelicot" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: flocq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "flocq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "interval" - mathcomp: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-fingroup - - mathcomp-algebra - - mathcomp-solvable - - mathcomp-field - - mathcomp-character - - hierarchy-builder - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target mathcomp - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-character" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp" - mathcomp-algebra: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-fingroup - - hierarchy-builder - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target mathcomp-algebra - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"mathcomp-algebra\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-algebra" - mathcomp-analysis: - needs: - - coq - - mathcomp-classical - - mathcomp-field - - mathcomp-bigenough - - hierarchy-builder - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target mathcomp-analysis - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"mathcomp-analysis\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-classical' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-classical" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-analysis" - mathcomp-bigenough: - needs: - - coq - - mathcomp-ssreflect - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target mathcomp-bigenough - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-bigenough" - mathcomp-character: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-fingroup - - mathcomp-algebra - - mathcomp-solvable - - mathcomp-field - - hierarchy-builder - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target mathcomp-character - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"mathcomp-character\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-character" - mathcomp-classical: - needs: - - coq - - mathcomp-algebra - - hierarchy-builder - - hierarchy-builder - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target mathcomp-classical - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"mathcomp-classical\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-classical" - mathcomp-field: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-fingroup - - mathcomp-algebra - - mathcomp-solvable - - hierarchy-builder - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target mathcomp-field - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"mathcomp-field\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-field" - mathcomp-fingroup: - needs: - - coq - - mathcomp-ssreflect - - hierarchy-builder - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target mathcomp-fingroup - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"mathcomp-fingroup\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-fingroup" - mathcomp-solvable: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-fingroup - - mathcomp-algebra - - hierarchy-builder - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target mathcomp-solvable - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"mathcomp-solvable\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-solvable" - mathcomp-ssreflect: - needs: - - coq - - hierarchy-builder - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target mathcomp-ssreflect - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"mathcomp-ssreflect\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-ssreflect" - odd-order: - needs: - - coq - - mathcomp-character - - mathcomp-ssreflect - - mathcomp-fingroup - - mathcomp-algebra - - mathcomp-solvable - - mathcomp-field - - mathcomp - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target odd-order - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"odd-order\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-character" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "odd-order" - trakt: - needs: - - coq - - coq-elpi - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target trakt - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"trakt\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq-elpi' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "coq-elpi" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "trakt" -name: Nix CI for bundle coq-8.17 -'on': - pull_request: - paths: - - .github/workflows/** - pull_request_target: - types: - - opened - - synchronize - - reopened - push: - branches: - - master From 89d56fafcb27d0ec21d934a3fce926de682728f9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 30 Jul 2023 22:58:55 +0200 Subject: [PATCH 33/35] move coercion hook code to the app --- .gitignore | 3 + apps/coercion/Makefile.coq.local | 3 + apps/coercion/_CoqProject | 7 ++- apps/coercion/_CoqProject.test | 2 + apps/coercion/src/META.coq-elpi-coercion | 10 ++++ apps/coercion/src/coq_elpi_coercion_hook.mlg | 58 +++++++++++++++++++ apps/coercion/src/elpi_coercion_plugin.mlpack | 1 + apps/coercion/theories/coercion.v | 1 + src/coq_elpi_vernacular.ml | 40 ------------- src/coq_elpi_vernacular.mli | 16 ++++- src/coq_elpi_vernacular_syntax.mlg | 5 -- 11 files changed, 99 insertions(+), 47 deletions(-) create mode 100644 apps/coercion/Makefile.coq.local create mode 100644 apps/coercion/src/META.coq-elpi-coercion create mode 100644 apps/coercion/src/coq_elpi_coercion_hook.mlg create mode 100644 apps/coercion/src/elpi_coercion_plugin.mlpack diff --git a/.gitignore b/.gitignore index feceb2a0a..a8d712e50 100644 --- a/.gitignore +++ b/.gitignore @@ -44,3 +44,6 @@ tests/test_glob/*.css META *.cache + +apps/coercion/src/coq_elpi_coercion_hook.ml +.filestoinstall \ No newline at end of file diff --git a/apps/coercion/Makefile.coq.local b/apps/coercion/Makefile.coq.local new file mode 100644 index 000000000..f120308b2 --- /dev/null +++ b/apps/coercion/Makefile.coq.local @@ -0,0 +1,3 @@ +CAMLPKGS+= -package coq-elpi.elpi +OCAMLPATH:=../../src/:$(OCAMLPATH) +export OCAMLPATH \ No newline at end of file diff --git a/apps/coercion/_CoqProject b/apps/coercion/_CoqProject index 4de7cb8dc..b5b8d84f0 100644 --- a/apps/coercion/_CoqProject +++ b/apps/coercion/_CoqProject @@ -4,6 +4,11 @@ -docroot elpi.apps -R theories elpi.apps --R elpi elpi.apps.coercion + +src/coq_elpi_coercion_hook.mlg +src/elpi_coercion_plugin.mlpack + +-I src/ +src/META.coq-elpi-coercion theories/coercion.v diff --git a/apps/coercion/_CoqProject.test b/apps/coercion/_CoqProject.test index e3c5855b0..045d669b9 100644 --- a/apps/coercion/_CoqProject.test +++ b/apps/coercion/_CoqProject.test @@ -8,3 +8,5 @@ tests/test_coercion.v tests/test_coercion_load.v + +-I src diff --git a/apps/coercion/src/META.coq-elpi-coercion b/apps/coercion/src/META.coq-elpi-coercion new file mode 100644 index 000000000..507e9af0e --- /dev/null +++ b/apps/coercion/src/META.coq-elpi-coercion @@ -0,0 +1,10 @@ + +package "plugin" ( + directory = "." + requires = "coq-core.plugins.ltac coq-elpi.elpi" + archive(byte) = "elpi_coercion_plugin.cma" + archive(native) = "elpi_coercion_plugin.cmxa" + plugin(byte) = "elpi_coercion_plugin.cma" + plugin(native) = "elpi_coercion_plugin.cmxs" +) +directory = "." diff --git a/apps/coercion/src/coq_elpi_coercion_hook.mlg b/apps/coercion/src/coq_elpi_coercion_hook.mlg new file mode 100644 index 000000000..dd2a4bc30 --- /dev/null +++ b/apps/coercion/src/coq_elpi_coercion_hook.mlg @@ -0,0 +1,58 @@ +DECLARE PLUGIN "coq-elpi-coercion.plugin" + +{ + +open Elpi +open Elpi_plugin +open Coq_elpi_arg_syntax +open Coq_elpi_vernacular + + +let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected = + let loc = API.Ast.Loc.initial "(unknown)" in + let atts = [] in + let sigma, goal = Evarutil.new_evar env sigma expected in + let goal_evar, _ = EConstr.destEvar sigma goal in + let query ~depth state = + let state, (loc, q), gls = + Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve [v; inferred]) + ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth state in + let state, qatts = atts2impl loc ~depth state atts q in + let state = API.State.set Coq_elpi_builtins.tactic_mode state true in + state, (loc, qatts), gls + in + let cprogram, _ = get_and_compile program in + match run ~static_check:false cprogram (`Fun query) with + | API.Execute.Success solution -> + let gls = Evar.Set.singleton goal_evar in + let sigma, _, _ = Coq_elpi_HOAS.solution2evd sigma solution gls in + if Evd.is_defined sigma goal_evar then Some (sigma, goal) else None + | API.Execute.NoMoreSteps + | API.Execute.Failure -> None + | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None + +let add_coercion_hook = + let coercion_hook_program = Summary.ref ~name:"elpi-coercion" None in + let coercion_hook env sigma ~flags v ~inferred ~expected = + match !coercion_hook_program with + | None -> None + | Some h -> elpi_coercion_hook h env sigma ~flags v ~inferred ~expected in + let name = "elpi-coercion" in + Coercion.register_hook ~name coercion_hook; + let inCoercion = + let cache program = + coercion_hook_program := Some program; + Coercion.activate_hook ~name in + let open Libobject in + declare_object + @@ superglobal_object_nodischarge "ELPI-COERCION" ~cache ~subst:None in + fun program -> Lib.add_leaf (inCoercion program) + +} + +VERNAC COMMAND EXTEND ElpiCoercion CLASSIFIED AS SIDEFF +| #[ atts = any_attribute ] [ "Elpi" "AddCoercionHook" qualified_name(p) ] -> { + let () = ignore_unknown_attributes atts in + add_coercion_hook (snd p) } + +END \ No newline at end of file diff --git a/apps/coercion/src/elpi_coercion_plugin.mlpack b/apps/coercion/src/elpi_coercion_plugin.mlpack new file mode 100644 index 000000000..0e41afce5 --- /dev/null +++ b/apps/coercion/src/elpi_coercion_plugin.mlpack @@ -0,0 +1 @@ +Coq_elpi_coercion_hook \ No newline at end of file diff --git a/apps/coercion/theories/coercion.v b/apps/coercion/theories/coercion.v index 97647c255..352d4dc47 100644 --- a/apps/coercion/theories/coercion.v +++ b/apps/coercion/theories/coercion.v @@ -1,3 +1,4 @@ +Declare ML Module "coq-elpi-coercion.plugin". From elpi Require Import elpi. Elpi Tactic Coercion. diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index 304e15940..6fb16636c 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -500,43 +500,3 @@ let skip ~atts:(skip,only) f x = | Some _, Some _ -> CErrors.user_err Pp.(str "Attributes #[skip] and #[only] cannot be used at the same time") in if exec then f x else () - -let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected = - let loc = API.Ast.Loc.initial "(unknown)" in - let atts = [] in - let sigma, goal = Evarutil.new_evar env sigma expected in - let goal_evar, _ = EConstr.destEvar sigma goal in - let query ~depth state = - let state, (loc, q), gls = - Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve [v; inferred]) - ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth state in - let state, qatts = atts2impl loc ~depth state atts q in - let state = API.State.set Coq_elpi_builtins.tactic_mode state true in - state, (loc, qatts), gls - in - let cprogram, _ = get_and_compile program in - match run ~static_check:false cprogram (`Fun query) with - | API.Execute.Success solution -> - let gls = Evar.Set.singleton goal_evar in - let sigma, _, _ = Coq_elpi_HOAS.solution2evd sigma solution gls in - if Evd.is_defined sigma goal_evar then Some (sigma, goal) else None - | API.Execute.NoMoreSteps - | API.Execute.Failure -> None - | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None - -let add_coercion_hook = - let coercion_hook_program = Summary.ref ~name:"elpi-coercion" None in - let coercion_hook env sigma ~flags v ~inferred ~expected = - match !coercion_hook_program with - | None -> None - | Some h -> elpi_coercion_hook h env sigma ~flags v ~inferred ~expected in - let name = "elpi-coercion" in - Coercion.register_hook ~name coercion_hook; - let inCoercion = - let cache program = - coercion_hook_program := Some program; - Coercion.activate_hook ~name in - let open Libobject in - declare_object - @@ superglobal_object_nodischarge "ELPI-COERCION" ~cache ~subst:None in - fun program -> Lib.add_leaf (inCoercion program) diff --git a/src/coq_elpi_vernacular.mli b/src/coq_elpi_vernacular.mli index 995814856..ac3ca1eef 100644 --- a/src/coq_elpi_vernacular.mli +++ b/src/coq_elpi_vernacular.mli @@ -44,4 +44,18 @@ val run_in_tactic : ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> Ge val export_command : qualified_name -> unit -val add_coercion_hook : Coq_elpi_utils.qualified_name -> unit +val atts2impl : + Elpi.API.Ast.Loc.t -> depth:int -> Elpi.API.State.t -> Attributes.vernac_flags -> + Elpi.API.Data.term -> Elpi.API.State.t * Elpi.API.Data.term +val get_and_compile : + qualified_name -> Elpi.API.Compile.program * bool +val run : static_check:bool -> + Elpi.API.Compile.program -> + [ `Ast of Elpi.API.Ast.query + | `Fun of + depth:int -> + Elpi.API.State.t -> + Elpi.API.State.t * + (Elpi.API.Ast.Loc.t * Elpi.API.Data.term) * + Elpi.API.Conversion.extra_goals ] -> + unit Elpi.API.Execute.outcome \ No newline at end of file diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg index 42c52978b..a81d1a39a 100644 --- a/src/coq_elpi_vernacular_syntax.mlg +++ b/src/coq_elpi_vernacular_syntax.mlg @@ -208,11 +208,6 @@ VERNAC COMMAND EXTEND Elpi CLASSIFIED AS SIDEFF | #[ atts = any_attribute ] [ "Elpi" "Template" "Tactic" string(s) ] -> { let () = ignore_unknown_attributes atts in EV.load_tactic s } - -| #[ atts = any_attribute ] [ "Elpi" "AddCoercionHook" qualified_name(p) ] -> { - let () = ignore_unknown_attributes atts in - Coq_elpi_vernacular.add_coercion_hook (snd p) } - END VERNAC COMMAND EXTEND ElpiRun CLASSIFIED BY { fun _ -> Vernacextend.(VtSideff ([], VtNow)) } From b2cb068941c2509197e184d487edf6af2f1558c0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 31 Jul 2023 11:35:04 +0200 Subject: [PATCH 34/35] rework README for coercion --- apps/coercion/README.md | 77 +++++++++++++++++--- apps/coercion/_CoqProject.test | 1 + apps/coercion/src/coq_elpi_coercion_hook.mlg | 2 +- apps/coercion/tests/test_coercion.v | 16 ++-- apps/coercion/tests/test_coercion_load.v | 2 +- apps/coercion/tests/test_coercion_open.v | 29 ++++++++ apps/coercion/theories/coercion.v | 11 ++- 7 files changed, 114 insertions(+), 24 deletions(-) create mode 100644 apps/coercion/tests/test_coercion_open.v diff --git a/apps/coercion/README.md b/apps/coercion/README.md index 049f647f3..acd6131a4 100644 --- a/apps/coercion/README.md +++ b/apps/coercion/README.md @@ -1,25 +1,80 @@ # Coercion -The `coercion` predicate enables to program Coq coercions in Elpi. +The `coercion` app enables to program Coq coercions in Elpi. -## Example of `coercion` +This app is experimental. + +## The coercion predicate + +The `coercion` predicate lives in the database `coercion.db` + +```elpi +% [coercion Ctx V Inferred Expected Res] is queried to cast V to Res +% - [Ctx] is the context +% - [V] is the value to be coerced +% - [Inferred] is the type of [V] +% - [Expected] is the type [V] should be coerced to +% - [Res] is the result (of type [Expected]) +pred coercion i:goal-ctx, i:term, i:term, i:term, o:term. +``` + +By addings rules for this predicate one can recover from a type error, that is +when `Inferred` and `Expected` are not unifiable. + +## Simple example of coercion + +This example maps `True : Prop` to `true : bool`, which is a function you +cannot express in type theory, hence in the standard Coercion system. ```coq From elpi.apps Require Import coercion. +From Coq Require Import Bool. -Elpi Accumulate Coercion lp:{{ +Elpi Accumulate coercion.db lp:{{ -coercion _ {{ true }} {{ bool }} {{ Prop }} {{ True }}. -coercion _ {{ false }} {{ bool }} {{ Prop }} {{ False }}. +coercion _ {{ True }} {{ Prop }} {{ bool }} {{ true }}. +coercion _ {{ False }} {{ Prop }} {{ bool }} {{ false }}. }}. -Elpi Typecheck Coercion. +Elpi Typecheck coercion. (* checks the elpi program is OK *) -Check true : Prop. -Check false : Prop. +Check True && False. ``` -## Requirements +## Example of coercion with proof automation + +This coercion enriches `x : T` to a `{x : T | P x}` by using +`my_solver` to prove `P x`. + +```coq +From elpi.apps Require Import coercion. +From Coq Require Import Arith ssreflect. + +Ltac my_solver := trivial with arith. + +Elpi Accumulate coercion.db lp:{{ + +coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [ + % we unfold letins since the solver is dumb and the `as` in the second + % example introduces a letin + (pi a b b1\ copy a b :- def a _ _ b, copy b b1) => copy X X1, + % we build the solution + Solution = {{ @exist lp:Ty lp:P lp:X1 _ }}, + % we call the solver + coq.ltac.collect-goals Solution [G] [], + coq.ltac.open (coq.ltac.call-ltac1 "my_solver") G [], +]. -Appropriate version of Coq with support for coercion hooks -https://github.com/coq/coq/pull/17794 +}}. +Elpi Typecheck coercion. + +Goal {x : nat | x > 0}. +apply: 3. +Qed. + +Definition ensure_pos n : {x : nat | x > 0} := + match n with + | O => 1 + | S x as y => y + end. +``` diff --git a/apps/coercion/_CoqProject.test b/apps/coercion/_CoqProject.test index 045d669b9..e6e1f59ad 100644 --- a/apps/coercion/_CoqProject.test +++ b/apps/coercion/_CoqProject.test @@ -7,6 +7,7 @@ -R tests elpi.apps.coercion.tests tests/test_coercion.v +tests/test_coercion_open.v tests/test_coercion_load.v -I src diff --git a/apps/coercion/src/coq_elpi_coercion_hook.mlg b/apps/coercion/src/coq_elpi_coercion_hook.mlg index dd2a4bc30..89b8d0d45 100644 --- a/apps/coercion/src/coq_elpi_coercion_hook.mlg +++ b/apps/coercion/src/coq_elpi_coercion_hook.mlg @@ -51,7 +51,7 @@ let add_coercion_hook = } VERNAC COMMAND EXTEND ElpiCoercion CLASSIFIED AS SIDEFF -| #[ atts = any_attribute ] [ "Elpi" "AddCoercionHook" qualified_name(p) ] -> { +| #[ atts = any_attribute ] [ "Elpi" "CoercionFallbackTactic" qualified_name(p) ] -> { let () = ignore_unknown_attributes atts in add_coercion_hook (snd p) } diff --git a/apps/coercion/tests/test_coercion.v b/apps/coercion/tests/test_coercion.v index 76f75527e..932605cb2 100644 --- a/apps/coercion/tests/test_coercion.v +++ b/apps/coercion/tests/test_coercion.v @@ -1,27 +1,27 @@ From elpi.apps Require Import coercion. +From Coq Require Import Bool. -Elpi Accumulate Coercion lp:{{ +Elpi Accumulate coercion.db lp:{{ -coercion _ {{ true }} {{ bool }} {{ Prop }} {{ True }}. -coercion _ {{ false }} {{ bool }} {{ Prop }} {{ False }}. +coercion _ {{ True }} {{ Prop }} {{ bool }} {{ true }}. +coercion _ {{ False }} {{ Prop }} {{ bool }} {{ false }}. }}. -Elpi Typecheck Coercion. +Elpi Typecheck coercion. -Check true : Prop. -Check false : Prop. +Check True && False. Parameter ringType : Type. Parameter ringType_sort : ringType -> Type. Parameter natmul : forall (R : ringType) (n : nat), (ringType_sort R). -Elpi Accumulate Coercion lp:{{ +Elpi Accumulate coercion.db lp:{{ coercion _ N {{ nat }} {{ ringType_sort lp:R }} {{ natmul lp:R lp:N }} :- coq.typecheck R {{ ringType }} ok. }}. -Elpi Typecheck Coercion. +Elpi Typecheck coercion. Section TestNatMul. diff --git a/apps/coercion/tests/test_coercion_load.v b/apps/coercion/tests/test_coercion_load.v index 67e55fa18..ee11df134 100644 --- a/apps/coercion/tests/test_coercion_load.v +++ b/apps/coercion/tests/test_coercion_load.v @@ -1,3 +1,3 @@ Require Import test_coercion. -Check true : Prop. +Check True : bool. diff --git a/apps/coercion/tests/test_coercion_open.v b/apps/coercion/tests/test_coercion_open.v new file mode 100644 index 000000000..4adcb6c57 --- /dev/null +++ b/apps/coercion/tests/test_coercion_open.v @@ -0,0 +1,29 @@ +From elpi.apps Require Import coercion. +From Coq Require Import Arith ssreflect. + +Ltac my_solver := trivial with arith. + +Elpi Accumulate coercion.db lp:{{ + +coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [ + % we unfold letins since the solve is dumb + (pi a b b1\ copy a b :- def a _ _ b, copy b b1) => copy X X1, + % we build the solution + Solution = {{ @exist lp:Ty lp:P lp:X1 _ }}, + % we call the solver + coq.ltac.collect-goals Solution [G] [], + coq.ltac.open (coq.ltac.call-ltac1 "my_solver") G [], +]. + +}}. +Elpi Typecheck coercion. + +Goal {x : nat | x > 0}. +apply: 3. +Qed. + +Definition add1 n : {x : nat | x > 0} := + match n with + | O => 1 + | S x as y => y + end. diff --git a/apps/coercion/theories/coercion.v b/apps/coercion/theories/coercion.v index 352d4dc47..c4b50c273 100644 --- a/apps/coercion/theories/coercion.v +++ b/apps/coercion/theories/coercion.v @@ -1,8 +1,7 @@ Declare ML Module "coq-elpi-coercion.plugin". From elpi Require Import elpi. -Elpi Tactic Coercion. -Elpi Accumulate lp:{{ +Elpi Db coercion.db lp:{{ % predicate [coercion Ctx V Inferred Expected Res] used to add new coercion, with % - [Ctx] is the context @@ -13,8 +12,14 @@ Elpi Accumulate lp:{{ % Be careful not to trigger coercion as this may loop. pred coercion i:goal-ctx, i:term, i:term, i:term, o:term. +}}. + +Elpi Tactic coercion. +Elpi Accumulate lp:{{ + solve (goal Ctx _ Ty Sol [trm V, trm VTy]) _ :- coercion Ctx V VTy Ty Sol. }}. +Elpi Accumulate Db coercion.db. Elpi Typecheck. -Elpi AddCoercionHook Coercion. +Elpi CoercionFallbackTactic coercion. From 1580c7ad3569b52e86253b99e354c64c92848ac8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Aug 2023 14:03:23 +0200 Subject: [PATCH 35/35] close changelog --- Changelog.md | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/Changelog.md b/Changelog.md index cb28294ef..19985282a 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,10 +1,18 @@ # Changelog -## UNRELEASED +## [1.19.0] - 04/08/2023 + +Requires Elpi 1.16.5 and Coq 8.18. + +### APPS +- New `coercion` app providing `coercion` predicate + to program coercions (thanks @proux01). + This app is experimental. ### API: -- Removed option `@nonuniform!` as it disappears from Coq +- Removed option `@nonuniform!` as it disappears from Coq 8.18. (c.f. https://github.com/coq/coq/pull/17716 ) + ## [1.18.0] - 27/07/2023 Requires Elpi 1.16.5 and Coq 8.17. @@ -62,11 +70,6 @@ Requires Elpi 1.16.5 and Coq 8.17. - `derive Inductive i {A}` now sets `A` implicit status globally - `lock Definition f {A}` now sets `A` implicit status globally -### APPS -- New `coercion` app providing `coercion` predicate - to program coercions (requires appropriate version of Coq - with coercion hook https://github.com/coq/coq/pull/17794 ) - ## [1.17.1] - 09/03/2023 Requires Elpi 1.16.5 and Coq 8.17.