diff options
| -rwxr-xr-x | dev/bench/gitlab.sh | 26 | ||||
| -rw-r--r-- | engine/namegen.ml | 8 | ||||
| -rw-r--r-- | tactics/equality.ml | 38 | ||||
| -rw-r--r-- | tactics/hints.ml | 59 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
5 files changed, 86 insertions, 47 deletions
diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh index 38b4e25bde..fe17769d99 100755 --- a/dev/bench/gitlab.sh +++ b/dev/bench/gitlab.sh @@ -12,6 +12,9 @@ r='\033[0m' # reset (all attributes off) b='\033[1m' # bold u='\033[4m' # underline nl=$'\n' +bt='`' # backtick +start_code_block='```' +end_code_block='```' number_of_processors=$(cat /proc/cpuinfo | grep '^processor *' | wc -l) @@ -36,6 +39,7 @@ echo $PWD #check_variable "BUILD_URL" #check_variable "JOB_NAME" #check_variable "JENKINS_URL" +check_variable "CI_JOB_URL" check_variable "coq_pr_number" check_variable "coq_pr_comment_id" check_variable "new_ocaml_switch" @@ -61,8 +65,9 @@ else exit 1 fi -mkdir -p "_bench" -working_dir="$PWD/_bench" +bench_dirname="_bench" +mkdir -p "${bench_dirname}" +working_dir="$PWD/${bench_dirname}" log_dir=$working_dir/logs mkdir "$log_dir" @@ -146,22 +151,31 @@ function coqbot_update_comment() { if [ ! -z "${coq_pr_number}" ]; then comment_text="" + artifact_text="" if [ -z "${is_done}" ]; then comment_text="in progress, " + artifact_text="eventually " else comment_text="" + artifact_text="" fi - comment_text="Benchmarking ${comment_text}log available [here](${BUILD_URL}/console), workspace available [here](${JENKINS_URL}/view/benchmarking/job/${JOB_NAME}/ws/${BUILD_ID})" + comment_text="Benchmarking ${comment_text}log available [here](${CI_JOB_URL}) ([raw log here](${CI_JOB_URL}/raw)), artifacts ${artifact_text}available for [download](${CI_JOB_URL}/artifacts/download) and [browsing](${CI_JOB_URL}/artifacts/browse)" if [ ! -z "${comment_body}" ]; then - comment_text="${comment_text}${nl}"'```'"${nl}${comment_body}${nl}"'```' + comment_text="${comment_text}${nl}${start_code_block}${nl}${comment_body}${nl}${end_code_block}" fi if [ ! -z "${uninstallable_packages}" ]; then comment_text="${comment_text}${nl}The following packages failed to install: ${uninstallable_packages}" fi + comment_text="${comment_text}${nl}${nl}<details><summary>Old Coq version ${old_coq_commit}</summary>" + comment_text="${comment_text}${nl}${nl}${start_code_block}${nl}$(git log -n 1 "${old_coq_commit}")${nl}${end_code_block}${nl}</details>" + comment_text="${comment_text}${nl}${nl}<details><summary>New Coq version ${new_coq_commit}</summary>" + comment_text="${comment_text}${nl}${nl}${start_code_block}${nl}$(git log -n 1 "${new_coq_commit}")${nl}${end_code_block}${nl}</details>" + comment_text="${comment_text}${nl}${nl}[Diff: ${bt}${old_coq_commit}..${new_coq_commit}${bt}](https://github.com/coq/coq/compare/${old_coq_commit}..${new_coq_commit})" + # if there's a comment id, we update the comment while we're # in progress; otherwise, we wait until the end to post a new # comment @@ -430,7 +444,7 @@ done # # The next script processes all these files and prints results in a table. -echo "INFO: workspace = https://ci.inria.fr/coq/view/benchmarking/job/$JOB_NAME/ws/$BUILD_ID" +echo "INFO: workspace = ${CI_JOB_URL}/artifacts/browse/${bench_dirname}" # Print the final results. if [ -z "$installable_coq_opam_packages" ]; then @@ -444,7 +458,7 @@ else rendered_results="$($program_path/render_results "$log_dir" $num_of_iterations $new_coq_commit_long $old_coq_commit_long 0 user_time_pdiff $installable_coq_opam_packages)" echo "${rendered_results}" - echo "INFO: per line timing: https://ci.inria.fr/coq/job/$JOB_NAME/ws/$BUILD_ID/html/" + echo "INFO: per line timing: ${CI_JOB_URL}/artifacts/browse/${bench_dirname}/html/" cd "$coq_dir" echo INFO: Old Coq version diff --git a/engine/namegen.ml b/engine/namegen.ml index fb9f6db0ea..f398f29f41 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -273,8 +273,8 @@ let visible_ids sigma (nenv, c) = accu := (gseen, vseen, ids) | Rel p -> let (gseen, vseen, ids) = !accu in - if p > n && not (Int.Set.mem p vseen) then - let vseen = Int.Set.add p vseen in + if p > n && not (Int.Set.mem (p - n) vseen) then + let vseen = Int.Set.add (p - n) vseen in let name = try Some (List.nth nenv (p - n - 1)) with Invalid_argument _ | Failure _ -> @@ -290,7 +290,7 @@ let visible_ids sigma (nenv, c) = accu := (gseen, vseen, ids) | _ -> EConstr.iter_with_binders sigma succ visible_ids n c in - let () = visible_ids 1 c in + let () = visible_ids 1 c in (* n = 1 to count the binder to rename *) let (_, _, ids) = !accu in ids @@ -416,6 +416,8 @@ let next_name_away_for_default_printing sigma env_t na avoid = *) type renaming_flags = + (* The term is the body of a binder and the environment excludes this binder *) + (* so, there is a missing binder in the environment *) | RenamingForCasesPattern of (Name.t list * constr) | RenamingForGoal | RenamingElsewhereFor of (Name.t list * constr) diff --git a/tactics/equality.ml b/tactics/equality.ml index 2388085059..535725b11d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1013,6 +1013,12 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind = Proofview.tclUNIT (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2])) +type equality = { + eq_data : (coq_eq_data * (EConstr.t * EConstr.t * EConstr.t)); + (* equality data + A : Type, t1 : A, t2 : A *) + eq_clenv : clausenv; + (* clause [M : R A t1 t2] where [R] is the equality from above *) +} let eq_baseid = Id.of_string "e" @@ -1025,7 +1031,7 @@ let apply_on_clause (f,t) clause = | _ -> user_err (str "Ill-formed clause applicator.")) in clenv_fchain ~with_univs:false argmv f_clause clause -let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = +let discr_positions env sigma { eq_data = (lbeq,(t,t1,t2)); eq_clenv = eq_clause } cpath dirn = build_coq_True () >>= fun true_0 -> build_coq_False () >>= fun false_0 -> let false_ty = Retyping.get_type_of env sigma false_0 in @@ -1043,13 +1049,14 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = in discriminator >>= fun discriminator -> discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf -> - let pf_ty = mkArrow eqn Sorts.Relevant false_0 in + let pf_ty = mkArrow (clenv_type eq_clause) Sorts.Relevant false_0 in let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in let pf = Clenv.clenv_value_cast_meta absurd_clause in tclTHENS (assert_after Anonymous false_0) [onLastHypId gen_absurdity; (Logic.refiner ~check:true EConstr.Unsafe.(to_constr pf))] -let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = +let discrEq eq = + let { eq_data = (_, (_, t1, t2)); eq_clenv = eq_clause } = eq in let sigma = eq_clause.evd in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1058,7 +1065,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let info = Exninfo.reify () in tclZEROMSG ~info (str"Not a discriminable equality.") | Inl (cpath, (_,dirn), _) -> - discr_positions env sigma u eq_clause cpath dirn + discr_positions env sigma eq cpath dirn end let onEquality with_evars tac (c,lbindc) = @@ -1071,9 +1078,10 @@ let onEquality with_evars tac (c,lbindc) = let eqn = clenv_type eq_clause' in (* FIXME evar leak *) let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in + let eq = { eq_data = (eq, eq_args); eq_clenv = eq_clause' } in tclTHEN (Proofview.Unsafe.tclEVARS eq_clause'.evd) - (tac (eq,eqn,eq_args) eq_clause') + (tac eq) end let onNegatedEquality with_evars tac = @@ -1385,7 +1393,8 @@ let simplify_args env sigma t = | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma c1;t2;simpl env sigma c2]) | _ -> t -let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = +let inject_at_positions env sigma l2r eq posns tac = + let { eq_data = (eq, (t,t1,t2)); eq_clenv = eq_clause } = eq in let e = next_ident_away eq_baseid (vars_of_env env) in let e_env = push_named (LocalAssum (make_annot e Sorts.Relevant,t)) env in let evdref = ref sigma in @@ -1422,7 +1431,8 @@ let () = CErrors.register_handler (function | NothingToInject -> Some (Pp.str "Nothing to inject.") | _ -> None) -let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = +let injEqThen keep_proofs tac l2r eql = + let { eq_data = (eq, (t,t1,t2)); eq_clenv = eq_clause } = eql in let sigma = eq_clause.evd in let env = eq_clause.env in match find_positions env sigma ~keep_proofs ~no_discr:true t1 t2 with @@ -1437,7 +1447,7 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = | Inr [([],_,_)] -> Proofview.tclZERO NothingToInject | Inr posns -> - inject_at_positions env sigma l2r u eq_clause posns + inject_at_positions env sigma l2r eql posns (tac (clenv_value eq_clause)) let get_previous_hyp_position id gl = @@ -1491,17 +1501,18 @@ let simpleInjClause flags with_evars = function let injConcl flags = injClause flags None false None let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent CAst.(make id))) -let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause = +let decompEqThen keep_proofs ntac eq = + let { eq_data = (_, (_,t1,t2) as u); eq_clenv = clause } = eq in Proofview.Goal.enter begin fun gl -> let sigma = clause.evd in let env = Proofview.Goal.env gl in match find_positions env sigma ~keep_proofs ~no_discr:false t1 t2 with | Inl (cpath, (_,dirn), _) -> - discr_positions env sigma u clause cpath dirn + discr_positions env sigma eq cpath dirn | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *) ntac (clenv_value clause) 0 | Inr posns -> - inject_at_positions env sigma true u clause posns + inject_at_positions env sigma true eq posns (ntac (clenv_value clause)) end @@ -1513,10 +1524,11 @@ let dEq ~keep_proofs with_evars = dEqThen ~keep_proofs with_evars (fun clear_flag c x -> (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)) -let intro_decomp_eq tac data (c, t) = +let intro_decomp_eq tac (eq, _, data) (c, t) = Proofview.Goal.enter begin fun gl -> let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in - decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) data cl + let eq = { eq_data = (eq, data); eq_clenv = cl } in + decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) eq end let () = declare_intro_decomp_eq intro_decomp_eq diff --git a/tactics/hints.ml b/tactics/hints.ml index db4b23705f..355cea8fa8 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -837,7 +837,7 @@ let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) = db = None; secvars; code = with_uid (Give_exact (c, cty, ctx, poly)); }) -let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (c, cty, ctx) = +let make_apply_entry env sigma hnf info ~poly ?(name=PathAny) (c, cty, ctx) = let cty = if hnf then hnf_constr env sigma cty else cty in match EConstr.kind sigma cty with | Prod _ -> @@ -862,25 +862,11 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) ( db = None; secvars; code = with_uid (Res_pf(c,cty,ctx,poly)); }) - else begin - if not eapply then failwith "make_apply_entry"; - if verbose then begin - let variables = str (CString.plural nmiss "variable") in - Feedback.msg_info ( - strbrk "The hint " ++ - pr_leconstr_env env sigma' c ++ - strbrk " will only be used by eauto, because applying " ++ - pr_leconstr_env env sigma' c ++ - strbrk " would leave " ++ variables ++ Pp.spc () ++ - Pp.prlist_with_sep Pp.pr_comma Name.print (List.map (Evd.meta_name ce.evd) miss) ++ - strbrk " as unresolved existential " ++ variables ++ str "." - ) - end; + else (Some hd, { pri; pat = Some pat; name; db = None; secvars; code = with_uid (ERes_pf(c,cty,ctx,poly)); }) - end | _ -> failwith "make_apply_entry" (* flags is (e,h,v) with e=true if eapply and h=true if hnf and v=true if verbose @@ -916,19 +902,25 @@ let fresh_global_or_constr env sigma poly cr = (c, Univ.ContextSet.empty) end -let make_resolves env sigma flags info ~check ~poly ?name cr = +let make_resolves env sigma (eapply, hnf) info ~check ~poly ?name cr = let c, ctx = fresh_global_or_constr env sigma poly cr in let cty = Retyping.get_type_of env sigma c in let try_apply f = - try Some (f (c, cty, ctx)) with Failure _ -> None in + try + let (_, hint) as ans = f (c, cty, ctx) in + match hint.code.obj with + | ERes_pf _ -> if not eapply then None else Some ans + | _ -> Some ans + with Failure _ -> None + in let ents = List.map_filter try_apply [make_exact_entry env sigma info ~poly ?name; - make_apply_entry env sigma flags info ~poly ?name] + make_apply_entry env sigma hnf info ~poly ?name] in if check && List.is_empty ents then user_err ~hdr:"Hint" (pr_leconstr_env env sigma c ++ spc() ++ - (if pi1 flags then str"cannot be used as a hint." + (if eapply then str"cannot be used as a hint." else str "can be used as a hint only for eauto.")); ents @@ -937,7 +929,7 @@ let make_resolve_hyp env sigma decl = let hname = NamedDecl.get_id decl in let c = mkVar hname in try - [make_apply_entry env sigma (true, true, false) empty_hint_info ~poly:false + [make_apply_entry env sigma true empty_hint_info ~poly:false ~name:(PathHints [GlobRef.VarRef hname]) (c, NamedDecl.get_type decl, Univ.ContextSet.empty)] with @@ -1223,9 +1215,28 @@ let add_resolves env sigma clist ~local ~superglobal dbnames = (fun dbname -> let r = List.flatten (List.map (fun (pri, poly, hnf, path, gr) -> - make_resolves env sigma (true,hnf,not !Flags.quiet) + make_resolves env sigma (true, hnf) pri ~check:true ~poly ~name:path gr) clist) in + let check (_, hint) = match hint.code.obj with + | ERes_pf (c, cty, ctx, _) -> + let sigma' = Evd.merge_context_set univ_flexible sigma ctx in + let ce = mk_clenv_from_env env sigma' None (c,cty) in + let miss = clenv_missing ce in + let nmiss = List.length miss in + let variables = str (CString.plural nmiss "variable") in + Feedback.msg_info ( + strbrk "The hint " ++ + pr_leconstr_env env sigma' c ++ + strbrk " will only be used by eauto, because applying " ++ + pr_leconstr_env env sigma' c ++ + strbrk " would leave " ++ variables ++ Pp.spc () ++ + Pp.prlist_with_sep Pp.pr_comma Name.print (List.map (Evd.meta_name ce.evd) miss) ++ + strbrk " as unresolved existential " ++ variables ++ str "." + ) + | _ -> () + in + let () = if not !Flags.quiet then List.iter check r in let hint = make_hint ~local dbname (AddHints { superglobal; hints = r }) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames @@ -1375,10 +1386,10 @@ let expand_constructor_hints env sigma lems = let constructor_hints env sigma eapply lems = let lems = expand_constructor_hints env sigma lems in List.map_append (fun (poly, lem) -> - make_resolves env sigma (eapply,true,false) empty_hint_info ~check:true ~poly lem) lems + make_resolves env sigma (eapply, true) empty_hint_info ~check:true ~poly lem) lems let make_resolves env sigma info ~check ~poly ?name hint = - make_resolves env sigma (true, false, false) info ~check ~poly ?name hint + make_resolves env sigma (true, false) info ~check ~poly ?name hint let make_local_hint_db env sigma ts eapply lems = let map c = c env sigma in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e2d60dfabd..5f7e35d205 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2330,7 +2330,7 @@ let intro_decomp_eq ?loc l thin tac id = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma, t = Typing.type_of env sigma c in - let _,t = reduce_to_quantified_ind env sigma t in + let _,t = reduce_to_atomic_ind env sigma t in match my_find_eq_data_decompose env sigma t with | Some (eq,u,eq_args) -> !intro_decomp_eq_function |